Course: Model Checking of Software and Systems
Schedule
- Course (Prof. Dr. Stefan Leue)
Wednesday 10:15 - 11:45h Room: C 252
Thursday 10:15 - 11:45h Room: D 247
- Tutorial (Alina Bey)
Monday 16:15 - 17:45h Room: P 912
Description
Participants
Master-level course. Open to Bachelor-level students.
Subject Area
Informatik der Systeme / Angewandte Informatik
Contents / Syllabus
The course will introduce into explicit state model checking for reactive software systems. Model checking is an algorithmic, automated technique for the behavioral analysis of soft- and hardware systems. We will illustrate the algorithmic foundations of this technique, present the SPIN tool, and address advanced topics. The accompanying project will address the modeling and analysis of an industrial case-study. Participants are expected to possess a basic knowledge in programming, concurrent systems, automata theory and logic.
Literature
- E. Clarke, O. Grumberg and D. Peled, Model Checking, MIT Press, 1999
- C. Baier and J.-P. Katoen, Principles of Model Checking, MIT Press, 2008
- G. Holzmann, The SPIN Model Checker - Primer and Reference Manual, Addison Wesley, 2003
Further literature will be announced during the course.
Lecture Slides
To access the lecture slides of the course, you need a user name and a password. Please contact Alina Bey to obtain it.
- Part 0: Course Organization
- Part 1: Systems and Software Failures
- Part 2: Model Checking in the Software Process
- Part 3: State-Based Modeling using Promela and SPIN
- Part 4: Transition Systems
- Part 5: Modeling Concurrency
- Part 6: State Machine Models and the State Explosion Problem
- Part 7: Linear-Time Properties and Invariants
- Part 8: Safety and Liveness
- Part 9: Fairness
- Part 10: Model Checking Regular Safety Properties
- Part 11: Büchi Automata and ω-Regular Languages
- Part 12: Linear Temporal Logic
- Part 13: Büchi Automata and LTL
- Part 14: Algorithms for Checking Safety Properties
- Part 15: Model Checking ω-Regular Properties
- Part 16: Partial Order Reduction
Assignments
- Assignment 1
- Assignment 2 and Promela Code
- Assignment 3
- Assignment 4
- Assignment 5
- Assignment 6
- Assignment 7
- Assignment 8
Mini Course Project
A short description of the project is available here: Project Description.
Further material: Overview of the SIP Protocol.
Credits
SWS: 6
ECTS-points: 10
