This core lecture (Stammvorlesung) addresses Bachelor and Master students in Computer Science, Bioinformatics, CuK or Computerlinguistics. Bachelor students must have passed the base lecture Programming 1. The lectures Math 1 and 2, Programming 2, and Theoretical Computer Science are recommended.
The aim of this course is to introduce Model Checking as an automatic approach to program verification. As a technique, it is especially suited for verifying properties of concurrent systems which often
comprise many nonterminating and communicating processes.
Given a mathematical model of the system under consideration and a property specification, Model Checking examines all possible system states and checks if the specification is satisfied.
The complexity of concurrent systems is due to the interleaving of the execution of the participating processes as well as to their interaction, for example by inter-process communication.
State-of-the-art model checking tools can handle state-spaces of about one billion distinguished states. Nevertheless, real-life systems may still exceed this limit by orders of magnitude. Therefore, techniques are needed which reduce this growth - known as the state-space explosion problem - without changing the (in-)validity of the specification's properties with respect to the original system-model.
In the first part of this course, we study transition systems as a means of modelling reactive systems and classify some of their important properties.
The second part introduces the automata theory and the temporal logics that Model Checking relies on.
In the third part, we address model checking timed systems.
The last part of the lecture is dedicated to other techniques for verification.
The module is offered in the winter 2006/07. Lectures are scheduled for Tue 14:00-16:00 and Thu 14:00-16:00.
We start on Oct, 17, and end on Feb 15 with a final exam. We have a midterm exam on Dec 21 and a practical exercise between 15.01.07 and 21.01.07 which takes about 20 hours. Excersises take place on Wed either 14:00-16:00 or 16:00-18:00. The lectures will be given in English; exercises are in English and German.
Further details are available at the CMS.
The grade will be based on the midterm exam (35%), the practical exercise (30%) and the final exam (35%).
There will be a minitest prior to the exercise in the individual groups. You need 30% of points of the overall minitest for the final exam. If you answer more questions correctly, you may earn a small bonus on the grade.
The lectures will be held in E 1 3 Hörsaal 001. The exercise classes will be in E 1 3 SR 013, SR 014 and SR 016 (please check the CMS for details).
The grade will be based on the accumulated raw points you earned in your successful examinations. High performance in the quizzes entitles you some bonus points.
Please login into the CMS to get more information!
Lecture Notes & Exercises
Lecture Notes and exercises are available in the CMS.
We will mostly follow the draft book 'Principles of Model Checking' by C. Baier and J.-P. Katoen. The latest versions of the book is not available electronically, but we have chapters (currently chapter 1-6) of the latest draft available for copying. Another version for copying will be available at the CIAM.
If you find some typos or errors, please enter it on this page.
Additional literature can be found in:
M. Huth and M.D. Ryan:
Logic in Computer Science -- Modelling and Reasoning about Systems, Cambridge University Press, 2nd edition, 2004
Verification of Reactive Systems, Springer-Verlag, Texts in Theoretical Computer Science. An EATCS Series, 2004
E.M. Clarke, O. Grumberg, D.A. Peled:
Model Checking, MIT Press, 1999
Symbolic Model Checking, Kluwer Academic, 1993
Concepts, Algorithms and Tools for Model Checking,
Erlangen: Institut für Mathematische Maschinen und Datenverarbeitung, 1999
|Dependable Systems & Software Group||Department of Computer Science||Universität des Saarlandes|