Abstract
Timed Observations is a failure and divergence semantic model for concurrent processes, suitable for real-time systems. Actions are not instantaneous but need some time to complete their execution, and true concurrency is expressed by action multisets (bags). Time is global and discrete.
The model is applied to TCSP, obtaining a denotational semantics, for which a complete proof system is developed.
Part of the work was developed during a two-month sojourn of the first author as collaborator in the RWTH-Aachen (Lehrstuhl für Informatik II) (FRG) and a short visit of the second author to this same center.
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
A. Azcorra. Modelado Formal de Sistemas Síncronos. PhD thesis, ETSI Telecomunicación, Univ.Politécnica de Madrid, 1989.
J.C.M. Baeten and J.A. Bergstra. Real Time Process Algebra. Technical Report, CWI/ Amsterdam, 1990.
G. Boudol and I. Castellani. Concurrency and atomicity. TCS, (59):25–84, 1988.
S.D. Brookes and A.W. Roscoe. An improved failures model for communicating processes. In Pittsburgh Seminar on Concurrency, Springer Verlag, 1985.
S.D. Brookes. A Model for Communicating Sequential Processes. PhD thesis, Oxford Univ., 1983.
R. Gerth and A. Boucher. A timed failures model for extended communicating processes. In ICALP 87, Springer Verlag, 1987.
C.A.R. Hoare, S.D. Brookes, and A.W. Roscoe. A Theory of Communicating Sequential Processes. Technical Report, Programming Research Group / Oxford Univ. (UK), 1981. Tech. Monograph PRG-16.
M. Hennessy. Algebraic Theory of Processes. MIT Press, 1988.
M. Hennessy and T. Regan. A Temporal Process Algebra. Technical Report, University of Sussex (UK), 1990.
R. Koymans, R.K. Shyamasundar, W.P. de Roever, R. Gerth, and S. Arun-Kumar. Compositional semantics for real-time distributed computing. In Conference on Logics of Programs, Springer Verlag, 1985.
R. Milner. A Calculus of Communicating Systems. LNCS 92, Springer Verlag, 1980.
G.J. Milne. CIRCAL and the representation of Communication, Concurrency and Time. Technical Report, Dept.of Computer Science / Univ.Edinburgh (UK), 1983. CSR 151–83.
R. Milner. Calculi for asynchrony and asynchrony. TCS, (25):267–310, 1983.
F. Moller and C. Tofts. A Temporal Calculus of Communicating Systems. Technical Report, Dept.of Computer Science / Univ.Edinburgh (UK), 1989. ECS-LFCS 89–104.
X. Nicollin, J.L. Richier, J. Sifakis, and J. Voiron. ATP-an algebra for timed processes. In M. Broy and C.B. Jones, editors, TC2-Working Conference on Programming Concepts and Methods, North-Holland, 1990.
Y. Ortega-Mallén and D. de Frutos-Escrig. Timed observations: a semantic model for real-time concurrency. In M. Broy and C.B. Jones, editors, TC2-Working Conference on Programming Concepts and Methods, North-Holland, 1990.
E.R. Olderog and C.A.R. Hoare. Specification-oriented semantics for communicating processes. Acta Informatica, (23):9–66, 1986.
E.R. Olderog. Process theory: semantics, specification and verification. In Advanced School on Current Trends in Concurrency, Springer Verlag, 1986.
Y. Ortega-Mallén. En Busca del Tiempo Perdido. PhD thesis, Fac. CC. Matemáticas, Univ.Complutense de Madrid, 1990.
Y. Ortega-Mallén. Timed Observations as Operational Semantics. Technical Report, Dept. Informática y Automática, Univ.Complutense Madrid (Spain), 1991. 91-1.
J. Quemada, A. Azcorra, and D. Frutos. A Timed Calculus for LOTOS. Technical Report, DIT, E.T.S.I. Telecomunicación / Univ. Politécnica de Madrid (Spain), 1989.
G.M. Reed and A.W. Roscoe. Metric spaces as models for real-time concurrency. In Mathematical Foundations of Programming Language Semantics, Springer Verlag, 1987.
S. Schneider. Correctness and Communication in Real-Time Systems. PhD thesis, Oxford University Computing Laboratory (UK), 1990.
A. Salwicki and T. Muldner. On the algoritmic properties of concurrent programs. In Logic of Programs 1979, Springer Verlag, 1981.
D. Taubner and W. Vogler. The step failure semantics and a complete proof system. Acta Informatica, (27):125–156, 1989.
Wang Yi. Real-time behaviour of asynchronous agents. In J.C.M. Baeten and J.W. Klop, editors, CONCUR'90, Theories of Concurrency: Unification and Extension, Springer Verlag, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1991 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ortega-Mallén, Y., de Frutos-Escrig, D. (1991). A complete proof system for timed observations. In: Abramsky, S., Maibaum, T.S.E. (eds) TAPSOFT '91. CAAP 1991. Lecture Notes in Computer Science, vol 493. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53982-4_23
Download citation
DOI: https://doi.org/10.1007/3-540-53982-4_23
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-53982-7
Online ISBN: 978-3-540-46563-8
eBook Packages: Springer Book Archive