Techniques for formal verification of concurrent and distributed program traces

Traditional approaches for eliminating errors in concurrent and distributed programs include formal methods and testing. This dissertation presents an approach toward combining formal methods and testing, while avoiding the complexity of model checking or theorem proving and the pitfalls of ad hoc testing. Our technique enables efficient formal verification of specifications on execution traces of actual scalable systems. By allowing an observer to analyze a partial order trace rather than a total order trace, we get the benefit of properly dealing with concurrent events and especially of detecting errors from analyzing successful executions, errors which can occur under a different thread scheduling. Surprisingly, temporal logic model checking even on a finite partial order trace is NP-complete in the size of the trace description. We develop techniques to combat the state explosion problem. Our algorithms have polynomial-time complexity in the size of the trace description as opposed to exponential. We suggest the use of an abstraction technique called slicing. Intuitively, the “slice” of a trace with respect to a predicate (specification) is a sub-trace that contains all the global states of the trace that satisfy the predicate such that it is computed efficiently (without traversing the state space) and represented concisely (without explicit representation of individual states). We present off-line and on-line slicing algorithms with respect to predicates in a subset of temporal logic CTL. We also show that the slicing problem is equivalent to the problem of detecting whether there exists at least one global state of the trace that satisfies the predicate. We develop efficient algorithms to detect several useful classes of predicates. In particular, we show how to use the slicing algorithms to detect predicates in a subset of temporal logic CTL. We also present efficient detection algorithms for predicates that do not allow efficient slicing. We have developed a prototype system Partial Order Trace Analyzer (POTA), which implements our algorithms. We verify several scalable and industrial protocols including CORBA’s GIOP, ISO’s ATMR, cache coherence and mutual exclusion. Our experimental results indicate that slicing can lead to exponential reduction over existing techniques both in time and space.