A sequential real-time refinement calculus

We present a comprehensive refinement calculus for the development of seque ntial, real-time programs from real-time specifications. A specification ma y include not only execution time limits, but also requirements on the beha viour of outputs over the duration of the execution of the program. The approach allows refinement steps that separate timing constraints and f unctional requirements. New rules are provided for handling timing constrai nts, but the refinement of components implementing functional requirements is essentially the same as in the standard refinement calculus. The product of the refinement process is a program in the target programmin g language extended with timing deadline directives. The extended language is a machine-independent, real-time programming language. To provide valid machine code for a particular model of machine, the machine code produced b y a compiler must be analysed to guarantee that it meets the specified timi ng deadlines.