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.

• Type: Conference
• Year: 1998
• Where: TABLEAUX
• Authors: Edmund M. Clarke, Sergey Berezin
• Keywords: Artificial Intelligence, Model Checking, Sergey Berezin Carnegie, TABLEAUX 1998, USA Model Checking