Model checking
Model checking is a method to algorithmically verify finite state systems formally. This is achieved by verifying if the model, often deriving from a hardware or software design, satisfies a logical specification. The specification is often written as temporal logic formulas. 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 executionss which alters the state, while the atomic propositions represent the basic properties that hold at a point of execution. The problem can be expressed mathematically as: given a temporal logic formula p and a model M with initial state s, decide if :.
See also Related techniques abstract interpretationAutomated theorem proving
Research groups Model Checking at CMUSAnToS Laboratory at K-State
Model checking tools Alloy languageBLAST (Berkeley Lazy Abstraction Software Verification Tool)BogorBOOP ToolkitHOL theorem proverJava PathfinderMOPEDProBProbabilistic Symbolic Model CheckerProofPowerPROSPERRabbitRAVEN (Real-Time Analysis and Verification Environment)SALSLAM projectSMVSpinUPPAAL
References 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
|
|
