Lectures: Wednesday, 10:40, Zoom (Jan Kofroň, František Plášil)
Labs: Monday, 10:40, Zoom (Jan Kofroň)
Page in SIS: NSWI101
Grading: Credit and exam
Previous year: 2019/20
News
- The second homework assignment is available here. The deadline is February 28, 2021.
- There will be no practicals class on Mon, November 23, 2020!
- The first homework assignment is available here. The deadline is February 28, 2021.
- The second lecture will be held on Monday, Oct 05, at 10:40, instead of the labs (practicals).
- Sept 24, 2020: The lectures and practicals will be both held using the Zoom platform. You will be informed by email about the connection info in advance.
Lectures
| Date | Title | Downloads |
|---|---|---|
| 30. 09. 2020 | LTS, Process Algebras | lecture01.pdf |
| 05. 10. 2020 | The Spin model checker | lecture02.pdf |
| 07. 10. 2020 | Kripke structures, model checking, LTL | lecture03.pdf |
| 14. 10. 2020 | LTL explicit model checking | lecture04.pdf |
| 21. 10. 2020 | CTL, explicit CTL model checking, fairness constraints | lecture05.pdf |
| 04. 11. 2020 | Ordered binary decision diagrams, fixpoints | lecture06.pdf |
| 11. 11. 2020 | Symbolic CTL model checking, partial order reduction | lecture07.pdf |
| 18. 11. 2020 | Timed automata | lecture08.pdf |
| 25. 11. 2020 | Bounded MC, infinite state MC, compositional reasoning | lecture09.pdf |
| 02. 12. 2020 | Symetries, abstractions | lecture10.pdf |
| 09. 12. 2020 | TLA+ | lecture11.pdf, examples-l11.zip, pluscal.pdf |
| 16. 12. 2020 | TLA+ | |
| 06. 01. 2021 | Probabilistic model checking | lecture13.pdf |
Labs
| Date | Title | Downloads |
|---|---|---|
| 12. 10. 2020 | Spin exercises | slides, examples |
| 19. 10. 2020 | Spin exercises II | slides, examples |
| 26. 10. 2020 | Spin exercises III | examples |
| 02. 11. 2020 | CTL model checking | slides |
| 09. 11. 2020 | OBDD exercises | slides |
| 16. 11. 2020 | NuXMV system | slides |
| 30. 11. 2020 | NuXMV examples | examples |
| 07. 12. 2020 | UPPAAL | |
| 14. 12. 2020 | TLA+ toolbox | AlternatingBit.tla |
Annotation
Basic concepts of behavior description of parallel and distributed systems. Equivalence checking and model checking — techniques and tools.
Syllabus
- 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
- TLA system
- 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
Lab
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: nswi101@d3s.mff.cuni.cz
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.
Grading
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
References
- 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