Model checking is a method to algorithmically verify finite state systems formally. This is achieved by verifying if the model, often deriving from a hardware or software design, satisfies a logical specification. The specification is often written as temporal logic formulas.
The model is usually expressed as a directed graph consisting of nodes (or vertices) and edges.
A set of atomic propositions is associated with each node.
The nodes represents states of a program, the edges represent possible executions which alters the state, while the atomic propositions represent the basic properties that hold at a point of execution.
The problem can be expressed mathematically as: given a temporal logic formula p and a model M with initial state s, decide if :
.
See also
Related techniques
Research groups
Model checking tools
References
- Model Checking, Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, MIT Press, 1999
External links