System Behavior Models and Verification – NSWI101

Model Checking
Time and Location: Winter Semester 2018/2019
Lectures: Wednesday, 10:40, S4
Lab: Thursday, 9:00, S7
Guaranteed by: Department of Distributed and Dependable Systems
Winter Term: 2/2 Zk+Z
Lecturers: František Plášil
e-mail: frantisek.plasil<at-sign>
Jan Kofroň
e-mail: jan.kofron<at-sign>
Lab: Jan Kofroň
e-mail for HW: nswi101<at-sign>
Information in SIS: NSWI101


  • There is no lab on Jan 03!
  • The second homework assignment can be found here.
  • There is no lab on Dec 20!
  • The first homework assignment can be found here.
  • There is no lab on Oct 04!



03.10.2018 LTS, Process Algebras lecture01.pdf
10.10.2018 Spin lecture02.pdf
17.10.2018 Kripke Structures, model checking, LTL lecture03.pdf
24.10.2018 LTL Explicit Model Checking lecture04.pdf
31.10.2018 CTL, Explicit CTL Model Checking lecture05.pdf
07.11.2018 Ordered Binary Decision Diagrams lecture06.pdf
14.11.2018 Symbolic CTL Model Checking lecture07.pdf
21.11.2018 Partial Order Reduction lecture08.pdf
28.11.2018 Timed Automata lecture09.pdf
05.12.2018 Infinte-State Model Checking, Bounded Model Checking lecture10.pdf
12.12.2018 Abstractions, Symmetries lecture11.pdf
19.12.2018 Stochastic Model Checking lecture12.pdf
09.01.2019 Assume-guarantee lecture13.pdf


11.10.2018 Spin Exerices Lab01.pdf |
18.10.2018 LTS and Spin Exercises Lab21.pdf | Lab22.pdf
01.11.2018 CTL Model Checking, Spin Exercises Lab051.pdf | Lab052.pdf
08.11.2018 OBDD Exercises Lab06.pdf
06.12.2018 NuSMV Lab08.pdf |
13.12.2018 NuSMV philosophers-soln.smv


Basic concepts of behavior description of parallel and distributed systems. Equivalence checking and model checking — techniques and tools.


  • Practical examples of behavior modeling and verification
    • The SPIN model checker (developed at Bell Labs) which is being successfully used from 1989 for analysis of communication and cryptographic protocols, distributed algorithms and parts of OS kernels (e.g. process schedulers)
    • The NuXMV (SMV) – Symbolic model checker based on Ordered Binary Decision Diagrams
    • UPPAAL model checker
  • Mathematical structures for behavior modeling: labeled transition systems, Kripke structures
  • Timed automata
  • Specification of system properties using temporal logic
  • Basic verification tasks: equivalence checking and model checking
    • Decidability and complexity (of equivalence checking and model checking) in dependence of the type of the model
    • Software tools for equivalence checking and model checking
  • Bounded model checking, probabilistic model checking
  • Open issues in formal verification: infinite-state systems, state explosion problem


The purpose of the lab is to provide students with a hand-on experience with verification tools (SPIN, SMV, UPPAAL), higher-level behavior specification languages (process algebra, behavior protocols), and temporal logics (LTL, CTL).

There will be two assignments (one taking approximately 8 hours of homework, the other an hour). The homeworks are to be submitted via e-mail:

Note: 10 % of your score will be deduced for every calendar day your assignment is late. This implies that no assignment will be accepted after 10 calendar days past its due date.


Final grades will be determined by the quality of homework and the result of the final exam in the following ratio:

  • 55 % Assignments (homework)
  • 45 % Final exam


  • P. Regan, S. Hamilton: NASA's Mission Reliable, IEEE Computer, vol. 37, no. 1, Jan 2004
  • G. J. Holzmann: The Spin Model Checker, Addison Wesley, 2003
  • E. M. Clarke, Jr., O. Grumberg, D. A. Peled: Model Checking, MIT Press, 2002
  • J. A. Bergstra, A. Ponse, S. A. Smolka: Handbook of Process Algebra, Elsevier 2001
  • R. Milner: Communication and Concurrency, Prentice Hall 1989
  • C. Stirling: Modal and Temporal Properties of Processes, Springer 2001
  • F. Plasil, S. Visnovsky: Behavior Protocols for Software Components, IEEE Transactions on Software Engineering, vol. 28, no. 11, Nov 2002 (link)
  • J. Adamek, F. Plasil: Component Composition Errors and Update Atomicity: Static Analysis, Journal of Software Maintenance and Evolution: Research and Practice, 2005 (link)
  • D. Engler: Static analysis versus software model checking for bug finding (paper, slides, other information can be found here)
  • J. Esparza: Software reliability (slides, other information can be found here [text of the web pages in German, referenced documents in English])
  • B. Nielsen: LTS Based Testing and IOCO (slides, other information can be found here)
  • T. Latvala: Reactive Systems (slides)
Modified on 2019-01-09