Technical Reports

The ICICS/CS Reading Room

UBC CS TR-96-02 Summary

Compositional Model Checking of Partially Ordered State Spaces, January 1996 Scott Hazelhurst, 268 pages

Symbolic trajectory evaluation (STE) --- a model checking technique based on partial order representations of state spaces --- has been shown to be an effective model checking technique for large circuit models. However, the temporal logic that it supports is restricted, and as with all verification techniques has significant performance limitations. The demand for verifying larger circuits, and the need for greater expressiveness requires that both these problems be examined.

The thesis develops a suitable logical framework for model checking partially ordered state spaces: the temporal logic \TL\ and its associated satisfaction relations, based on the quaternary logic $\Q$. \TL\ is appropriate for expressing the truth of propositions about partially ordered state spaces, and has suitable technical properties that allow STE to support a richer temporal logic. Using this framework, verification conditions called \emph{assertions} are defined, a generalised version of STE is developed, and three STE-based algorithms are proposed for investigation. Advantages of this style of proof include: models of time are incorporated; circuits can be described at a low level; and correctness properties are expressed at a relatively high level.

A primary contribution of the thesis is the development of a compositional theory for \TL\ assertions. This compositional theory is supported by the partial order representation of state space. To show the practical use of the compositional theory, two prototype verification systems were constructed, integrating theorem proving and STE. Data is manipulated efficiently by using binary decision diagrams as well as symbolic data representation methods. Simple heuristics and a flexible interface reduce the human cost of verification.

Experiments were undertaken using these prototypes, including verifying two circuits from the IFIP WG 10.5 Benchmark suite. These experiments showed that the generalised STE algorithms were effective, and that through the use of the compositional theory it is possible to verify very large circuits completely, including detailed timing properties.

If you have any questions or comments regarding this page please send mail to