Gavin Lowe and Hussein Zedan
February 1995, 32pp.
We describe the Temporal Agent Model (TAM) together with its associated refinement calculus. The calculus is based on a wide-spectrum language within which functional and temporal properties can be expressed in either abstract (ie specification) or concrete (ie design) terms. The refinement process transforms abstract specifications to concrete designs through successive applications of sound refinement laws. An extension to the calculus allows us to calculate a scheduler for the resulting design. We present a specification paradigm based on splitting the functional and temporal requirements, and describe refinement techniques based on this paradigm. We illustrate the calculus via an example taken from the avionics industry.