Model checking - Definition and Overview

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 techniques

• abstract interpretation
• Automated theorem proving

Research groups

• Model Checking at CMU (http://www-2.cs.cmu.edu/~modelcheck/)
• SAnToS Laboratory at K-State (http://www.cis.ksu.edu/santos/)

Model checking tools

• Alloy language
• BLAST (Berkeley Lazy Abstraction Software Verification Tool)
• Bogor
• BOOP Toolkit
• HOL
• Java Pathfinder (http://ase.arc.nasa.gov/jpf)
• MOPED
• ProB (http://www.ecs.soton.ac.uk/~mal/systems/prob.html)
• Probabilistic Symbolic Model Checker
• ProofPower
• PROSPER
• Rabbit
• RAVEN (Real-Time Analysis and Verification Environment) (http://www-ti.informatik.uni-tuebingen.de/~fmg/raven/raven.html)
• SAL
• SLAM project
• SMV
• Spin
• UPPAAL

References

• Automatic verification of finite state concurrent systems using temporal logic (http://doi.acm.org/10.1145/5397.5399), 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 (http://citeseer.org/cs?q=Model+checking)