You are here: irt.org | FOLDOC | 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 » modeling language » modelling
FOLDOC, Topics, A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z, ?, ALL