PMC:

A Process Algebra for Real-Time Systems

Henrik Reif Andersen and Michael Mendler

Department of Computer Science, Technical University of Denmark Building 344, DK-2800 Lyngby, Denmark E-mail: {hra,mvm}@id.dtu.dk

Abstract

Most timed process algebras view a real-time system as operating under the regime of a global time parameter constraining the occurrence of actions. By the use of quantitative timing constraints they aim at describing completely the global real-time behaviour of timed systems in a fairly detailed fashion. Based on an industrial case study we believe that these approaches are often overly realistic with disadvantages for both the specification and the modelling of real-time systems. We propose a rather different, abstract approach to the specification and modelling of real-time systems that captures the qualitative aspects of timing constraints through the use of multiple clocks. Clocks enforce global synchronization of actions without compromising the abstractness of time by referring to a concrete time domain. Technically, we present the process algebra PMC as a non-trivial extension of CCS by multiple clocks with associated timeout and clock ignore operators.

We describe the object of investigation in the industrial case study, a highly sophisticated instrument – the Brüel & Kjær 2145 Frequency Analyzer – and show how the central real-time constraints are expressed concisely in PMC. Focus is on the actual specification of the instrument and the technical results that have been obtained for PMC is only touched briefly.

Relevant references

For the algebraic theory, see [AM94] (proofs in [AM93a, AM93b]). For more details on the case study, see [AM95]. These papers are available by WWW (URL http://www.id.dtu.dk/∼hra) or anonymous ftp (ftp.id.dtu.dk, directory pub/hra).

References

[AM93a] Henrik R. Andersen and Michael V. Mendler. A process algebra with multiple clocks. Technical Report ID-TR: 1993-122, Department of Computer Science, Technical University of Denmark, August 1993.

[AM93b] Henrik R. Andersen and Michael V. Mendler. Complete axiomatization of observation congruence for PMC. Technical Report ID-TR: 1993-126, Department of Computer Science, Technical University of Denmark, December 1993.

[AM94] Henrik R. Andersen and Michael V. Mendler. An asynchronous process algebra with multiple clocks. In Donald Sannella, editor, ESOP’94. Proceedings of the 5th European Symposium on Programming, Edinburgh, Scotland, 11-13 April 1994, volume 788 of LNCS, pages 58–73. Springer-Verlag, April 1994.

[AM95] Henrik R. Andersen and Michael V. Mendler. Describing a signal analyzer in the process algebra PMC – a case study. To appear in proceedings of FASE’95, LNCS, 1995. Preprint available as technical report ID-TR: 1994-144, Department of Computer Science, Technical University of Denmark, August 1994.