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

• abstract interpretation
• Automated theorem proving

Research groups

• Model Checking at CMU
• SAnToS Laboratory at K-State

Model checking tools

• Alloy language
• BLAST (Berkeley Lazy Abstraction Software Verification Tool)
• Bogor
• BOOP Toolkit
• HOL theorem prover
• Java Pathfinder
• MOPED
• ProB
• Probabilistic Symbolic Model Checker
• ProofPower
• PROSPER
• Rabbit
• RAVEN (Real-Time Analysis and Verification Environment)
• SAL
• SLAM project
• SMV
• Spin
• UPPAAL

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

External links

• Citations from CiteSeer