Right on Time: Pre-verified Software Components for Construction of Real-Time Systems
We present a method that makes use of the theorem prover PVS to specify,
develop and verify real-time software components for embedded control
systems software with periodic tasks. The method is based on an intuitive
discrete time "Clocks" theory by Dutertre and Stavridou that models periodic
timed trajectories representing dataflows. We illustrate the method by
considering a Held_For operator on dataflows that is used to specify real-time
requirements. Recursive functions using the PVS TABLE construct are used to
model both the system requirements and the design. A software component is
designed to implement the Held_For operator and then verified in PVS. This
pre-verified component is then used to guide design of more complex
components and decompose their design verification into simple inductive
proofs. Finally, we demonstrate how the rewriting and propositional
simplification capabilities of PVS can be used to refine a component based
implementation to improve the performance while still guaranteeing correctness.
An industrial control subsystem design problem is used to illustrate the process.