The complexities of real-time systems are such that it is often thought necessary to give a formal justification of their correctness, especially if they are to be used in a safety-critical environment. In this paper we describe our work on a formally based design method for real-time systems which allows the timing aspects of a concurrent system to be mathematically described and verified, as well as semi-automatically implemented. Our design language, AORTA, is a timed process algebra, with features to ensure that all designs can be implemented. A predictable real-time kernel is also described, which is used in the construction of a system from an AORTA design, and which allows the timing of the implementation to be verified.
|Publication status||Published - 1994|
|Event||RTOSS '94: 11th IEEE Workshop on Real-Time Operating Systems and Software - Seattle|
Duration: 1 Jan 1994 → …
|Conference||RTOSS '94: 11th IEEE Workshop on Real-Time Operating Systems and Software|
|Period||1/01/94 → …|