![[Mail]](../../../../Images/umschlag.gif)
| Webmaster | Disclaimer | Last modified: 2006-04-07 09:51 UTC |
![[I2 logo]](../../../../Images/i2.gif)
![[RWTH logo]](../../../../Images/rwth-rot90.gif)
(Informatik 2)
HomeNewsJobsContactStaffTeachingResearchMOVES SeminarDFG-GK AlgoSynCS ChairsLuFG I2
Model Checking
Graduate Course - Winter Term 2005/06
Lehrstuhl für Informatik 2
Schedule
| Type | Time | Place | Start | Lecturer |
|---|---|---|---|---|
| V4 | Tue 14:00-15:30 | AH II | 18.10. | Katoen |
| Wed 10:00-11:30 | AH II | 19.10. | Katoen | |
| Ü2 | Fr 10:00-11:30 | AH II | 21.10. | Neuhäußer |
News
- The results of the repetition exam are available.
- The repetition exam takes place on Friday, March 31st (10:00-11:30 in AH III).
Further information - The results of the exam are available here.
- A corrected version of slide 5 of Lecture 25 has been put on the web on February 8. To replace the CTL state-formulas in a CTL fairness constraint by an atomic proposition, the standard CTL semantics has to be applied, and not the fair one!
- The exam will take place on Friday, Feb. 10th. from 10:00 until 11:30 in AH II
The only allowed materials are a copy of the lecture notes and a copy of the slides.
Motivation and background
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 reactive 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.
Contents
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 the state-space explosion problem and study techniques that allow to reduce the system model's size.
The last part of the lecture is dedicated to model checking probabilistic systems. Here, we study how to verify quantitative properties like "in 99% of all cases, no deadlock occurs".
- modelling concurrent and communicating systems
- transition systems
- parallelism and communication
- the state-space explosion problem
- linear time properties
- deadlocks
- reachability
- liveness
- fairness
- regular properties
- automata on finite words
- automata on infinite words
- regular sequence properties
- model checking
- linear time temporal logic (LTL)
- computation tree logic (CTL)
- combating the state-space explosion
- equivalences and abstraction
- partial-order reduction
- symbolic model checking with binary decision diagrams
- model checking probabilistic systems
- probabilistic computation tree logic (PCTL)
Previous knowledge
Apart from the standard courses in the first two years (like automata theory and mathematical logic), there are no mandatory courses required.Language
The lecture will be given in English.All course material (i.e., lecture notes and slides) will be in English.
Exercises
Exercises can be worked on in groups of at most two students. To achieve a certificate to this
course, at least half of the exercises has to be reasonably dealt with and a final exam has to be passed.
The exercise sheets will be issued weekly.
Overhead transparencies
All overhead transparencies that are used during the lecture will be made available here.| Date | Lecture | Subject | Slides | Exercise |
|---|---|---|---|---|
| October 18 | 1 | Introduction |
Lecture 1 | Exercise 0 |
| October 19 | 2 | Transition Systems |
Lecture 2 | Exercise 1 |
| October 25 | 3 | Concurrency (1) |
Lecture 3 | |
| October 26 | 4 | Concurrency (2) |
Lecture 4 | Exercise 2 |
| November 4 | - | Exercise Class |
- | Exercise 3 |
| November 8 | 5 | Linear-Time Properties |
Lecture 5 | |
| November 9 | 6 | Safety and Invariants |
Lecture 6 (updated on 14.11) |
Exercise 4 |
| November 15 | 7 | Liveness |
Lecture 7 | |
| November 16 | 8 | Fairness (1) |
Lecture 8+9 | Exercise 5 |
| November 22 | 9 | Fairness (2) |
||
| November 23 | 10 | Verifying Regular Safety Properties |
Lecture 10 | Exercise 6 |
| November 29 | 11 | Buechi Automata (1) |
Lecture 11+12 | |
| November 30 | 12 | Buechi Automata (2) |
Exercise 7 | |
| December 6 | 13 | Buechi Automata (3) |
Lecture 13 | |
| December 7 | 14 | Verifying Omega-Regular Properties |
Lecture 14 | Exercise 8 |
| December 13 | 15 | Nested Depth-First Search |
Lecture 15 | |
| December 14 | 16 | Linear Temporal Logic (1) |
Lecture 16 | Exercise 9 |
| December 20 | 17 | Linear Temporal Logic (2) |
Lecture 17 | |
| December 21 | 18 | Fairness in LTL |
Lecture 18 | Exercise 10 |
| January 10 | 19 | From LTL to Automata (1) |
Lecture 19+20 | |
| January 11 | 20 | From LTL to Automata (2) |
Exercise 11 | |
| January 18 | 21 | SPIN and Promela |
Lecture 21 (slides by Theo C. Ruys) |
|
| January 20 | 22 | Computation Tree Logic (1) |
Lecture 22 | Ex 12a Ex 12b |
| January 24 | 23 | Computation Tree Logic (2) |
Lecture 23 | |
| January 25 | 24 | CTL Model Checking |
Lecture 24 | Exercise 13 |
| January 31 | 25 | Fairness and CTL* |
Lecture 25 | |
| February 1 | 26 | Bisimulation Equivalence |
Lecture 26 | Exercise 14 |
| February 7 | 27 | Simulation Order (1) |
Lecture 27+28 | |
| February 8 | 28 | Simulation Order (2) |
Links
- symbolic CTL model checking: the symbolic model verifier (SMV)
- LTL model checking: the spin model checker
Literature
Notes are made available to students attending the lecture.
They will be revised as the course proceeds and can be downloaded here.
They may be accessed only from within Aachen university and with the password
given in the first exercise class.
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 (Library)
- K. Schneider: Verification of Reactive Systems, Springer-Verlag, Texts in Theoretical Computer Science. An EATCS Series, 2004 (Library)
- E.M. Clarke, O. Grumberg, D.A. Peled: Model Checking, MIT Press, 1999 (Library)
- K.L. McMillan: Symbolic Model Checking, Kluwer Academic, 1993 (Library)
-
J.-P. Katoen:
Concepts, Algorithms and Tools for Model Checking,
Erlangen: Institut für Mathematische Maschinen und Datenverarbeitung, 1999 (Library)
