3.1 Model Checking and NuSMV
1. Introduction to Model Checking
Watch
Introduction to Model Checking (9:10)
Read
- Introduction to model checking Download Introduction to model checking by S. Merz (preprint of chapter 3 of "Modeling and Verification of Real-Time Systems: Formalisms and Software Tools").
2. NuSMV
Watch
Introduction to NuSMV (6:54)
Modules in NuSMV (3:50)
Read
- Official NuSMV tutorial Links to an external site.. This tutorial is rather dense and approaches the material a bit differently. It also includes features that are not covered in this lecture. Use this tutorial if you need more examples and as a different type of source for learning.
- Official NuSMV user manual Links to an external site.. Use this if you need a reference for the syntax and semantics of NuSMV, and advanced usage.
Do
3. Temporal properties
Introduction to temporal logic (13:35)
Safety/Liveness (3:16)
Reflect
- What kinds of everyday properties can you model easily in temporal logic? How?
- What kinds of properties seem to be difficult?
- What kinds of pitfalls exist when modeling properties in temporal logic?
4. Fairness
Fairness (9:12)