Model checking

From Wikipedia, the free encyclopedia

This article is about checking of models in computer science. For the checking of models in statistics, see statistical model validation.

Model checking is the process of checking whether a given structure is a model of a given logical formula. The concept is general and applies to all kinds of logics and suitable structures. A simple model-checking problem is testing whether a given formula in the propositional logic is satisfied by a given structure.

An important class of model checking methods have been developed to algorithmically verify formal systems. This is achieved by verifying if the structure, often derived from a hardware or software design, satisfies a formal specification, typically a temporal logic formula. Pioneering work in the model checking of temporal logic formulae was done by E. M. Clarke and E. A. Emerson in 1981 and by J. P. Queille and J. Sifakis in 1982. Clarke, Emerson, and Sifakis shared the 2007 Turing Award for their work on model checking.

Model checking is most often applied to hardware designs. For software, because of undecidability (see Computability theory) the approach cannot be fully algorithmic; typically it may fail to prove or disprove a given property.

The structure is usually given as a source code description in an industrial hardware description language or a special-purpose language. Such a program corresponds to a finite state machine (FSM), i.e., a directed graph consisting of nodes (or vertices) and edges. A set of atomic propositions is associated with each node, typically stating which memory elements are one. 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 structure M with initial state s, decide if M,s \models p. If M is finite, as it is in hardware, model checking reduces to a graph search.

[edit] Model checking tools

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. There are several approaches to combat this problem.

  1. Symbolic algorithms avoid ever building the graph for the FSM; instead, they represent the graph implicitly using a formula in propositional logic. The use of binary decision diagrams (BDDs) was made popular by the work of Ken McMillan (1992).
  2. Bounded model checking algorithms unroll the FSM for a fixed number of steps k and check whether a property violation can occur in k or fewer steps. This typically involves encoding the restricted model as an instance of SAT. The process can be repeated with larger and larger values of k until all possible violations have been ruled out (cf. Iterative deepening depth-first search).
  3. Partial order reduction can be used (on explicitly represented graphs) to reduce the number of independent interleavings of concurrent processes that need to be considered. The basic idea is that if it does not matter, for the kind of things one intends to prove, whether A or B is executed first, then it is a waste of time to consider both the AB and the BA interleavings.
  4. Abstraction attempts to prove properties on a system by first simplifying it. The simplified system usually does not satisfy exactly the same properties as the original one so that a process of refinement may be necessary. Generally, one requires the abstraction to be sound (the properties proved on the abstraction are true of the original system); however, most often, the abstraction is not complete (not all true properties of the original system are true of the abstraction). An example of abstraction is, on a program, to ignore the values of non boolean variables and to only consider boolean variables and the control flow of the program; such an abstraction, though it may appear coarse, may be in fact be sufficient to prove e.g. properties of mutual exclusion.
  5. Counter-example guided abstraction refinement (CEGAR) begins checking with a coarse (imprecise) abstraction and iteratively refines it. When a violation (counter-example) is found, the tool analyzes it for feasibility (i.e., is the violation genuine or the result of an incomplete abstraction?). If the violation is feasible, it is reported to the user; if it is not, the proof of infeasibility is used to refine the abstraction and checking begins again.

Model checking 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.

[edit] Some model checking tools

Contents
0–9 A B C D E F G H I J K L M N O P Q R S T U V W X Y Z   See also 
Tool Category Publisher(s) Specification Language

(Logic used to specify the system and properties, etc.)

 Antecendants

(What the software is based on, other seminal products, etc.)

 License

(Type of license - e.g. GPL, closed source, commercial, etc)

 Notes

(Any notes on the software)

 Link
Cadence - Incisive Formal Verifier Type Cadence [1]
SPIN Model checker for asynchronous process systems Bell Labs LTL [2]
KRONOS Timed model checker Verimag TCTL GPL [3]
0-In Formal Verification [4]
Alloy language [5]
CHESS Preemption-bounded exploration of multithreaded programs Microsoft Research Binary release is available at http://research.microsoft.com/chess/ [6]
Synopsys - Magellan [7]
APMC [8]
AcPeg - Access Control Systems verification tool through Model Checking [9]
iLock - Formal Safety Verification of Rail Control Systems [10]
BLAST - CEGAR-style model checker for C programs
LoTREC [11]
Bogor [12]
BOOP Toolkit
Cadena [13]


[edit] See also

[edit] Articles

[edit] Related techniques

[edit] Research groups

[edit] Other

[edit] References

This article was originally based on material from the Free On-line Dictionary of Computing, which is licensed under the GFDL.