Model checking

From Free net encyclopedia

Model checking is a method to algorithmically verify formal 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.

The model is usually expressed as a transition system, i.e directed graph consisting of nodes (or vertices) and edges. A set of atomic propositions is associated with each node. The nodes represent states of a system, the edges represent possible executions which alters the state, while the atomic propositions represent the basic properties that hold at a point of execution.

Formally, the problem can be stated as follows: given a desired property, expressed as a temporal logic formula p, and a model M with initial state s, decide if <math>M,s \models p</math>.

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