Formal Analysis and Verification

• 26 hrs lectures
• 26 hrs projects

Students are acquainted with principles and methods of formal analysis and verification and with their application within the process of designing safety-critical systems. Students know capabilities and the basic ways of using computer-aided tools for formal analysis and verification.

Acquired knowledge about the significance and possibilities of using formal methods within the development of various kinds of systems and about their growing use in practice.

The goal of the course is to introduce formal analysis and verification to students as a modern and promising  method of automated evaluation of properties of various kinds of safety-critical systems (such as drivers and other parts of operating systems, control software, workflow, communication protocols, parts of hardware, etc.). The course acquaints students both with the theoretical background of the given area, with computer-aided tools based on them as well as with successful applications of formal analysis and verification in practice (Intel, Nasa, Microsoft, Ericsson, Nokia, ...).

There are no prerequisites

• Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008.
• Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005.
• Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
• Aho, A.V., Lam, S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools. Addison Wesley, 2nd ed., 2006. (Část věnovaná statické analýze.)
• Bradley, A.R., Manna, Z.: The Calculus of Computation: Decision Procedures with Applications to Verification, Springer, 2007.
• Valmari, A.: The State Explosion Problem. In Reisig, W., Rozenberg, G.: Lectures on Petri Nets I: Basic Models, volume 1491 of Lecture Notes in Computer Science, pages 429-528. Springer-Verlag, 1998.
• Chess, B., West,J.: Secure Programming with Static Analysis. Addison-Wesley Professional, 2007.
• Khedker, U., Sanyal, A., Sathe, B.: Data Flow Analysis: Theory and Practice, CRC Press, 2009.
• Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, Springer, 2008.
• Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley Professional, 2003.
• Ben-Ari, M.: Principles of the Spin Model Checker, Springer, 2008.
• Bertot Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq'Art: The Calculus of Inductive Constructions, Springer, 2010.
• Soubor materiálů prezentovaných na přednáškách a zveřejněných přes WWW.
• Materiály aktuálně volně dostupné na Internetu, a to zejména články a dokumentace týkající se počítačových nástrojů pro formální analýzu a verifikaci.

• Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, 2008.
• Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis, Springer-Verlag, 2005.
• Edmund, M.C., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000.
• Khedker, U., Sanyal, A., Sathe, B.: Data Flow Analysis: Theory and Practice, CRC Press, 2009.

1. The meaning of the terms ``formal analysis and verification''. Capabilities and contribution of formal analysis and verification. The structure of the (automated) process of formal analysis and verification. Theorem proving, using state spaces, the state explosion problem.
2. State spaces, state space paths, abstractions of states and transitions. Interleaving and true concurrency. Linear and branching time. Safety, liveness, and fairness.
3. A brief overview of commonly used modelling languages (networks of finite automata, Petri nets, specialized parallel languages, etc.). Specification and query languages. Statistics on the level of state spaces and on the level of modelling languages. Model instrumentation, Büchi automata, testers.
4. Temporal logics. LTL, CTL, CTL*, mu-calculus. The relation of temporal logics and automata. Indexed temporal logics.
5. Process algebras. A generalized view on process algebras, their relation to state spaces, operators of hiding and parallel composition. The different process algebraic equivalences and preorders, possibilities of evaluating them.
6. Computational complexity of formal analysis and verification tasks. Complexity w.r.t. the size of state spaces and w.r.t. the size of models. The relation of time and space requirements of formal analysis and verification methods.
7. State space reduction. An overview of the various approaches to reducing state spaces, combining state space generating and reducing algorithms with algorithms analyzing the state spaces. Abstracting and transforming models. Compositionality.
8. State space reduction. Binary decision diagrams and symbolic methods. Bitstate hashing. Reducing state spaces using symmetries in the behaviour of the modelled systems. Partial order reduction methods.
9. Computer-aided tools supporting formal analysis and verification using state spaces. Spin, Slam, Java PathFinder, Zing, SMV, etc. (according to the state of the art).
10. An overview of successful applications of formal analysis and verification in the area of embedded systems, protocol engineering, control systems, workflow, etc.
11. Real time systems. Logical and physical time. Safety, liveness, and feasibility in real time. Modelling and specification languages in the domain of real time, timed automata, real time temporal logics.
12. Dealing with state spaces of systems working in real time, regions, zones. Automated support for formal analysis and verification of real time systems (Uppaal, Kronos, TReX, ...) and their applications. Hybrid systems (HyTech).
13. Theorem proving. Principles, automated support (PVS, etc.), applications. Combining theorem proving and methods based on state spaces

Study evaluation is based on marks obtained for specified items. Minimimum number of marks to pass is 50.

Having at least 50% of the possible point evaluation of the homeworks.

• Two evaluated home assignments - each for 15 points.
• A final written examination - 70 points.
• To be allowed to sit for the written examination, a student is to earn at least 15 points during the semester.
• The passing boundary w.r.t. the ECTS assessment - 50 points.