Guide for the Use of the Ada Ravenscar Profile in High Integrity Systems (Part 2)

摘要

Chapter 1 described the motivation for the Ravenscar Profile in terms of the need to verify the temporal behaviour of concurrent real-time programs. In this chapter, we provide an introduction to the forms of verification that can applied to Ravenscar applications, to deliver dependable systems. The approach to verification in the presence of Ada tasking is similar in many ways to that traditionally used for cyclic executives. Each thread of control is independently verified for conformance with its precise/formal specification, for example by performing requirements-based testing or by use of static analysis tools on its sequential behaviour. Then, the program as a whole is verified against all its timing constraints. This latter stage differs from the cyclic executive approach in the presence of priority-based preemptive task scheduling in that it can be automated by the use of, for example, a Response Time Analysis (RTA) tool to verify that a given task set meets its deadlines. The tool-based approach greatly simplifies the process of verification of timing constraints during development, and of re-verification after the system has undergone modification during maintenance.