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 : .
See also
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
- Alloy language
This article (or an earlier version of it) contains material from FOLDOC, used with permission. Modify if needed.
Referenced By
Formal semantics | Formal semantics of programming languages | List of mathematical topics (M-O) | Semantics of programming languages
|
