An action-based formal model for

concurrent, real-time systems?

C.J. Fidgey A.J. Wellingsz

Abstract

A formal model for describing concurrent, real-time systems is presented. It is based on existing atomic-action formalisms, yet can handle practical concerns such as time-consuming behaviours, both true and interleaved concurrency, and pre-emption of actions. A multi-layered development method is described which can model the steps that programmers actually undertake in the design of such systems.

Keywords and phrases: real time; concurrency; action systems; Z; Ada.

1 Introduction

Many formal approaches to modelling real-time systems have been proposed in recent years. However, to facilitate elegant definitions, most make simplifying assumptions such as `maximal parallelism' and `instantaneous' actions that do not match reality. In short, such models are inadequate for representing the development steps that real-time programmers actually undertake when faced with practical concerns such as task pre-emption, priority-based scheduling policies, operating system overheads, etc.

Here we present a formal approach that can model such concepts. It is based on the `action system' [Bac92] approach to modelling concurrency with the specification language Z [PST91] used to describe individual actions. Although both of these formalisms are founded on a notion of atomic actions, our method can nevertheless model time-consuming, overlapping behaviours, and pre-emption of actions.
?This report is also available as Software Verification Research Centre, University of Queensland, Technical Report 95-1, January 1995.
ySoftware Verification Research Centre, Department of Computer Science, The University of Queensland, Queensland 4072, Australia. E-mail: [email protected]
zReal-time Systems Research Group, Department of Computer Science, University of York, Heslington, York, Y01 5DD, United Kingdom. E-mail: [email protected]