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.
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
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 bedownloaded from the network of FU-Berlin (e.g., via VPN)