GLOBAN 2006 - The Global Computing Approach to Analysis of Systems

Model checking

Lectures by Kim Guldstrand Larsen, University of Aalborg, Denmark

Abstract

Model checking is a method to algorithmically verify the correctness of systems. This is achieved by verifying if the model, often deriving from a hardware or software design, satisfies a formal specification. The specification is often written as temporal logic formulas.

Model checking tools face a combinatorial blow-up of the state-space, commonly known as the state explosion problem. To cope with this problem methods have been developed for symbolic representation and exploration of state-spaces, partial order reduction, abstraction and on-the-fly model checking. These methods were initially developed to reason about the logical correctness of discrete state systems, but have since been extended to deal with real-time, limited forms of hybrid systems and stochastic behaviour.

The lectures aim at covering the model checking techniques for analysing discrete state and real-time systems as found in the tools visualSTATE and UPPAAL. Also, the model checking capabilities of HyTech (hybrid behaviour), RAPTURE and PRISM (stochastic behaviour) will be outlined.