Model checking is the process of checking whether a given model satisfies a given logical formula. The concept is general and applies to all kinds of logics and their models. A simple model-checking problem is testing whether a given formula in the propositional logic is satisfied by a given model.An important class of model checking methods have been developed to
algorithmically verify formal
systems. This is achieved by verifying if the model, often derived from a
hardware or
software design, satisfies a
formal specification, typically a
temporal logic formula. Pioneering work in the model checking of temporal logic formulae was done by E. M. Clarke and E. A. Emerson in 1981 and by J. P. Queille and J. Sifakis in 1982.
See more at Wikipedia.org...
<
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)
Free Download Now!
