Advertisement

A complete proof system for timed observations

  • Yolanda Ortega-Mallén
  • David de Frutos-Escrig
CAAP Colloquium On Trees In Algebra And Programming
Part of the Lecture Notes in Computer Science book series (LNCS, volume 493)

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.

Keywords

Normal Form Proof System Basic Term Concurrent Process Denotational Semantic 
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

  1. [Azc89]
    A. Azcorra. Modelado Formal de Sistemas Síncronos. PhD thesis, ETSI Telecomunicación, Univ.Politécnica de Madrid, 1989.Google Scholar
  2. [BB90]
    J.C.M. Baeten and J.A. Bergstra. Real Time Process Algebra. Technical Report, CWI/ Amsterdam, 1990.Google Scholar
  3. [BC88]
    G. Boudol and I. Castellani. Concurrency and atomicity. TCS, (59):25–84, 1988.Google Scholar
  4. [BR85]
    S.D. Brookes and A.W. Roscoe. An improved failures model for communicating processes. In Pittsburgh Seminar on Concurrency, Springer Verlag, 1985.Google Scholar
  5. [Bro83]
    S.D. Brookes. A Model for Communicating Sequential Processes. PhD thesis, Oxford Univ., 1983.Google Scholar
  6. [GB87]
    R. Gerth and A. Boucher. A timed failures model for extended communicating processes. In ICALP 87, Springer Verlag, 1987.Google Scholar
  7. [HBR81]
    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
  8. [Hen88]
    M. Hennessy. Algebraic Theory of Processes. MIT Press, 1988.Google Scholar
  9. [HR90]
    M. Hennessy and T. Regan. A Temporal Process Algebra. Technical Report, University of Sussex (UK), 1990.Google Scholar
  10. [KSdR*85]
    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.Google Scholar
  11. [Mil80]
    R. Milner. A Calculus of Communicating Systems. LNCS 92, Springer Verlag, 1980.Google Scholar
  12. [Mil83a]
    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.Google Scholar
  13. [Mil83b]
    R. Milner. Calculi for asynchrony and asynchrony. TCS, (25):267–310, 1983.Google Scholar
  14. [MT89]
    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
  15. [NRSV90]
    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
  16. [OdF90]
    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.Google Scholar
  17. [OH86]
    E.R. Olderog and C.A.R. Hoare. Specification-oriented semantics for communicating processes. Acta Informatica, (23):9–66, 1986.Google Scholar
  18. [Old86]
    E.R. Olderog. Process theory: semantics, specification and verification. In Advanced School on Current Trends in Concurrency, Springer Verlag, 1986.Google Scholar
  19. [Ort90]
    Y. Ortega-Mallén. En Busca del Tiempo Perdido. PhD thesis, Fac. CC. Matemáticas, Univ.Complutense de Madrid, 1990.Google Scholar
  20. [Ort91]
    Y. Ortega-Mallén. Timed Observations as Operational Semantics. Technical Report, Dept. Informática y Automática, Univ.Complutense Madrid (Spain), 1991. 91-1.Google Scholar
  21. [QAF89]
    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
  22. [RR87]
    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.Google Scholar
  23. [Sch90]
    S. Schneider. Correctness and Communication in Real-Time Systems. PhD thesis, Oxford University Computing Laboratory (UK), 1990.Google Scholar
  24. [SM81]
    A. Salwicki and T. Muldner. On the algoritmic properties of concurrent programs. In Logic of Programs 1979, Springer Verlag, 1981.Google Scholar
  25. [TV89]
    D. Taubner and W. Vogler. The step failure semantics and a complete proof system. Acta Informatica, (27):125–156, 1989.Google Scholar
  26. [Yi90]
    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.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • Yolanda Ortega-Mallén
    • 1
  • David de Frutos-Escrig
    • 1
  1. 1.Sección Departamental de Informática y Automática Facultad de MatemáticasUniversidad ComplutenseMadridSpain

Personalised recommendations