Model checking

Model checking is a method to test system descriptions automatically and systematically whether they satisfy their specified properties. This includes safety properties (nothing bad ever happens) and liveness properties (something good will eventually happen). More importantly, a model checker computes counter examples if a property does not hold, making it a powerful tool for debugging.
Model checking is used in diverse areas: model checkers analyse chip designs for correctness (to avoid bugs like Intel's FDIV bug and F00F bug). A model checker was used to prove that the software of the Mars Pathfinder software is free of deadlocks. Modules of the Deep Space 1 space craft have been analysed with model checkers. On earth, model checkers have been used to verify properties of Delta Works' storm surge barriers.
Model checking is superior to simulation due to its systematic and exhaustive way of working. Engineers at IBM found that of the 24% of the design errors found by model checking about 40% could never have been found by testing and simulation.
This course has three important themes: The theoretical background of model checking will be presented during the lecture. We will also look an modelling problems and discuss the limits and strengths of model checking. The tutorial will consist of handson exercises to familiarise participants with using model checkers. Finally, students shall model a problem independently and analyse the model using a model checker.
Topics include

Differrences between modelling and programming

Modelling reactive systems with SPIN and Promela

Specification of properties using temporal logics

Automata theoretic models of systems and specifications and their decision procedures

Symbolic model checking using NuSMV and binary decision diagrams

Timed automata and realtime systems

Model checking of times automata with Uppaal

Methods of model abstraction and the preservation of properties across abstractions

(19548)
Typ  Vorlesung 

Dozent/in  Prof. Dr. Marcel Kyas 
Institution  Institute of Computer Science Freie Universität Berlin 
Semester  WS 09/10 
Veranstaltungsumfang  
Zeit  Office Hours: Thursday 1415
Time: Thursday, 1618 (lecture), Monday 1618 (tutorial) 
Zielgruppe
Voraussetzungen
ALPIV
A course in logic and basic automata theory is highly recommended, but not required.
Literaturliste
Text books for this course
 Christel Baier und JoostPieter Katoen, Principles of Model Checking, The MIT Press, 2008
 Mordechai Ben Ari, Principles of the SPIN Model Checker, Springer Verlag, 2008
 Gerard Holzmann, The SPIN Model Checker, AddisonWesley, 2004
 Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, Model Checking, MIT Press, 1999
Lecturer's Assistance
If you encounter problems regarding your tutor, assignments, etc, please contact Marcel Kyas.
Tutorials
 First tutorial: 21.10.09
Course Material
 Course notes will be made available at Ms Bahe's office during this term.
 Slides (everything I typed as of 10.02.2010, with reorderings)
Reader
 Divide, Abstract, and Model Check.
 A methodology for hardware verification using compositional model checking
 Verifying Properties of Large Sets of Processes with Network Invariants
 A Structural Induction Theorem for Processes
 An Undecidable Problem for Timed Automata
Project Material
 Waitfree and lockfree algorithms
 Realtime protocols
 Synchronisation
Assignments
Participants are expected to work on biweekly assignments, which ought to be turned in by groups of two students.
In addition, there will be a large practical assignment, where students are expected to build a model of a more complex case study and use model checking to verify some properties. This assignment will be handed out during the fourth week of the term. A report on that assignment should be handed in four weeks after the end of lecturing, together with all models and specifications. You can work in groups of two on that assignment.
Assignments can only be downloaded from the network of FUBerlin (e.g., via VPN)
 1st Assignment due 21.10.2009
 2nd Assignment, due 28.10.2009
 3rd Assignment, due 11.11.2009
 4th Assignment, due 18.11.2009
 5th Assignment, due 27.11.2009
 6th Assignment, due 4.12.2009
 7th Assignment, due 18.12.2009
 8th Assignment, due 20.01.2010
 9th Assignment, due 29.01.2010
 10th Assignment, due 10.02.2010
Examination
Oral examinations by appointment.
Criteria for successful participation

Active participation in the tutorials is essential!
 At least n2 times present

Handin your assignments on time
 Teamwork is required, 23 students in a team, preferrably 2.

Successful submission of at least n2 assignments
 At least 50% of the score on each assignment.

Each student must be able to present the assignment during the tutorials
 Each student must have presented in the tutorials at least once
 Submission of the large practical assignment.
 At least 50% of the max. number of points required in the exam
 The final grade is based on the exam, only.
Text books for this course
 Christel Baier und JoostPieter Katoen, Principles of Model Checking, The MIT Press, 2008
 Mordechai Ben Ari, Principles of the SPIN Model Checker, Springer Verlag, 2008
 Gerard Holzmann, The SPIN Model Checker, AddisonWesley, 2004
 Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, Model Checking, MIT Press, 1999
Model checkers presented during the course
 The SPIN model checker
 The NuSMV model checker
 The UPPAAL mode checker