Somesh Jha

Symmetry and Induction in Model Checking Degree Type: Ph.D. in Computer Science
Advisor(s): Edmund Clarke
Graduated: December 1996

Abstract:

With the increasing complexity of digital systems, testing of digital systems is becoming increasingly important. Perhaps, the most popular method for testing hardware is simulation. The incompleteness of simulation based testing methods has spurred the recent surge in the research on formal verification. In formal verification, one buildsa precise model of the hardware under scrutiny and proves that the model satisfies a specification of interest. For example, suppose one wants to verify that a router chip does not deadlock. In this case the user will build a precise model of the router and the specification will express the property of deadlock freedom. The two approaches to formal verification are model checking and theorem proving. In this thesis we will only discuss model checking. Most model checking procedures suffer from the state explosion problem, i.e., the size of the state space
of the system can be exponential in the number of state variables of the system. For certain systems, exploiting the inherent symmetry can alleviate the state-explosion problem. We discuss Model Checking procedures which exploit symmetry. Current model checkers can only verify a single state-transition system at a time. We also want to extend the model checking techniques to handle in nite families of nite-state systems.

In practice, finite state concurrent systems often exhibit considerable symmetry. We investigate techniques for reducing the complexity of temporal logic model checking in the presence of symmetry. In particular, we show that symmetry can frequently be used to reduce the size of the state space that must be explored during model checking. We also investigate complexity of various problems related to exploiting symmetry in model checking. Partial order based reduction techniques exploit independence of actions. We demonstrate that partial order and symmetry based reduction techniques can be applied simultaneously. The ability to reason automatically about entire families of similar state-transition systems is an important research goal. Such families arise frequently in the design of reactive systems in both hardware and software. The infinite family of token rings is a simple example. More complicated examples are trees of processes consisting of one root, several internal and leaf nodes, and hierarchical buses with different numbers of processors and caches. A technique for verifying entire families of state-transition systems based on network grammars and process invariants is presented here.

Thesis Committee:
Edmund M. Clarke (Chair)
Stephen Brookes
Daniel Jackson
Robert Kurshan (Bell Labs, Lucent)

James Morris, Head, Computer Science Department
Raj Reddy Dean, School of Computer Science

Keywords:
formal verification, temporal logic, CTL, model checking, calculus, symmetry, induction, partial order.