Practical course in Model Checking

Content

Model Checking is an automatic approach to program verification. In this practical course we will consider real world systems and specify their designated behavior. We then use the state of the art Model Checker Spin and its modelling language Promela to build a verification model of the system under consideration. Subsequently, Spin is used to check whether our model complies with the specification.

In this lab, we will start with some introductory examples of how to use Spin and its modelling language Promela.
Then we will consider different distributed algorithms like
- mutual exclusion algorithms,
- leader election protocols and
- routing protocols.
The aim is to model these algorithms in Promela and - dependent on the protocol under consideration - specify the important properties.

Schedule

There will be regular meetings to discuss the achievements made so far as well as to determine the next objectives. The meetings take place in the seminar room (room 4201b) of the chair:

Date	Topics	Slides
07.04.2006, 14:30	First meeting: Introduction	Organization and Spin Tutorial
26.04.2006, 15:00	Szymanski presentation and byzantine consensus	Szymanski
19.05.2006, 13:00	Byzantine consensus protocol presentation	Phase Queen
31.05.2006, 15:00	E-Commerce protocol presentation	E-Commerce
23.06.2006, 13:00	First TORA meeting	Slides
05.07.2006, 15:00	Second TORA meeting	Slides

Contact

For questions please contact

Preliminaries

Apart from the standard courses of the first two years (like automata theory and mathematical logics), a lecture in Model Checking is required.
Good knowledge of programming languages like Java, C or C++

Practical course in Model Checking

Content

Schedule

Contact

Preliminaries

Links