TY - THES
AU - Hazelhurst, Scott
PY - 1996
TI - Compositional model checking of partially ordered state spaces
KW - Thesis/Dissertation
LA - eng
M3 - Text
AB - 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 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.
N2 - 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 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.
UR - https://open.library.ubc.ca/collections/831/items/1.0051407
ER - End of Reference