Lectures on Mondays 11-13, room X 5115.0020.
Lab sessions on Wednesdays 13-15, room V 5161.0207.
(Ocasys page) ||
(Timetables)
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. Some examples of specifications: absence of deadlocks, any assertion on values of variables, race conditions, program termination, absence of overflows, absence of illegal memory access (e.g., array out of bounds, null-pointer dereference), precedence (A always happens before B).
I show you how you can check a system against its specification both (i) statically (i.e., at system design-time or compile-time) and (ii) dynamically (i.e., at system runtime). You will see that both (i) and (ii) build on the same fundamentals, but that the former is (naturally) computationally much more demanding than the latter, while providing more guarantees. In the research literature, you can read more about (i) above by searching for 'model checking' or 'formal verification', and about (ii) by searching for 'runtime checking', 'runtime verification', or sometimes simply 'monitoring'.
For the theory of model checking, we cover transition systems as used to model any system, a temporal logic to write safety and liveness specifications for system behaviour, and finally some model-checking algorithms and their complexity. We see how to automatically extract the necessary formal models out of an existing software implementation of the system, and also how to automatically compute models of concurrent systems out of smaller models of sequential systems. For the practice of model checking, we look at types of system and software errors, and work on examples from the software and protocol-design areas, using the model checkers Spin (now developed at NASA JPL) and CBMC (Bounded Model Checking for ANSI-C, now developed at the University of Oxford).
This is a rather practical course oriented towards debugging realistic systems. The final exam counts for 40% of the final grade, and must be greater than 5. There will be theoretical and practical assignments through the quarter, which together count for the remaining 60% (the grade here should also be at least 5). The assignments have strict deadlines, and can be solved during the lab session (where help is available), or individually at home (help still available through email). The assignments may be submitted both paper-based and electronically.
Lecture 1:
Formal verification: The story about system correctness
(slides)
No lab session in the first week. 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 from software
(slides).
Assignment 1 is at end of the slides; this
has you run through basic exercises using Spin, and then some more realistic automated verification.
All assignments are individual. The deadline is 10 days from the lecture, before the end of the day.
You may hand in as a written report (electronically by mail),
or as an in-person demonstration (during any lab session).
Lecture 3:
System specification with Linear Temporal Logic
(slides).
The second assignment is at the end of these slides; this one is about writing and
using program properties for verification. You see two applications: a piece of code with
known bugs from a spacecraft, and mutual exclusion code.
Lectures 4-5:
Automata-based model checking for LTL
(slides).
This file contains both Lecture 4 on omega-automata, and Lecture 5 on
an automata-based model-checking algorithm.
The third assignment (and last using Spin) is at the end of the slides;
this assignment allows some free choice, and includes
checking some concurrent software,
checking a small networking protocol (the alternating-bit protocol),
and some related scientific literature.
Lecture 6:
Bounded Model Checking with SAT
(slides).
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 a research paper. The deadline is Jan 13.
Assignment five (and last) is simply last year's exam, and is online. You only need to submit 3 of those 5 problems to get the remaining 30 centipoints for a maximum practical grade. The deadline for this is Jan 20, before the end of the day, i.e. two days before the exam.
Lecture 7:
Runtime Verification for LTL
(slides).
This shows you how to check a system at runtime against
the same temporal specifications as before.
Lecture 8:
The bigger picture of formal verification
(slides).
This aims to widen the view on verification techniques, and briefly
introduces past-time LTL, timed, and probabilistic model checking.