Skip to main content
SpringerLink
Log in

Reconciling real-time with asynchronous message passing

  • Conference paper
  • First Online:
FME '97: Industrial Applications and Strengthened Foundations of Formal Methods (FME 1997)

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

Included in the following conference series:

Abstract

At first sight, real-time and asynchronous message passing like in SDL and ROOM seem to be incompatible. Indeed these languages fail to model real-time constraints accurately. In this paper, we show how to reconcile real-time with asynchronous message passing, by using an assumption which is supported by every mailing system throughout the world, namely that messages are time-stamped with their sending and arrival time. This assumption allows us to develop a formalism which is adequate to model and to specify real-time constraints. The proposed formalism is shown at work on a small real-time example.

This work is partly sponsored by the Deutsche Forschungs Gemeinschaft (DFG) project SYSLAB

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. Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science, 2(126):183–235, April 1994.

    Google Scholar 

  2. R. Alur and T.A. Henzinger. Logics and models of real time: a survey. In J.W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, editors, Real Time: Theory in Practice, Lecture Notes in Computer Science 600, pages 74–106. Springer-Verlag, 1992.

    Google Scholar 

  3. F. Bause and P. Buchholz. Protocol analysis using a timed version of SDL. In J. Quemada, J. Malias, and E. Vazquez, editors, Formal Description Techniques. North Holland, 1991.

    Google Scholar 

  4. [BDD+93] M. Broy, F. Dederichs, C. Dendorfer, M. Fuchs, T.F. Gritzner, and R. Weber.The Design of Distributed Systems-An Introduction to FOCUS. Technical Report SFB 342/2/92 A, Technische Universität München, Institut für Informatik, 1993.

    Google Scholar 

  5. M. Broy and K. Stølen. Interactive System Design. To appear, 1997.

    Google Scholar 

  6. Radu Grosu, Cornel Klein, and Bernhard Rumpe. Enhancing the SYSLAB system model with state. TUM-I 9631, Technische Universität München, 1996.

    Google Scholar 

  7. Radu Grosu, Cornel Klein, Bernhard Rumpe, and Manfred Broy. State transition diagrams. TUM-I 9630, Technische Universität München, 1996.

    Google Scholar 

  8. Radu Grosu and Ketil Stoelen. A Model for Mobile Point-to-Point Dataflow Networks without Channel Sharing. In Martin Wirsing and Maurice Nivat, editors, Proceedings of the 5th International Conference on Algebraic Methodology and Software Technology, AMAST'96, Munich, Germany, pages 505–519. Lecture Notes in Computer Science 1101, 1996.

    Google Scholar 

  9. D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8, 1987.

    Google Scholar 

  10. Ursula Hinkel. SDL and Time — A Mysterious Relationship. 1996. submitted to SDL Forum 97.

    Google Scholar 

  11. T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. In Proceedings of the Seventh Annual Symposium on Logic in Computer Science, pages 394–406. IEEE Computer Society Press, 1992.

    Google Scholar 

  12. C.A.R. Hoare. Communicating sequential processes. Prentice-Hall International series in computer science. Prentice Hall, Inc., Englewood Cliffs, New Jersey, 1985.

    Google Scholar 

  13. ITU-T. Recommendation Z.100, Specification and Description Language (SDL). ITU-T, Geneva, 1993.

    Google Scholar 

  14. ITU-T. Z.120 — Message Sequence Chart (MSC). ITU-T, Geneva, 1996.

    Google Scholar 

  15. S. Leue. Specifying Real-Time Requirements for SDL Specifications — A Temporal Logic-Based Approach. In Proceedings of the Fifteenth International Symposium on Protocol Specification, Testing, and Verification PSTV'95. Chapmann & Hall, 1995.

    Google Scholar 

  16. N. Lynch, R. Segala, F. Vaandrager, and H.B. Weinberg. Hybrid I/O automata. Technical Report CS-119578, CWI, Computer Science Department, Amsterdam, 1995. Also appeared in: Hybrid Systems III, Lecture Notes in Computer Science. Available under http://www.cs.kun.nl/-fvaan/.

    Google Scholar 

  17. N.A. Lynch and F. Vaandrager. Forward and backward simulations — part II: Timed systems. Information and Computation, 128(1):1–25, 1996.

    Google Scholar 

  18. Olaf Müller and Peter Scholz. Specification of real-time and hybrid systems in Focus. TUM-I 9627, Technische Universität München, 1996.

    Google Scholar 

  19. A. Olsen, O. Faegemand, B. Møller-Pedersen, R. Reed, and J. R. W. Smith. Systems Engineering Using SDL-92. Elsevier Science, NorthHolland, 1994.

    Google Scholar 

  20. L.C. Paulson. ML for the Working Programmer. Cambridge University Press, 1991.

    Google Scholar 

  21. B. Rumpe and C. Klein. Automata describing object behavior.In H. Kilov and W. Harvey, editors, Specification of Behavioral Semantics in Object-Oriented Information Modeling, pages 265–286, Norwell, Massachusetts, 1996. Kluwer Academic Publishers.

    Google Scholar 

  22. B. Selic, G. Gullekson, and P. T. Ward. Real-Time Object-Oriented Modeling. John Wiley and Sons, Inc., 1994.

    Google Scholar 

  23. M. Von der Beeck. A Comparison of Statecharts Variants. Lecture Notes in Computer Science, 863:128–148, September 1994.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, D-80290, TU München

    M. Broy, R. Grosu & C. Klein

Authors
  1. M. Broy
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. R. Grosu
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. C. Klein
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

John Fitzgerald Cliff B. Jones Peter Lucas

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Broy, M., Grosu, R., Klein, C. (1997). Reconciling real-time with asynchronous message passing. In: Fitzgerald, J., Jones, C.B., Lucas, P. (eds) FME '97: Industrial Applications and Strengthened Foundations of Formal Methods. FME 1997. Lecture Notes in Computer Science, vol 1313. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63533-5_10

Download citation

  • DOI: https://doi.org/10.1007/3-540-63533-5_10

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63533-8

  • Online ISBN: 978-3-540-69593-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation