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 state transition system, i.e 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 system, 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>.
Model checking tools have to handle state explosion problem. There are several approaches how to coping this problem: symbolic algorithms, partial order reduction, on the fly model checking, etc.
| Contents |
See also
Related techniques
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
- Cadence SMV
- CHIC
- COSPAN
- HOL theorem prover
- Java Pathfinder (http://ase.arc.nasa.gov/jpf)
- MOPED
- NuSMV
- 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
- Verification Interacting with Synthesis (VIS)
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. Sistla, 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)
- This article was originally based on material from the Free On-line Dictionary of Computing, which is licensed under the GFDL.