Model checking

In order to solve such a problem algorithmically, both the model of the system and its specification are formulated in some precise mathematical language.

A simple model-checking problem consists of verifying whether a formula in the propositional logic is satisfied by a given structure.

[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.

[3] Model checking began with the pioneering work of E. M. Clarke, E. A. Emerson,[4][5][6] by J. P. Queille, and J.

[7] Clarke, Emerson, and Sifakis shared the 2007 Turing Award for their seminal work founding and developing the field of model checking.

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.

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.

[12] Formally, the problem can be stated as follows: given a desired property, expressed as a temporal logic formula

When such state-space traversal is based on representations of a set of states and transition relations as logical formulas, binary decision diagrams (BDD) or other related data structures, the model-checking method is symbolic.

After the success of propositional satisfiability in solving the planning problem in artificial intelligence (see satplan) in 1996, the same approach was generalized to model checking for linear temporal logic (LTL): the planning problem corresponds to model checking for safety properties.

The authors of "Patterns in Property Specification for Finite-State Verification" translate this requirement into the following LTL formula:[15] Here,

[21] These results have been extended to the task of enumerating all solutions to a first-order formula with free variables.

Elevator control software can be model-checked to verify both safety properties, like "The cabin never moves with its door open" , [ 1 ] and liveness properties, like "Whenever the n th floor's call button is pressed, the cabin will eventually stop at the n th floor and open the door" .