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 apply tools that support the application of formal methods.

1. The role of formal methods in the development of IT systems (introduction): formal requirements specification, modelling, verification (model checking, proof of correctness). Relationship between engineering and formal models, model mappings. Design tools and environments using formal methods (examples).2. Basic formal models and their semantics: Kripke structures, labelled transition systems, Kripke transition systems, timed automata and networks of timed automata.3. Formalization of requirements with temporal logics: Linear temporal logic (LTL), branching time temporal logics (CTL, CTL*). Comparison of expressiveness.4. Formal verification with model checking: Model checking with tableau method and symbolic techniques. Verification of time-dependent behaviour.Related teaching material: Tutorial on UPPAAL. https://uppaal.org/documentation/5. Verification of models with a large state space: Representation of the state space using decision diagrams. Bounded model checking.6. Practical applications: Modelling embedded controllers and protocols with timed automata; checking temporal properties using the UPPAAL model checker. Automatic test case generation using model checkers. Monitor synthesis based on temporal logic properties.7. High-level modelling of state-dependent behaviour: Formal semantics of statecharts. Design using statecharts, verification of statecharts. Common solutions of statechart-based source code synthesis.8. Modelling concurrent systems and analysis of their behavioural properties: The Petri net formalism. Checking the dynamic properties of models (deadlocks, liveness, boundedness, persistence, home states) by simulation or based on the reachability graph. Hierarchical Petri nets. Modelling examples.9. Analysis of the structural properties of concurrent systems: Expression and verification of invariants related to states and behaviour, structural boundedness and controllability. Property-preserving model reduction techniques.10. Modelling data-dependent behaviour: Modelling data types and data manipulation. Extension of dynamic and structural properties. Practical application examples: Verification of the consistency of distributed data management, analysis of protocols.11. Specification and verification of extra-functional properties: Extension of Petri nets with probability and time; Stochastic Petri nets. Formalization of requirements for stochastic analysis, evaluation of performance and reliability properties.12. Model refinement: Methods of systematic model refinement. Checking the consistency of model refinement using behavioural relations.13. Formal verification techniques based on software source code: Model checking of C programs. The use of abstraction: static analysis with abstract interpretation, predicate abstraction, counterexample-guided abstraction refinement during model checking.14. Proving program correctness: Formalization of contracts, pre- and post-conditions, invariants, their verification based on the high-level description and intermediate representation of the algorithms.