- Due to illness, the lecture on Wednesday January 18 does not take place.
- Note that there is no exercise class in the week of January 9-14, 2017.
- The kick-off lecture takes place on Tuesday October 18, 2016.
|Lecture||Tue||14:15 – 15:45||9U10||18.10||Katoen|
|Wed||10:15 – 11:45||5052||19.10||Katoen|
|Exercise||Wed||14:15 – 15:45||4201b||26.10||Quatmann, Volk|
Motivation and background
This course is concerned with model checking, an automated technique to verify properties of hardware and software systems. Whereas the focus of the course Model Checking is on the elementary techniques of model checking, this course is focused on two main topics: advancing current model-checking technology, and, on the other hand, model-checking techniques for quantitative system aspects in particular real-time aspects.
More concretely, the course will -–after a summary of the main model-checking techniques for LTL and CTL-– treat state space reduction techniques. This ranges from algorithms to minimise state-space representations using equivalences and pre-orders (bisimulation and simulation relations), techniques to avoid representing all possible interleaving of concurrent components (partial-order reduction) and data structures for the succinct representation of state spaces (e.g., binary decision diagrams).
In the second part of the course, models and algorithms are treated for the verification of timed properties, such as “is it possible that the system will crash within 30 seconds”. The model of timed automata, their infinite-state semantics, and finite abstractions thereof will be treated. This is complemented by a treatment of algorithms for checking timed reachability properties. This results in an effective framework that is used for checking real-time properties of embedded systems, communication protocols, robotics, and so on.
- Different notions of bisimulation and their minimization algorithms
- Simulation pre-orders, and checking simulation pre-orders
- Partial-order reduction techniques
- Symbolic model checking using binary decision diagrams
- Other symbolic model-checking techniques
- Timed automata
- Timed reachability
- Exercises can be worked on in groups of at most two students.
- To achieve a certificate to this course or to be admitted to the final exam, at least half of the exercises has to be reasonably dealt.
- The exercise sheets will be issued weekly, starting from October 19, 2017.
|2||19.10||CTL* and Bisimulation||amc16_lecture2||ex01|
|6||08.11||Stutter Bisimulation Quotienting||amc16_lecture6||ex04|
|7||16.11||Simulation and Universal CTL*||amc16_lecture7|
|9||29.11||Ample Set Conditions||amc16_lecture9|
|10||30.11||Partial-Order Reduction (1)||amc16_lecture10||ex06|
|11||06.12||Partial-Order Reduction (2)||amc16_lecture11||ex07|
|12||13.12||Reduced Ordered Binary Decision Diagrams|
|13||14.12||Symbolic Model Checking with ROBDDs||amc16_lecture13||ex08|
|14||10.01||Bounded Model Checking||
See also sections 3+4 in: bmc_material
|15||11.01||Bounded Model Checking||ex09|
|17||31.01||Time Divergence, Timelock, and Zenoness||amc16_lecture17|
|18||01.02||Decidability of Timed Reachability||amc16_lecture18 number_of_regions||ex11|
|19||07.02||Zone-Based Reachability and Difference Bound Matrices|| amc16_lecture19
- The lecture will be given in English. All course material (i.e., lecture notes and slides) will be in English.
- The students will be awarded 6 ECTS credits for the lecture after passing the final exam.
The course is based on the book: Principles of Model Checking by Christel Baier and Joost-Pieter Katoen, in particular Chapters 6.7, 7, 8 and 9 and additional material on timed automata not covered in the book. It is possible to buy a book (about 38 euros), but there is no real need to do so as there are various copies of the book available at the CS library.
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.
- E.M. Clarke, O. Grumberg, D.A. Peled: Model Checking, MIT Press, 1999.
- K.L. McMillan: Symbolic Model Checking, Kluwer Academic, 1993.
- Errata for Principles of Model Checking