Model-Checking SS 2009

News | Basic information | Content | Exercises | Slides | Links

Model-Checking (also in German: Modellprüfung) is a technique for automatic verification of hardware and software systems. Given a such system and a correctness specification, a model checker checks if the system works correctly.

Since mid-80s Model-Checking is been used and has achieved enormous progress, especially in the hardware sector. Nowadays all the major hardware manufacturer have Model-Checking groups, that have developed software tools applied for the verification of large circuits. Last year, the Model-Checking's inventors has awarded by the Turing-Award.

In the lecture will been discussed the basics of Model-Checking. It will be illustred how systems can be modeled, and how one can express correctness specifications using temporal logic. It will then describe the algorithms that automatically test whether the model holds the properties formulated in temporal logic. In the lecture is also presented some common tools such as Spin and SMV. As a listener you will have the opportunity to try out these tools.

In the winter semester will be a further lecture with the title Model-Checking II, that will be held from Mr. Esparza.

For understanding the lecture only some general knowledge are preconditioned from the basic studies.

Literature:

The lecture is not oriented to a particular book. For deeper understanding may, however, e.g. serve the following works:

• Clarke, Grumberg, Peled: Model Checking, MIT Press, 1999
• Emerson: Temporal and Modal Logic, Chapter 16 in "Handbook of Theoretical Computer Science", vol. B, Elsevier, 1991
• Holzmann: The SPIN Model Checker, Addison-Wesley, 2003

It will be used the lecture slides that can be found here.