Model checking
Encyclopedia : M : MO : MOD : Model checking
Model checking is a method to algorithmically verify formal systems. This is achieved by verifying if the model, often deriving from a hardware or software design, satisfies a formal specification. The specification is often written as temporal logic formulas.
The model is usually expressed as a 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 represent states of a system, the edges represent possible transitions which may alter the state, while the atomic propositions represent the basic properties that hold at a point of execution.
Formally, the problem can be stated as follows: given a desired property, expressed as a temporal logic formula p, and a model M with initial state s, decide if [M,s \models p].
Model checking tools face a combinatorial blow up of the state-space, commonly known as the state explosion problem, that must be addressed to solve most real-world problems. Researchers have developed symbolic algorithms, partial order reduction, binary decision diagrams (BDDs), abstraction and on the fly model checking in order to cope with this problem. These tools were initially developed to reason about the logical correctness of discrete state systems, but have since been extended to deal with real-time and limited forms of hybrid systems.
See also
Articles
- [An Introduction to Model Checking] at embedded.com
Related techniques
Research groups
- [Software Design Group at MIT]
- [Model Checking at Carnegie Mellon University]
- [Software Verification and Validation at UT Austin]
- [SAnToS Laboratory at K-State]
- [Automated Software Engineering at Nasa Ames Research Center]
- [NASA/JPL Laboratory for Reliable Software]
- [VLSI/CAD Research group - University of Colorado at Boulder]
- [Verification and Validation - Brigham Young University, Provo, Utah]
- [ParaDiSe Laboratory - Masaryk University in Brno]
- [VASY Research team - INRIA Rhône-Alpes, France]
Model checking tools
- [Alloy language]
- [APMC]
- BLAST (Berkeley Lazy Abstraction Software Verification Tool)
- [LoTREC]
- [Bogor]
- BOOP Toolkit
- Cadena
- Cadence SMV
- [CADP]
- [CBMC], a bounded Model Checker for C/C++ programs
- CHIC
- COSPAN
- Coverity
- [GEAR], a game based model checking tool capable of CTL, modal μ-calculus and [specification patterns].
- HOL theorem prover
- [Java Pathfinder]
- [LTSA]
- [MOPED]
- [MOPS], Modelchecking Programs for Security properties
- [NuSMV: a new symbolic model checker]
- [ProB]
- Probabilistic Symbolic Model Checker
- ProofPower
- PROSPER
- Rabbit
- [RAVEN (Real-Time Analysis and Verification Environment)]
- [RuleBase]
- [SATABS], predicate abstraction for C/C++ programs
- SAL
- SLAM project
- [Symbolic Model Checker (SMV)]
- Spin
- UPPAAL
- [Verification Interacting with Synthesis (VIS)]
References
- [and SPIN: What do they promise?], Venkatesh Vinayakarao, 2006.
- [Automatic verification of finite state concurrent systems using temporal logic], E.M. Clarke, E.A. Emerson, and A.P. Sistla, ACM Trans. on Programming Languages and Systems, 8(2), pp. 244–263, 1986.
- [Concurrency theory, calculi and automata for modelling untimed and timed concurrent systems], H. Bowman and R.S. Gomez. Springer, January 2006.
- This article was originally based on material from the Free On-line Dictionary of Computing, which is [Foldoc licenselicensed] under the GFDL.
From Wikipedia, the Free Encyclopedia. Original article here. Support Wikipedia by contributing or donating.
All text is available under the terms of the GNU Free Documentation License See Wikipedia Copyrights for details.