A simple proof checker for real-time systems
This thesis presents a practical approach to verifying real-time properties of V L S I designs. A simple proof checker with built-in decision procedures for linear programming and predicate calculus offers a pragmatic approach to verifying real-time systems in return for a slight loss of formal r...
Main Author: | |
---|---|
Format: | Others |
Language: | English |
Published: |
2009
|
Online Access: | http://hdl.handle.net/2429/3826 |
id |
ndltd-UBC-oai-circle.library.ubc.ca-2429-3826 |
---|---|
record_format |
oai_dc |
spelling |
ndltd-UBC-oai-circle.library.ubc.ca-2429-38262018-01-05T17:31:39Z A simple proof checker for real-time systems Leung, Catherine This thesis presents a practical approach to verifying real-time properties of V L S I designs. A simple proof checker with built-in decision procedures for linear programming and predicate calculus offers a pragmatic approach to verifying real-time systems in return for a slight loss of formal rigor when compared with traditional theorem provers. In this approach, an abstract data type represents the hypotheses, claim, and pending proof obligations at each step. A complete proof is a program that generates a proof state with the derived claim and no pending obligations. The user provides replacements for obligations and relies on the proof checker to validate the soundness of each operation. This design decision distinguishes the proof checker from traditional theorem provers, and enhances the view of "proofs as programs". This approach makes proofs robust to incremental changes, and there are few "surprises" when applying rewrite rules or decision procedures to proof obligations. A hand-written proof constructed to verify the timing correctness of a high bandwidth communication protocol was verified using this checker. Science, Faculty of Computer Science, Department of Graduate 2009-01-21T19:37:27Z 2009-01-21T19:37:27Z 1995 1995-11 Text Thesis/Dissertation http://hdl.handle.net/2429/3826 eng 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. 9136973 bytes application/pdf |
collection |
NDLTD |
language |
English |
format |
Others
|
sources |
NDLTD |
description |
This thesis presents a practical approach to verifying real-time properties of V L S I designs.
A simple proof checker with built-in decision procedures for linear programming and
predicate calculus offers a pragmatic approach to verifying real-time systems in return
for a slight loss of formal rigor when compared with traditional theorem provers. In this
approach, an abstract data type represents the hypotheses, claim, and pending proof
obligations at each step. A complete proof is a program that generates a proof state
with the derived claim and no pending obligations. The user provides replacements for
obligations and relies on the proof checker to validate the soundness of each operation.
This design decision distinguishes the proof checker from traditional theorem provers,
and enhances the view of "proofs as programs". This approach makes proofs robust
to incremental changes, and there are few "surprises" when applying rewrite rules or
decision procedures to proof obligations. A hand-written proof constructed to verify the
timing correctness of a high bandwidth communication protocol was verified using this
checker. === Science, Faculty of === Computer Science, Department of === Graduate |
author |
Leung, Catherine |
spellingShingle |
Leung, Catherine A simple proof checker for real-time systems |
author_facet |
Leung, Catherine |
author_sort |
Leung, Catherine |
title |
A simple proof checker for real-time systems |
title_short |
A simple proof checker for real-time systems |
title_full |
A simple proof checker for real-time systems |
title_fullStr |
A simple proof checker for real-time systems |
title_full_unstemmed |
A simple proof checker for real-time systems |
title_sort |
simple proof checker for real-time systems |
publishDate |
2009 |
url |
http://hdl.handle.net/2429/3826 |
work_keys_str_mv |
AT leungcatherine asimpleproofcheckerforrealtimesystems AT leungcatherine simpleproofcheckerforrealtimesystems |
_version_ |
1718586608723165184 |