Main Page | See live article | Alphabetical index 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 abstract interpretation 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. This article is from Wikipedia. All text is available under the terms of the GNU Free Documentation License.