Dictionary De - En
De - Es
De - Pt| English Dictionary: Model Checking | by the DICT Development Group |
| 1 result for Model Checking | |
| From The Free On-line Dictionary of Computing (15Feb98) [foldoc]: | |
|
model checking 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) | |
