X.: Right on time: Pre-verified software components for constructuion 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.