Automated reasoning designs computing systems which automate the process of making inferences. This course gives an introduction to the principles and practice of Model Checking, a verification technique which automatically and soundly checks whether a given model of a system conforms to a given specification.
For the theory of model checking, we cover transition systems as used to model systems, a temporal logic to write safety and liveness specifications, and matters of complexity of model-checking algorithms. We overview techniques which tackle the state-space explosion problem when checking large models such as those of concurrent systems, and techniques to automatically extract the necessary formal models out of a software implementation. For the practice of model checking, we use model checking tools on examples from the software and protocol-design areas, using model checkers such as SPIN and CBMC (Bounded Model Checking for ANSI-C).
This is a rather practical course oriented towards debugging realistic enough software. The final exam counts for 50% of the final grade. There will be practical assignments through the quarter, which together count for the remaining 50%; these have strict deadlines, and can be solved during the lab session (where help is available), or individually at home (help will still be available through email). The assignments may be submitted both paper-based and electronically.
Lecture 1: Model Checking: Motivation and course overview [slides
(pdf)]. (Nov 15, 2011)
No assignment; try to get your hands on the two
recommended books (Clarke et al., and Holzmann), and install yourselves the
latest version of SPIN.
Lecture 2: Modelling systems and model extraction [slides (pdf)]. (Nov
22, 2011)
The last few slides of the lecture also contain the assignment;
this has you run through basic exercises using Spin, and do model extraction out
of code.
All assignments are individual. The deadline is a week from the lecture, at 5pm.
You may hand in as a written report (either electronically or during the lab),
or as an in-person demonstration (during the lab).
Lecture 3: System specification with Linear Temporal Logic [slides
(pdf)]. (Nov 29, 2011)
The second assignment is at the end of these
slides; this one is about using assertions for verification, writing and using
LTL for verification, and a few exercises on program properties (number of
distinct executions, deadlock, starvation, termination).
For this, you have one week and a half. The same rules apply as for the first
assignment.
Lectures 4 and 5: Explicit-state Model Checking for LTL [slides (pdf)]. (Dec 6
and 13, 2011)
This contains both the Lecture 4 on omega-automata, and
Lecture 5 on the automata-based model-checking algorithm.
The third
assignment is at the end of the slides; this assignment includes checking a
small abstraction of the Mars Pathfinder software for a deadlock, checking a
small networking protocol (the alternating-bit protocol) and some exercises on
automata theory.
The deadline is Thu Dec 22.
Lecture 6:
Bounded Model Checking with SAT [slides (pdf)]. (Dec 20, 2011)
This
lecture introduces another model checking algorithm for C software, and the
model checker CBMC.
Assignment four is at the end of the slides; this
demonstrates software model checking on C code, with the CBMC model checker. The
first part of the assignment has you look into classical software bugs; the
second part asks you to read two research papers.
The deadline is Jan 15.
Lecture 7: Decreasing the state-space with partial-order reduction [slides
(pdf)]. (Jan 10, 2012)
We see a method to reduce the state-space of a
system model without losing behaviour relevant from the point of view of the
specification.
Assignment five [(pdf)] (optional!) is closer to the exam
format; submit anytime until Mon Jan 23.
Lecture 8: The bigger picture: other techniques for analysis and
verification [slides (pdf)]. (Jan 17, 2012)
This aims to widen the view
on verification techniques, and briefly introduces timed, probabilistic, and
SMT-based model checking, and finally runtime verification.