|
|
|
|
|
Model CheckingModel 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 executions 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 Research groups Model checking tools References - Model Checking, Edmund M. Clarke, Jr., Orna Grumberg and Doron A. Peled, MIT Press, 1999
External links
|
 |
|
| Copyright 2005-2009 OnPedia.com. All Rights Reserved |
|
|