Model checking is an automatic method of verifying a formal system, most often derived from the hardware or software of a computer system. The system is described by a model, which must satisfy a formal specification described by a formula, often written in some variety of temporal logic.
The model is usually expressed as a system of transitions, that is, a directed graph, consisting of a set of vertices and arcs. A set of atomic propositions is associated with each node. Thus, nodes represent the possible states of a system, the arcs possible evolutions of the same, by means of permitted executions, that alter the state, whereas the propositions represent the basic properties that are satisfied at each point of execution. >
Formally, the problem is represented as follows: Given a desired property, expressed as a formula in temporal logic p, and a model M with an initial state s; decide if M , s & # x22A8; p {\displaystyle M,s\models p} .
There are automatic tools to perform Model checking, based on combinatorial techniques, exploring the space of possible states; which leads to the problem of state explosion. To avoid this, several researchers have developed techniques based on symbolic algorithms, abstraction, partial order reduction and model checking on the fly. Initially, tools were designed to work with discrete systems, but have been extended to real-time systems or hybrid systems.
The inventors of the method, Edmund M. Clarke, E. Allen Emerson and Joseph Sifakis, received the 2007 ACM Turing Award in recognition of their fundamental contribution to the field of computer science.
wiki