Search in: Word
Vietnamese keyboard: Off
Virtual keyboard: Show
Computing (FOLDOC) dictionary
model checking
Jump to user comments
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 temporallogic, 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.