|
|
|---|
|
|
|
|---|
M. M. Wilding, Machine-checked real-time system verification
Relevance: a non-trivial applications program on the CLI Verified Stack
In the introduction to this dissertation, the author writes:
“The complexity and importance of real-time systems makes their formalization and verification crucial. We ensure proper real-time system behavior in several ways through mathematical proof. We check proofs using Nqthm, a mechanical proof system also known as the Boyer-Moore theorem prover.
...
We verify a high-level language application that, using a proved compiler and microprocessor design, assures the optimality and timely behavior of an application. The verified program uses a clever algorithm to meet its specification and a method for structuring proofs allows large verified programs to be developed. An interpreter-based language semantics allows reliable execution behavior reasoning, including reasoning about timing.”
The dissertation deals with several programs written in the Piton assembly language (bib::moore96) for the FM9001 (bib::hb92). In addition to establishing functional correctness, the proofs ensure that the Piton images fit in the space provided by the fabricated FM9001, provide upper bounds on the instruction counts, and the sizes of both the control stack and the temporary stack implemented by Piton on the FM9001. See also bib::wilding93 for a discussion of one of these programs, namely one that implements a winning strategy for the game of Nim.
See the Nqthm scripts by downloading and extracting the