Advanced Model Checking

News

  • 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.

Schedule

Type Day Time Hall Start Lecturer
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.

screen-shot-2016-10-17-at-17-03-33State space reduction

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).

screen-shot-2016-10-17-at-19-37-50In 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.

Contents

  • 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

Prerequisites

Basic knowledge of automata theory, complexity theory, and data structures and algorithms. The course is a follow-up course of Introduction to Model Checking. It is recommended to have basic knowledge of LTL and CTL model checking, but this is not mandatory.

Exercises

  • 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.

Slides

No. Date Subject Slides Exercise
1  18.10 Introduction  amc16_orga
 amc16_lecture1		  
2  19.10 CTL* and Bisimulation  amc16_lecture2 ex01
3  25.10 Bisimulation Quotienting  amc16_lecture3  
4  26.10 Stutter Bisimulation  amc16_lecture4-6 ex02
5  02.11 Divergence Sensitivity   ex03
6  08.11 Stutter Bisimulation Quotienting  amc16_lecture6 ex04
7  16.11 Simulation and Universal CTL*  amc16_lecture7  
8  23.11 Simulation Quotienting  amc16_lecture8 ex05
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

 amc16_lecture12

 canonicity_proof.pdf

 
13  14.12 Symbolic Model Checking with ROBDDs  amc16_lecture13 ex08
14  10.01 Bounded Model Checking

 amc16_lecture14

See also sections 3+4 in: bmc_material

  
15  11.01 Bounded Model Checking   ex09
16  17.01 Timed Automata  amc16_lecture16 ex10
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
 amc16_lecture20		  

Exam

TBA

Further information

  • 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.
Literature

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.

Links

  • Errata for Principles of Model Checking