Course: Model Checking of Software
- Course (Prof. Dr. Stefan Leue)
Thursday 9:30 - 12:00h Room: D 247
- Tutorial (Dipl. Inf. Christoph Scheben)
Thursday 14:15h - 15:45h Room: D 247
Course OrganizationThe course consists of lectures, tutorials, and a mini-project in which you have a chance to work with the SPIN model checker. You will get a 0.3 bonus for your final exam grade if you can achieve no less than 80% of the total points for the assigned exercises.
Lecture SlidesSlides are usually published after they are covered by the lectures.
- Part 0: Course Organization
- Tutorial: Promela
- Part 9: Fairness
- Part 12: Büchi Automata and LTL
- Part 15: Partial Order Reduction
- Complete [no annotated Version]
ExercisesThe solutions to each assignment will be presented at the tutorial on the same day (Mo 16:15-17:45, D 247) as the deadline for that assignment.
|Publishing Date||Assignment #||Deadline for Submission|
Mini Course Project
A short description of the project is available here: project description.
Further material: Overview of the SIP Protocol.
The tutorial on April 29 will give an introduction to the project and discuss organizational issues.
ParticipantsMaster-level course. Open to Bachelor-level students.
Subject AreaInformatik der Systeme / Angewandte Informatik
Contents / SyllabusThe 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.
- 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.