A specification-oriented semantics for the refinement of real-time systems

A refinement calculus for the development of real-time systems is presented. The calculus is based upon a wide-spectrum language called the temporal agent model (TAM), within which both functional and timing properties can be expressed in either abstract or concrete terms. A specification-oriented semantics for the language is given. Program development is considered as a refinement process, i.e. calculation of a structured program from an unstructured specification. A calculus of decomposition is defined. An example program is developed.