Model checking

Overview[edit]

Property checking is used for verification when two descriptions are not equivalent. During refinement, the specification is complemented with details that are unnecessary in the higher-level specification. There is no need to verify the newly introduced properties against the original specification since this is not possible. Therefore, the strict bi-directional equivalence check is relaxed to a one-way property check. The implementation or design is regarded as a model of the system, whereas the specifications are properties that the model must satisfy.^[2]


An important class of model-checking methods has been developed for checking models of hardware and software designs where the specification is given by a temporal logic formula. Pioneering work in temporal logic specification was done by Amir Pnueli, who received the 1996 Turing award for "seminal work introducing temporal logic into computing science".^[3] Model checking began with the pioneering work of E. M. Clarke, E. A. Emerson,^[4][5][6] by J. P. Queille, and J. Sifakis.^[7] Clarke, Emerson, and Sifakis shared the 2007 Turing Award for their seminal work founding and developing the field of model checking.^[8][9]


Model checking is most often applied to hardware designs. For software, because of undecidability (see computability theory) the approach cannot be fully algorithmic, apply to all systems, and always give an answer; in the general case, it may fail to prove or disprove a given property. In embedded-systems hardware, it is possible to validate a specification delivered, e.g., by means of UML activity diagrams^[10] or control-interpreted Petri nets.^[11]


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 that 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 ${\displaystyle p}$, and a structure ${\displaystyle M}$ with initial state ${\displaystyle s}$, decide if ${\displaystyle M,s\models p}$. If ${\displaystyle M}$ is finite, as it is in hardware, model checking reduces to a graph search.

Here is a list of significant model-checking tools: