Abstract
We present an overview and synthesis of existing results about process algebras for the specification and analysis of timed systems. The motivation is double: present an overview of some relevant and representative approaches and suggest a unifying framework for them.
After presenting fundamental assumptions about timed systems and the nature of abstract time, we propose a general model for them: transition systems whose labels are either elements of a vocabulary of actions or elements of a time domain. Many properties of this model are studied concerning their impact on description capabilities and on realisability issues.
An overview of the language features of the process algebras considered is presented, by focusing on constructs used to express time constraints. The presentation is organised as an exercise of building a timed process algebra from a standard process algebra for untimed systems. The overview is completed by a discussion about description capabilities according to semantic and pragmatic criteria.
Work supported by the ESPRIT BRA SPEC
Chapter PDF
Similar content being viewed by others
References
D. Austry and G. Boudol. Algèbre de processus et synchronisation. Theoretical Computer Science, 30, 1984.
J.C.M. Baeten and J.A. Bergstra. Real Time Process Algebra. Technical Report CS-R9053, Centre for Mathematics and Computer Science, Amsterdam, the Netherlands, 1990.
G. Berry and L. Cosserat. The Esterel synchronous programming language and its mathematical semantics. In LNCS 197: Proceedings CMU Seminar on Concurrency, Springer-Verlag, 1985.
T. Bolognesi and F. Lucidi. LOTOS-like process algebra with urgent or timed interactions. In Proceedings of REX Workshop “Real-Time: Theory in Practice”. Mook, the Netherlands, June 1991.
P. Caspi, N. Halbwachs, D. Pilaud, and J. Plaice. Lustre: a declarative language for programming synchronous systems. In 14th Symposium on Principles of Programming Languages, Munich, January 1987.
J. Davies and S. Schneider. An Introduction to Timed CSP. Technical Report PRG-75, Oxford University Computing Laboratory, UK, August 1989.
D. Harel. StateCharts: a visual approach to complex systems. Science of Computer Programming, 8–3:231–275, 1987.
M. Hennessy and T. Regan. A Temporal Process Algebra. Technical Report 2/90, University of Sussex, UK, April 1990.
M. Hennessy and T. Regan. A Process Algebra for Timed Systems. Technical Report 5/91, University of Sussex, UK, April 1991.
A.S. Klusener. Completeness in Real Time Process Algebra. Technical Report CS-R9106, Centre for Mathematics and Computer Science, Amsterdam, the Netherlands, January 1991.
R. Milner. A Calculus of Communicating Systems. In LNCS 92, Springer Verlag, 1980.
R. Milner. Calculi for Synchrony and Asynchrony. Theoretical Computer Science, 25, 1983.
G. J. Milne. The Formal Description and Verification of Hardware Timing. IEEE Transactions on Computers, 40 (7), July 1991.
F. Moller and C. Tofts. A Temporal Calculus of Communicating Processes. In J.C.M. Baeten and J.W. Klop, editors, LNCS 458. Proceedings of CONCUR '90 (Theories of Concurrency: Unification and Extension), Amsterdam, the Netherlands, pages 401–415, Springer-Verlag, August 1990.
X. Nicollin, J.-L. Richier, J. Sifakis, and J. Voiron. ATP: an Algebra for Timed Processes. In Proceedings of the IFIP TC 2 Working Conference on Programming Concepts and Methods, Sea of Gallilee, Israel, April 1990.
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, J. Sifakis, and S. Yovine. From ATP to Timed Graphs and Hybrid Systems. In Proceedings of REX Workshop “Real-Time: Theory in Practice”. Mook, the Netherlands, June 1991.
G.D. Plotkin. A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19, århus University. Computer Science Department, århus, Denmark, 1981.
G.M. Reed and A.W. Roscoe. A timed model for Communicating Sequential Processes. Theoretical Computer Science, 58 (pp 249–261), 1988.
S. Schneider. An Operational Semantics for Timed CSP. Programming Research Group, Oxford University, UK, February 1991.
Wang Yi. Real-time behaviour of asynchronous agents. In J.C.M. Baeten and J.W. Klop, editors, LNCS 458. Proceedings of CONCUR '90 (Theories of Concurrency: Unification and Extension), Amsterdam, the Netherlands, pages 502–520, Springer-Verlag, August 1990.
Wang Yi. CCS+Time=an Interleaving Model for Real Time Systems. In Proceedings of ICALP '91, Madrid, Spain, July 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1992 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nicollin, X., Sifakis, J. (1992). An overview and synthesis on timed process algebras. In: Larsen, K.G., Skou, A. (eds) Computer Aided Verification. CAV 1991. Lecture Notes in Computer Science, vol 575. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55179-4_36
Download citation
DOI: https://doi.org/10.1007/3-540-55179-4_36
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-55179-9
Online ISBN: 978-3-540-46763-2
eBook Packages: Springer Book Archive