Model Checking

This course gives an introduction to model-checking, a technique for automatic verification of software and reactive, embedded systems. Model checking was invented long time ago, and has been used successfully in many industrial projects. Considerable research in this topic is still in progress. This course gives the basic elements required for understanding model checking, and the basic skills for using model checking tools. It also provides the basic knowledge for researchers to start doing research in this topic.

The course includes a practical component based on the SPIN model checker as well as the theoretical background.

No special knowledge is required except for a computer science background.

The course lasts 3 days, i.e. 6 x 3-hour sessions.

Course Contents

  1. Introduction
    • System Verification
    • Definition of Model Checking
    • Model Checking versus Theorem Proving, Debugging
  2. System Modelling with Automata
    • Introductory Examples
    • Automata: Definitions
    • Synchronized Products
    • Synchronization by Message Passing and Shared Variables
    • Automata Model for Peterson's Algorithm
  3. System Properties Specification with Temporal Logics
    • The Language of Temporal Logic
    • The Formal Syntax of Temporal Logic
    • The Semantic of Temporal Logic
    • PLTL and CTL
    • The Proof System for PLTL
    • The Expressiveness of CTL*
  4. Model Checking Algorithms
    • Model Checking CTL
    • Model Checking PLTL
    • The State Explosion Problem
  5. Symbolic Model Checking
    • What is symbolic model checking
    • Symbolic Computation of State Sets
    • Symbolic Representation of Sets
    • Binary Decision Diagrams (BDD)
    • Representing Automata by BDDs
    • BDD-based Modelchecking
  6. Abstraction Methods
    • Why is Model Abstraction Required
    • Abstraction by State Merging
    • What Can Be Proved in the Abstract Automaton
    • Abstraction on the Variables
    • Abstraction by Restriction
    • Observer Automata
  7. SPIN Model Checker
    • What Can We Do with SPIN
    • SPIN's Essentials
    • PROMELA Language
    • Describing Processes with PROMELA
    • Simulating the System
    • Verification of Assertions
    • Verification of PLTL formulas
    • Case Studies
    • Documentation

 

References

  1. Edmund M. Clarke, Jr., Orna Grumberg, and Doron A. Peled.Model Checking, The MIT Press, 1999, Fourth Printing 2002.
  2. Michael Huth and Mark Ryan. Logic in Computer Science: Modelling and Reasoning about Systems, Second Edition, Cambridge University Press, 2004.
  3. B. Bérard et al.. Systems and Software Verification, Modelchecking Techniques and Tools, Springer-Verlag, 2001.
  4. Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, 1993.
  5. Doron A. Peled. Software Reliability Methods, Texts in Computer Science (Foreword by Edmund M. Clarke). Springer-Verlag, 2001.
  6. Gerard J. Holzmann, The SPIN Model Checker, 2004, Lucent Technology Inc, Bell Laboratories.