Sciweavers

TABLEAUX
1998
Springer

Model Checking: Historical Perspective and Example (Extended Abstract)

13 years 7 months ago
Model Checking: Historical Perspective and Example (Extended Abstract)
ple (Extended Abstract) Edmund M. Clarke and Sergey Berezin Carnegie Mellon University -- USA Model checking is an automatic verification technique for finite state concurrent systems such as sequential circuit designs and communication protocols. Specifications are expressed in propositional temporal logic. An exhaustive search of the global state transition graph or system model is used to determine if the specification is true or not. If the specification is not satisfied, a counterexample execution trace is generated if possible. By encoding the model using Binary Decision Diagrams (BDDs) it is possible to search extremely large state spaces with as many as 10120 reachable states. In this paper we describe the theory underlying this technique and outline its historical development. We demonstrate the power of model checking to find subtle errors by verifying the Space Shuttle Three-Engines-Out Contingency Guidance Protocol.
Edmund M. Clarke, Sergey Berezin
Added 06 Aug 2010
Updated 06 Aug 2010
Type Conference
Year 1998
Where TABLEAUX
Authors Edmund M. Clarke, Sergey Berezin
Comments (0)