資料來源 : Free On-Line Dictionary of Computing
model checking
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)