Model checking
Model checking is a software technology consisting in algorithmically checking whether a model (often deriving from a hardware or software design) satisfies a logical specification.
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.
A specification language, usually some kind of temporal logic, is used to express properties.
The problem can be expressed mathematically as: given a temporal logic formula p and a model M with initial state s, decide if :.
References
- Automatic verification of finite state concurrent systems using temporal logic, E.M. Clarke, E.A. Emerson, and A.P. Sisla, ACM Trans. on Programming Languages and Systems, 8(2), pp. 244--263, 1986
- Model Checking, Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, MIT Press, 1999
This article (or an earlier version of it) contains material from FOLDOC, used with permission. Modify if needed.