Course: Model Checking of Software and Systems

Course: Model Checking of Software and Systems

Schedule

• Course (Prof. Dr. Stefan Leue)
  Monday 10:00 - 11:30  Room: PZ 801
  Wednesday  10:00 - 11:30  Room: PZ 901

• Tutorial (Alina Bey)
  Wednesday 11:45 - 13:15 Room: G 308

Description

Contents

All materials needed for the course are available from the Ilias-Webpage.

First you have to log-in with your uni-e-mail credentials. Afterwards you have to sign-up for the course.

The password will be announced in the first lecture.

Participants

Master-level course. Open to Bachelor-level students.

Subject Area

Informatik der Systeme / Angewandte Informatik

Prerequesites

Bachelor level background in programming, algorithms, concurrent systems, automata theory, graph theory and logic.

Contents / Syllabus

The course will introduce into model checking for reactive software and 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 aim at the modeling and analysis of an industrial case-study.

It is the goal of the course to enable students to understand and assess the efficiency and practical applicability of model checking technology. It is a further goal to illustrate to students that model checking is implemented in tools, and that these can be applied to practical, industrial-strength case studies. This will enable them to decide about an adequat use of model checking technology when conducting their own software and systems development projects, or to pursue further research in this area.

Final written examination (90 mins) or oral examination (30 mins.) Participants achieving at least 80% of the marks that can be obtained in the assignments will earn a 0.3 point grade bonus.

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 literarture will be announced during the course.

Further literature will be announced during the course.

Credits

SWS: 4+2
ECTS-points: 10