PARTY:

A Process Algebra with Real-Time from York1

Chris Ho-Stuart H. S. M. Zedan Ming Fang C. M. Holt2

Formal Systems Research Group3

Computer Science Dept, University of York, YO1 5DD, UK

Abstract.

A number of process algebras for describing real-time behaviour have been proposed in recent years, but they invariably make restrictive assumptions about the kinds of behaviour which can be described.

We introduce the Process Algebra with Real-Time from York (PARTY). PARTY is based on a simple yet powerful, intuitive and general model of real-time behaviour. A realtime process interacts with its environment by synchronizing on observable instantaneous actions. There is no lower limit on the time between successive events, and we do not assume maximum parallelism.

PARTY expressions can represent behaviour constrained by limited resources, and value passing behaviour. A program has been written for analysing PARTY processes.

1 Introduction

A number of process algebras for real-time systems have been proposed in recent years, extending earlier untimed process algebras. Milner's CCS[11] has several extensions[4, 6, 12, 16], Hoare's CSP[8] has been extended to Timed CSP[15] and the ProCoS programming language PLtime[10], and Baeten and Weijland's ACP[3] has a timed extension[2]. Timed CSP has recently been given operational semantics[14], although these semantics do not correspond exactly with the original Timed CSP. Each of these extensions has significant limitations.

PARTY is a real-time process algebra which addresses these limitations, while still having a small set of simple process constructors and an elegant and general underlying abstraction of real-time behaviour[7]. An effective formal method for reasoning about behaviour specifications is currently being developed. A PARTY workbench has been written, and has been used to test all the sample processes given in this paper. The workbench has a number of planned extensions, but has already proved to be a useful tool for checking specifications.

Of the models which exist for processes without explicit time, the synchronization trees of CCS[11] in particular have been very influential, and have served as a useful vehicle for comparing other process

1This work is supported by IED/SERC funded project (GR/F 98055/4/1/2083)
2C. M. Holt is at the University of Newcastle-upon-Tyne
3Email addresses are [email protected] [email protected]
[email protected] [email protected]