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"). We recommend that you study this text twice: First as background material after having taken the lecture "Introduction to Model Checking", and then again to help you prepare for the exam.
Do
- Answer the Quiz on "The SLAM Toolkit" correctly. (You can retry until you pass.)
Lecture slides
Slides (PDF) Download Slides (PDF)
2. Introduction to Model Checking (2), NuSMV
Watch
Introduction to NuSMV (6:54)
Introduction to temporal logic (13:35)
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
Lecture slides
Slides (PDF) Download Slides (PDF)
3. NuSMV (2)
Modules in NuSMV (3:50)
Safety/Liveness (3:16)
Lecture slides
Slides (PDF) Download Slides (PDF)
4. BDDs, Fairness
Watch
Binary Decision Diagrams (BDDs) (5:37)
Fairness (9:12)
Pitfalls in Modelling Systems (6:21)
Do
Lecture slides
Slides (PDF) Download Slides (PDF)