model checking

theory, algorithm, testing To algorithmically check whether

a program (the model) satisfies a specification.

The model is usually expressed as a directed graph

consisting of nodes (or vertices) and edges. A set of

atomic propositions is associated with each node. The nodes

represents states of a program, the edges represent possible

executions which alters the state, while the atomic

propositions represent the basic properties that hold at a

point of execution.

A specification language, usually some kind of temporallogic, is used to express properties.

The problem can be expressed mathematically as: given a

temporal logic formula p and a model M with initial state s,

decide if M,s models p.

["Automatic verification of finite state concurrent systems

using temporal logic", E.M. Clarke, E.A. Emerson, and

A.P. Sisla, ACM Trans. on Programming Languages and Systems

8(2), pp. 244--263, 1986].

(1997-06-26)