REFINEMENT OF COMPLEX-SYSTEMS - A CASE-STUDY

We describe the Temporal Agent Model (TAM) together with its associate d refinement calculus. The calculus is based on a wide-spectrum langua ge within which functional and temporal properties can be expressed in either abstract (i.e. specification) or concrete (i.e. 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 r esulting design. We present a specification paradigm based on splittin g the functional and temporal requirements, and describe refinement te chniques based on this paradigm. We illustrate the calculus with an ex ample taken from the avionics industry.