AG Technische Informatik

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 hands-on 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 real-time systems

  • Model checking of times automata with Uppaal

  • Methods of model abstraction and the preservation of properties across abstractions

(19612)

Typ

Vorlesung

Dozent/in

Prof. Dr. Marcel Kyas

Institution

Institute of Computer Science

Freie Universität Berlin

Semester

WS 10/11

Veranstaltungsumfang

Zeit

 Office Hours: Thursday 14-15

 Time: Thursday, 16-18 (lecture), Monday 16-18 (tutorial)

Zielgruppe

Master students, diploma students, and 3rd year Bachelor students

Voraussetzungen

ALPIV

A course in logic and basic automata theory is highly recommended, but not required.

Literaturliste

Text books for this course

 Location: SR006
ECTS-credits:
8

 

KVV page

Lecturer's Assistance

If you encounter problems regarding your tutor, assignments, etc,  please contact Marcel Kyas.

Tutorials

  • First tutorial: 25.10.09

Course Material

Examination

Written exam on 17.2.2011.

 

Criteria for successful participation

  • Active participation in the tutorials is essential!
    • At least n-2 times present
  • Hand-in your obligatory assignments on time
    • Teamwork is required, 2-3 students in a team, preferrably 2.
  • Successful submission of all but one obligatory assignment
    • At least 50% of the score on each assignment.
  • There will be a small written test at the beginning of most tutorials, selected from a range og assignments
    • You must pass n - 2 tests.  
  • Submission of the project and project report
    • The project topic will be selected during lecture
    • Your are expected to work for about 3 weeks on the project
    • The project model and report will be graded
  • At least 50% of the max. number of points required to pass the exam
  • The final grade is based on the exam (5/8) and the project (3/8).

Model checkers presented during the course