As the complexity of computer systems and the risk of their potential failures are increasing, it becomes more and more important to prove that the design and implementation of critical system components are correct (error-free). One of the typical solutions for the challenge of provably correct design is the application of formal methods: formal models provide a precise and unambiguous specification of requirements and construction of design models; formal verification allows the checking of design decisions and proof of properties; and the verified models allow automated software synthesis. The subject provides an overview of the background that is needed for the construction and analysis of the formal models of IT components and systems, including the most important modelling languages, as well as the related analytical and simulation-based verification methods. The subject demonstrates the application of formal methods in the field of requirement specification, system and software design, model based verification, and source code synthesis.
Students who successfully fulfil the requirements of the course will be able
(1) to understand and apply various formal methods,
(2) to construct formal models based on informal system descriptions,
(3) to understand the advantages and limitations of formal verification techniques,
(4) to use tools that support the application of formal methods.