资料来源 : 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)