- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- UBC Theses and Dissertations /
- Leveraging distributed explicit-state model checking...
Open Collections
UBC Theses and Dissertations
UBC Theses and Dissertations
Leveraging distributed explicit-state model checking for practical verification of liveness in hardware protocols Bingham, Brad
Abstract
Protocol verification is a key component to hardware and software design. The proliferation of concurrency in modern designs stresses the need for accurate protocol models and scalable verification tools. Model checking is an approach for automatically verifying properties of designs, the main limitation of which is state-space explosion. As such, automatic verification of these designs can quickly exhaust the memory of a single computer. This thesis presents PReach, a distributed explicit-state model checker, designed to robustly harness the aggregate computing power of large clusters. The initial version verified safety properties, which hold if no error states can be reached. PReach has been demonstrated to run on hundreds of machines and explore state space sizes up to 90 billion, the largest published to date. Liveness is an important class of properties for hardware system correctness which, unlike safety, expresses more elaborate temporal reasoning. However, model checking of liveness is more computationally complex, and exacerbates scalability issues as compared with safety. The main thesis contribution is the extension of PReach to verify two key liveness-like properties of practical interest: deadlock-freedom and response. Our methods leverage the scalability and robustness of PReach and strike a balance between tractable verification for large models and catching liveness violations. Deadlock-freedom holds if from all reachable system states, there exists a sequence of actions that will complete all pending transactions. We find that checking this property is only a small overhead as compared to safety checking. We also provide a technique for establishing that deadlock-freedom holds of a parameterized system -- a system with a variable number of entities. Response is a stronger property than deadlock-freedom and is the most common liveness property of interest. In practical cases, fairness must be imposed on system models when model checking response to exclude those execution traces deemed inconsistent with the expected underlying hardware. We implemented a novel twist on established model checking algorithms, to target response properties with action-based fairness. This implementation vastly out-performs competing tools. This thesis shows that tractable verification of interesting liveness properties in large protocol models is possible.
Item Metadata
Title |
Leveraging distributed explicit-state model checking for practical verification of liveness in hardware protocols
|
Creator | |
Publisher |
University of British Columbia
|
Date Issued |
2015
|
Description |
Protocol verification is a key component to hardware and software design.
The proliferation of concurrency in modern designs stresses the need for
accurate protocol models and scalable verification tools.
Model checking is an approach for automatically verifying properties
of designs, the main limitation of which is state-space explosion.
As such, automatic verification of these designs can quickly exhaust
the memory of a single computer.
This thesis presents PReach, a distributed explicit-state model checker,
designed to robustly harness the aggregate computing power of large clusters.
The initial version verified
safety properties, which hold if no error states can be reached.
PReach has been demonstrated to run on hundreds of machines and explore state
space sizes up to 90 billion, the largest published to date.
Liveness is an important class of properties for hardware system correctness
which, unlike safety, expresses more elaborate temporal reasoning.
However, model checking of liveness is more computationally complex,
and exacerbates scalability issues as compared with safety.
The main thesis contribution is the extension of PReach to verify two key liveness-like properties of practical interest:
deadlock-freedom and response.
Our methods leverage the scalability and robustness of PReach and strike a balance between tractable verification for large models
and catching liveness violations.
Deadlock-freedom holds if from all reachable system states, there exists
a sequence of actions that will complete all pending transactions.
We find that checking this property
is only a small overhead as compared to safety checking.
We also provide a technique for establishing that deadlock-freedom holds of
a parameterized system --
a system with a variable number of entities.
Response is a stronger property than deadlock-freedom and is
the most common liveness property of interest.
In practical cases, fairness must be imposed on system models
when model checking response
to exclude those execution traces deemed inconsistent with the expected
underlying hardware.
We implemented a novel twist on established model checking algorithms,
to target response properties with action-based fairness.
This implementation vastly out-performs competing tools.
This thesis shows that tractable verification of interesting liveness properties
in large protocol models is possible.
|
Genre | |
Type | |
Language |
eng
|
Date Available |
2015-04-09
|
Provider |
Vancouver : University of British Columbia Library
|
Rights |
Attribution-NonCommercial-NoDerivs 2.5 Canada
|
DOI |
10.14288/1.0166129
|
URI | |
Degree | |
Program | |
Affiliation | |
Degree Grantor |
University of British Columbia
|
Graduation Date |
2015-05
|
Campus | |
Scholarly Level |
Graduate
|
Rights URI | |
Aggregated Source Repository |
DSpace
|
Item Media
Item Citations and Data
Rights
Attribution-NonCommercial-NoDerivs 2.5 Canada