Faculty of Information Technology, BUT

Course details

Formal Analysis and Verification

FAV Acad. year 2006/2007 Winter semester 5 credits

Course is not open in this year
Close
Formal analysis and verification are modern and rapidly developing approaches to rigorous correctness checking of computer-based systems.The course acquaints students with the theoretical foundations of formal verification, with computer-aided tools based on them as well as with successful applications of formal analysis and verification in practice. An emphasis is put on state spaces-based methods that offer a high degree of automation welcome in practice. The course covers various ways of efficiently generating, reducing and exploiting state spaces of logical-time as well as real-time systems. Theorem proving is then briefly mentioned as an alternative to state spaces-based methods.

Guarantor

Language of instruction

Czech, English

Completion

Credit+Examination (written)

Time span

39 hrs lectures, 13 hrs projects

Assessment points

70 exam, 30 projects

Department

Lecturer

Subject specific learning outcomes and competences

Knowledge of principles and methods of formal analysis and verification and of possibilities of applying them within the process of designing safety-critical systems. Acquaintance with selected computer-aided tools for formal analysis and verification.

Learning objectives

The goal of the course is to acquaint students with formal analysis and verification as a modern and promising  method for 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.).

Study literature

  • Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000. ISBN 0-262-03270-8
  • Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P., McKenzie, P.: Systems and Software Verification: Model-Checking Techniques and Tools, Springer-Verlag, 2001. ISBN 3-540-41523-8

Fundamental literature

  • Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, 2000. ISBN 0-262-03270-8
  • Berard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P., McKenzie, P.: Systems and Software Verification: Model-Checking Techniques and Tools, Springer-Verlag, 2001. ISBN 3-540-41523-8
  • Holzmann, G.J.: The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley Professional, 2003. ISBN 0-321-22862-6
  • Monin, J.F., Hinchey, M.G.: Understanding Formal Methods, Springer-Verlag, 2003. ISBN 1-852-33247-6
  • 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, pp. 429-528. Springer-Verlag, 1998. ISBN 3-540-65306-6

Syllabus of lectures

  1. Capabilities, advantages, and the structure of the (automated) process of formal analysis and verification. 
  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 common modelling languages. Specification and query languages. State space statistics, model instrumentation, Büchi automata, testers.
  4. Temporal logics. LTL, CTL, CTL*, mu-calculus. The relation of temporal logics and automata.
  5. Process algebras. Different relations on processes and possibilities of evaluating them.
  6. Computational complexity of formal analysis and verification tasks.
  7. An overview of the various approaches to reducing state spaces, combining state space generation with reducing and analysing the state spaces. Abstraction, compositionality.
  8. Binary decision diagrams and symbolic methods. Bitstate hashing. Symmetry-based state space reductions. Partial order reduction methods.
  9. Computer-aided tools (model checkers) supporting formal analysis and verification based on state space exploration. Spin, Slam, Blast, Java PathFinder, Zing, SMV, etc.
  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. Modelling and specification languages in the domain of real-time, timed automata, real time temporal logics.
  12. State spaces of real-time systems, regions, zones and automated verification tools based on them (Uppaal, Kronos, TReX, ...). Hybrid systems (HyTech).
  13. Theorem proving. Principles, automated support (PVS, etc.), applications. Combining theorem proving and methods based on state spaces.

Syllabus - others, projects and individual work of students

Two home assignments devoted to creating a model of a simple system and validating its behaviour by means of two chosen tools for formal analysis and verification (Spin, Zing, Blast, SMV, JPF, INA, Uppaal, TReX, PVS, etc.).

Progress assessment

Two evaluated home assignments.

Exam prerequisites

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