| Summary: | 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
|
|---|
