Skip to main content
SpringerLink
Log in

Operational semantics for timed observations

  • Session 9A
  • Conference paper
  • First Online:
Formal Techniques in Real-Time and Fault-Tolerant Systems (FTRTFT 1992)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 571))

Abstract

Timed Observations is a semantical framework suitable to study the behaviour of timed concurrent processes. For each process we observe its external behaviour consisting of timed traces (the visible actions performed by the process and related to the instant time when they are executed), refusals (actions refused by a process after executing a trace), and the possibly divergent timed traces (traces that can be extended by an unbounded sequence of internal actions). Thus the model has a timed failures divergences semantics, and was already presented in [OdF90b] as a denotational semantics, which was applied to TCSP. In the present paper we concentrate on giving an equivalent operational characterization.

Part of the work was developed during a two-month sojourn of the author as collaborator in the RWTH-Aachen (Lehrstuhl für Informatik II) (G).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. J.C.M. Baeten and J.A. Bergstra. Real Time Process Algebra. Technical Report, CWI, Amsterdam, 1990.

    Google Scholar 

  2. J.A. Bergstra and J.W. Klop. Algebra of communicating processes with abstraction. TCS, (37):77–121, 1985.

    Google Scholar 

  3. S.D. Brookes and A.W. Roscoe. An improved failures model for communicating processes. In Pittsburgh Seminar on Concurrency, Springer Verlag, 1985. LNCS 197.

    Google Scholar 

  4. S.D. Brookes. A Model for Communicating Sequential Processes. PhD thesis, Oxford Univ., 1983.

    Google Scholar 

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

    Google Scholar 

  6. M. Hennessy. Algebraic Theory of Processes. MIT Press, 1988.

    Google Scholar 

  7. M. Hennessy and T. Regan. A Temporal Process Algebra. Technical Report, University of Sussex (UK), 1990.

    Google Scholar 

  8. ISO. Information Processing Systems — Open Systems Interconnection — Lotos: a Formal Description Technique based on the Temporal Ordering of Observational Behaviour. 1987. DIS8807.

    Google Scholar 

  9. R. Koymans, R.K. Shyamasundar, W.P. de Roever, R. Gerth, and S. ArunKumar. Compositional semantics for real-time distributed computing. In Conference on Logics of Programs, Springer Verlag, 1985. LNCS 193.

    Google Scholar 

  10. R. Milner. A Calculus of Communicating Systems. LNCS 92, Springer Verlag, 1980.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  13. 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, Programming Concepts and Methods, North-Holland, 1990.

    Google Scholar 

  14. Y. Ortega-Mallén and D. de Frutos-Escrig. A complete proof system for timed observations. In Abramsky and Maibaum, editors, TAPSOFT'91, Springer-Verlag, 1991. LNCS 493, vol.1.

    Google Scholar 

  15. E.R. Olderog and C.A.R. Hoare. Specification-oriented semantics for communicating processes. Acta Informatica, (23):9–66, 1986.

    Google Scholar 

  16. Y. Ortega-Mallén. En Busca del Tiempo Perdido. PhD thesis, Fac. CC. Matemáticas, Univ.Complutense de Madrid, 1990.

    Google Scholar 

  17. D.M.R. Park. Concurrency and automata on infinite sequences. In 5 th. G.I. Conference, Springer Verlag, 1981. LNCS 104.

    Google Scholar 

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

    Google Scholar 

  19. 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. LNCS 298.

    Google Scholar 

  20. D. Taubner and W. Vogler. The step failure semantics and a complete proof system. Acta Informatica, (27):125–156, 1989.

    Google Scholar 

  21. Wang Yi. CCS + time = an interleaving semantic model for real time systems. November 1990. Chalmers University of Technology, S-41296 Goteborg, Sweden.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Sectión de Informática y Automática Facultad de Matemáticas, Universidad Complutense, 28040, Madrid, Spain

    Yolanda Ortega-Mallén

Authors
  1. Yolanda Ortega-Mallén
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jan Vytopil

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ortega-Mallén, Y. (1991). Operational semantics for timed observations. In: Vytopil, J. (eds) Formal Techniques in Real-Time and Fault-Tolerant Systems. FTRTFT 1992. Lecture Notes in Computer Science, vol 571. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-55092-5_28

Download citation

  • DOI: https://doi.org/10.1007/3-540-55092-5_28

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-55092-1

  • Online ISBN: 978-3-540-46692-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation