Real-time computer systems differ from general-purpose computer systems in that they introduce the notion of time to the computational requirements of the system. Real-time systems must not only provide logically correct and adequate results but these results also have to be provided within a certain period of time.
In this work we introduce Circus Time Action; the language uses a subset of Circus and adds time operators to the notion of actions in Circus. We propose an extension to the semantic model of the UTP. The new model captures time information and registers these observations along with the other observations of the program; the model proposed is a discrete time mode. The decision of using a discrete time model instead of a continuous time model is the fact that Circus is both a programming language and a specification language and discrete models can be used in both specification and programming. The language can be used to specify both hard and soft real-time systems; it is also suitable for representing periodic and aperiodic tasks. We also explore the relation between the new time model and the UTP model.
As a further contribution, we propose a framework based on partitioning a timed program into untimed programs plus timer events and a set of timers; when in parallel the two parts are semantically equivalent to the original program. The untimed part uses two new operators, normal form external choice and the parallel composition these operators have specialised behaviour concerning the timer events. We give the semantics of these new operators in an algebric style. We show that the algebraic characterisation is complete by a normal form reduction process which eliminate these operators. The normal form program resulting from the application of the algebraic laws is an untimed program that contains timer events but preserving the semantics of the original timed program. The framework permits the use of untimed tools for model checking such as FDR in the validation of timed specifications. To illustrate the framework we analysis some properties of the simple alarm system controller. The specification of the system is given using Circus Time Action, the normal form program is obtained by applying a syntax transformation. The requirements of the alarm controller are also expressed in Circus Time Action and transformed to a normal form. We use the CSP model checking tool to show that the program meets its requirements.
Department of Computer Science
Deramore Lane, University of York, Heslington, York, YO10 5GH, UK
Tel: 01904 325500 | Fax: 01904 325599