Model Checking and NuSMV

Note: The first part corresponds to the second half of Lecture 4 (after the concluding lecture on Event-B). Please watch that video and read the first part of the background material before that lecture. The following parts consist of two videos, each belonging to one lecture (Lectures 5–7).

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 and recording

Slides (PDF) Download Slides (PDF)

Lecture recording (41:29)

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.