PMC: A Process Algebra for Real-Time Systems

Henrik Reif Andersen
Michael Mendler

In 6th NWPT, pages 78-79

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 qualitativeaspects 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.

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

Available as PostScript, DVI,
Relevant papers.

BRICS WWW home page