AKA Practical Course “Germany’s Next Top Model Checker”

Practical Software Lab Course for the Master Programme, Winter Semester 2024/25. This practical course complements our lecture in the same semester, Model Checking, which will introduce the theoretical aspects.

Motivation: Model Checking

Digital systems are a fundamental aspect of our modern society and are often found in critical environments, where a malfunction causes serious material or personal damage. Formal verification mathematically proves system correctness to methodically rule out system failure.

Model Checking is a formal verification technique that is applicable throughout a system’s life cycle. For example, hardware developers such as IBM and Intel commonly use model checking to verify their products. The model checking tool SLAM—developed at Microsoft—which verifies device drivers. Software model checkers such as CPAchecker verify the correctness of program code.

The technique works by providing a model—a “blueprint” of the system specifying its behavior—and a set of properties that are derived from the system’s requirements. A model checker, i.e., a tool implementing model checking algorithms, then checks if the given model satisfies the given properties and returns that all properties are satisfied or which properties are violated. A major reason for the success of model checking is that this process is fully automatic: once model and properties are given, no further user input is needed.

Topics and Goals

In this practical course, students will implement their own model checker using algorithms and data structures introduced in the Model Checking lecture. Given a transition system as a model, we will follow along the lecture in implementing algorithms to e.g. compute the set of reachable states, check properties specified using linear temporal logic (LTL) or computation tree logic (CTL), apply bisimulation minimisation, and more.

Organization

News

• September 3: Page published

Registration

Please contact gntmc@moves.rwth-aachen.de if you are interested in this practical lab. Registration through the SuPra system is not possible at the moment.

Prerequisites

Participation in the model checking lecture (either in the current winter term or in a previous iteration) is recommended, although not a hard requirement.

Meetings

Plenary meetings will be held approximately every two weeks to discuss previous assignments, the next assignment, and overall flow of the course.

The first meeting takes place in the week from Nov 4. A precise date and time for the regular meetings will be agreed upon with the organisers and participants.

Discussion Forum

A discussion forum will be made available for general and technical questions and discussions among students. Students are urged to answer other student’s questions.

Remarks

• Attendance of every group meeting is mandatory.
• The language for this course will be English.
• Students are expected to form and work in groups of 3-4 students.
• Grades are based on the quality of the presentations, the quality of the source code, and the performance of the implementation.
• The implementation language is not fixed. Each group can choose freely (e.g. C++, Java, Rust, …). As performance is a concern, some languages are more suitable than others, though. Note that we do require good source code quality, including unit tests.
• We will make use of the university’s GitLab instance: https://git.rwth-aachen.de

Course Material

The course (as well as the related lecture) are based on

Principles of Model Checking
by Christel Baier and Joost-Pieter Katoen
MIT Press, 2008.

Note: It is possible to buy a book (about 40 euros), but there is no need to do so as there are various copies of the book available at the CS library.

There is also an errata document here.

Additional literature:

• E.M. Clarke, O. Grumberg, D.A. Peled: Model Checking, MIT Press, 1999.
• M. Huth and M.D. Ryan: Logic in Computer Science – Modelling and Reasoning about Systems, Cambridge University Press, 2nd edition, 2004.
• K. Schneider: Verification of Reactive Systems, Springer-Verlag, Texts in Theoretical Computer Science. An EATCS Series, 2004.

Our probabilistic model checker Storm: In our group, we develop the model checker Storm which can handle probabilistic models. Although we will not discuss probabilistic models in this practical course, our recent publications on Storm might be of interest.

Contact

The course is organized by Tim Quatmann and Philipp Schroer. If you have any questions, please send an email to gntmc@moves.rwth-aachen.de.