A Semantics for Limited Resource Refinement

Simon Atkinson?

Real-Time Systems Research Group

Department of Computer Science

University of York

Heslington, York, YO1 5DD

May 6, 1996

Abstract

The correct development of Real-Time Systems is critical. The use of formal development methods for Real-Time Systems is a means of ensuring their correct behaviour. A refinement calculus such as TAM [SZ93] is a formal method which aims to achieve this. Unfortunately, most Real-Time Systems have some form of limited resources which cannot be expressed during the development process in TAM. This paper presents a new semantics for the TAM operators and extends the scope of the TAM refinement calculus to include limited resources

1 Introduction

Real-Time systems are increasingly used in todays society. In many areas of their application their correct behaviour is critical. A formal development method for Real-Time systems is of great benefit for these applications as the behaviour of the implementation can be proved correct and that it meets its requirements. One such formal method which aims to be a realistic development method for Real-Time systems is TAM [SZ93, Sch92]. This method has a wide spectrum language allowing specifications and implementations to be expressed and a refinement calculus [Mor90] to formally derive an implementation

?Supported by EPSRC grant 93313802.