- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- UBC Theses and Dissertations /
- Compositional model checking of partially ordered state...
Open Collections
UBC Theses and Dissertations
UBC Theses and Dissertations
Compositional model checking of partially ordered state spaces Hazelhurst, Scott
Abstract
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.
Item Metadata
Title |
Compositional model checking of partially ordered state spaces
|
Creator | |
Publisher |
University of British Columbia
|
Date Issued |
1996
|
Description |
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.
|
Extent |
10445169 bytes
|
Genre | |
Type | |
File Format |
application/pdf
|
Language |
eng
|
Date Available |
2009-02-20
|
Provider |
Vancouver : University of British Columbia Library
|
Rights |
For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.
|
DOI |
10.14288/1.0051407
|
URI | |
Degree | |
Program | |
Affiliation | |
Degree Grantor |
University of British Columbia
|
Graduation Date |
1996-05
|
Campus | |
Scholarly Level |
Graduate
|
Aggregated Source Repository |
DSpace
|
Item Media
Item Citations and Data
Rights
For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use.