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 temporal logic, 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)
Nearby terms:
MODEF « MODEL « model « model checking »
modeling » modelling » Modelsim
|
