Model checking
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 :<math>M,s \models p<math>.
See also
Related Technique
Research Group
Model Checking Tools
- Alloy language
- BLAST (Berkeley Lazy Abstraction Software Verification Tool)
- Bogor
- BOOP Toolkit
- HOL
- Java Pathfinder
- MOPED
- ProofPower
- PROSPER
- SAL
- SLAM project
- SMV
- Spin
- UPPAAL
References
- , 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
