Overview of the course:
This course introduces the students to an approach to validation of hardware and software based on formal analysis of system behaviors. Among the formal methods, model checking enjoys considerable popularity because of its relatively high degree of automation. This approach has been highly effective in the analysis of integrated circuits designs, and nowadays it is an integral part of the design cycle in companies like Intel, IBM, and Cadence.
The course presents the foundations of model checking starting from the modelling of systems and properties, and then proceeding with the basic algorithms for model checking. Among other things, the distinction between branching time and linear time is discussed, safety and liveness properties are defined, and the use of logics and automata as specifications is discussed. Various logics are introduced, including CTL*, CTL, and LTL. It is shown that model checking for CTL can be reduced to the computation of fixed points of appropriate monotonic functions, and that LTL model checking is based on the translation of the given formula into a Buechi automaton. Both the explicit and the symbolic approaches to model checking are outlined. The students will apply the acquired knowledge on modeling and validation of complex systems in the lab with the SPIN model checker.
Lectures + laboratory. The laboratories for the course focus on the usage of the model checker vis, with emphasis on modelling aspects. The students familiarize with the logic CTL, the proper use of fairness constraints, and the application of model checking techniques to planning problems.
More info here.