Activity description

Laboratory for Microcomputer Systems

In the area of ensuring the correctness of systems, both action-based and status-based approaches have their own good and bad features. The current approach to the specification and reasoning of reversible systems represents an alternative to the prevailing action-based approaches to date. For modern network technologies such as software-defined networks and the Internet of Things, proper and reliable operation is very important. Because these technologies are relatively new, formal methods and tools are not yet well developed for them. One useful tool is the integrated SpinRCP development environment, which is freely accessible to all users of the Spin verification tool. By introducing new functionality into SpinRCP, the lab contributes to the development of science and the greater use of formal methods in the design of modern networks and protocols.