Abstract
In this paper we take a look at real-time systems from an implementation-oriented perspective. We are interested in the formal description of genuinely distributed systems whose correct functional behaviour depends on real-time constraints. The question of how to combine real-time with distributed processing in a clean and satisfactory way is the object of our investigation.
The approach we wish to advance is based on PMC, an asynchronous process algebra with multiple clocks. The keywords here are ‘asynchrony’ as the essential feature of distributed computation and the notion of a ‘clock’ as an elementary real-time mechanism. We base the discussion on an actual industrial product: The Brüel & Kjær 2145 Vehicle Signal Analyzer, an instrument for measuring and analyzing noise generated by cars and other machines with rotating objects. We present an extension of PMC by ML-style value passing and demonstrate its use on a simplified version of the Brüel & Kjær Signal Analyzer.
The first author has been supported by the Danish Technical Research Council and the second author by the Human Capital and Mobility Network Euro Form.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
L. Aceto and D. Murphy. On the ill-timed but well-caused. In E. Best, editor, Proc. Concur'93, pages 97–111. Springer LNCS 715, 1993.
R. Alur and D. Dill. The theory of timed automata. In de Bakker et al. [11], pages 45–73.
H. R. Andersen and M. Mendler. A complete axiomatization of observation congruence in PMC. Technical Report ID-TR:1993-126, Department of Computer Science, Technical University of Denmark, December 1993.
H. R. Andersen and M. Mendler. A process algebra with multiple clocks. Technical Report ID-TR:1993-122, Department of Computer Science, Technical University of Denmark, August 1993.
H. R. Andersen and M. Mendler. An asynchronous process algebra with multiple clocks. In D. Sannella, editor, Programming Languages and Systems — ESOP'94, pages 58–73. Springer, LNCS 788, 1994.
J.C.M. Baeten and J.W. Klop, editors. Proceedings of CONCUR '90, volume 458 of LNCS. Springer-Verlag, 1990.
G. Berry and L. Cosserat. The esterel synchronous programming language and its mathematical semantics. In S. D. Brookes, A. W. Roscoe, and G. Winskel, editors, Seminar on Concurrency, pages 389–448. Springer LNCS 197, 1984.
G. Berry, S. Ramesh, and R.K. Shyamasundar. Communicating reactive processes. In Principles of Programming Languages POPL'93, pages 85–98. ACM, 1993.
Brüel & Kjær. Vehicle Signal Analyzer Type 2145, User Manual Vol. 1, April 1994.
Zhou Chaochen, C. A. R. Hoare, and A. P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269–276, 1991.
J. W. de Bakker, C. Huizing, W. P. de Roever, and G. Rozenberg, editors. Real-Time: Theory in Practice, volume 600 of LNCS. Springer-Verlag, 1991.
N. Halbwachs, D. Pilaud, F. Ouabdesselam, and A.-C. Glory. Specifying, programming and verifying real-time systems using a synchronous declarative language. In Workshop on automatic verification methods for finite state systems, Grenoble, France, June 12–14 1989. Springer LNCS 407.
M. Hennessy and H. Lin. Symbolic bisimulations. Technical Report 1/92, University of Sussex, April 1992.
M. Hennessy and T. Regan. A process algebra for timed systems. Computer Science Technical Report 91:05, Department of Computer Science, University of Sussex, April 1991. To appear in Information and Computation.
Jozef Hooman. Specification and Compositional Verification of Real-Time Systems. Number 558 in Lecture Notes in Computer Science. Springer-Verlag, 1991.
Chen Liang. An interleaving model for real-time systems. Technical Report ECS-LFCS-91-184, Laboratory for Foundations of Computer Science, University of Edinburgh, November 1991.
R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT press, 1990.
Robin Milner. Communication and Concurrency. Prentice Hall, 1989.
Robin Milner, Joachim Parrow, and David Walker. Modal logics for mobile processes. Technical Report SICS/R-91/03-SE, Swedish Institute of Computer Science, 1991.
Faron Moller and Chris Tofts. A temporal calculus of communicating systems. In Baeten and Klop [6], pages 401–415.
X. Nicollin and J. Sifakis. The algebra of timed processes ATP: theory and application. Technical Report RT-C26, LGI-IMAG, Grenoble, France, December 1990.
X. Nicollin and J. Sifakis. An overview and synthesis on timed process algebras. In de Bakker et al. [11], pages 526–548.
G. Reed and A. Roscoe. A timed model for communicating sequential processes. In Laurent Kott, editor, Proceedings of the 13'th ICALP, pages 314–323. Springer, LNCS 226, 1986.
S. Schneider, J. Davies, D.M. Jackson, G.M. Reed, J.N. Reed, and A.W. Roscoe. Timed CSP: Theory and practice. In de Bakker et al. [11], pages 526–548.
Yi Wang. Real-time behaviour of asynchronous agents. In Baeten and Klop [6].
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Andersen, H.R., Mendler, M. (1995). Describing a Signal Analyzer in the process algebra PMC — A case study. In: Mosses, P.D., Nielsen, M., Schwartzbach, M.I. (eds) TAPSOFT '95: Theory and Practice of Software Development. CAAP 1995. Lecture Notes in Computer Science, vol 915. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59293-8_224
Download citation
DOI: https://doi.org/10.1007/3-540-59293-8_224
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-59293-8
Online ISBN: 978-3-540-49233-7
eBook Packages: Springer Book Archive