Temporal Logic Model Checking

Edmund M. Clarke
School of Computer Science
Carnegie Mellon University

Logical errors in finite state reactive systems are an important problem for designers. They can delay getting a new product on the market or cause the failure of some critical device that is already in use. My research group has developed a verification method called temporal logic model checking for this class of systems. In this approach specifications are expressed in a propositional temporal logic, and reactive systems are modeled as state-transition graphs. An efficient search procedure is used to determine automatically if the specifications are satisfied by the state-transition graph. The technique has been used in the past to find subtle errors in a number of non-trivial circuit and protocol designs.

During the last few years, the size of the reactive systems that can be verified by model checking techniques has increased dramatically. By representing sets of states and transition relations implicitly using Binary Decision Diagrams (BDDs), we are now able to check examples that are many orders of magnitude larger than was previously the case. In this lecture we describe how the BDD-based model checking techniques work and illustrate their power by verifying the Space Shuttle Contingency Guidance Protocol. This protocol specifies what happens when the shuttle has to abort its flight during take-off.

11 Aug 1997, Ulf Nilsson