An M-Net semantics for a real-time extension of µSDL

  • Hans Fleischhack
  • Josef Tapken
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1313)


In this paper an extension of SDL by real-time assertions is suggested. A denotational compositional semantics in terms of timed high level Petri nets is given. This semantics allows to reason about timed SDL-specifications by simulation of the underlying high level nets as well as by unfolding these into timed low level nets and then applying analysis methods for timed Petri nets or temporal model checking. The approach is embedded in the MOBY-tool.


Temporal Logic Firing Event Expiry Time Action Symbol Input Queue 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    P. Amthor, H. Fleischhack, and J. Tapken: MOBY — more than a Tool for the Verification of SDL-Specifications, Research Paper, Universität Oldenburg, 1996.Google Scholar
  2. 2.
    F. Bause and P. Buchholz, Protocol Analysis Using a Timed Version of SDL, in J. Quemada, J. Mañas, and E. Vazquez (Eds.), Formal Description Techniques, III, pp. 269–285, North-Holland, 1991.Google Scholar
  3. 3.
    B. Berthomieu and M. Diaz, Modelling and Verification of Time Dependent Systems Using Time Petri Nets, IEEE Transactions on Software Engineering, Volume 17/3, pages 259–273 (1991).Google Scholar
  4. 4.
    E. Best, Partial Order Verification with PEP, Report HIB 26/96, Universität Hildesheim, 1996.Google Scholar
  5. 5.
    E. Best, R. Devillers, and J. G. Hall. The box calculus: a New Causal Algebra With Multi-Label Communication. In G. Rozenberg, (Ed.); Advances in Petri Nets 92, Volume 609 of Lecture Notes in Computer Science, pages 21–69. Springer, 1992.Google Scholar
  6. 6.
    E. Best, H. Fleischhack, W. Fraczak, R. P. Hopkins, H. Klaudel, and E. Pelz. A Class of Composable High Level Petri Nets. In G. De Michelis and M. Diaz, (Eds.), Application and Theory of Petri Nets 1995, Volume 935 of Lecture Notes in Computer Science, pages 103–118. Springer, 1995.Google Scholar
  7. 7.
    E. Best, H. Fleischhack, W. Fraczak, R. P., H. Mandel, and E. Pelz. An M-net Semantics of B(PN)2. In J. Desel, (Ed.), Structures in Concurrency Theory, Workshops in Computing, Springer, 1995.Google Scholar
  8. 8.
    CCITT. Specification and Description Language, CCITT Z.100, International Consultative Committee on Telegraphy and Telephony, Geneva, 1992.Google Scholar
  9. 9.
    J. Esparza. Model Checking Using Net Unfoldings, Science of Computer Programming, Volume 23, pages 151–195, Elsevier, 1994.Google Scholar
  10. 10.
    H. Fleischhack, and B. Grahlmann, Towards Compositional Verification of SDL Systems, Research Paper, 1997. (submitted)Google Scholar
  11. 11.
    B. Grahlmann and E. Best: PEP-More Than a Petri Net Tool. In T. Margaria and B. Steffen, (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, Volume 1055 of Lecture Notes in Computer Science, pages 397–401, Springer, 1996.Google Scholar
  12. 12.
    J. Henriksen e.a., MONA: Monadic Second-Order Logic in Practice, in Brinksma, Cleaveland, Larsen, Margaria, and Steffen, (Eds.) TACAS '95, Tools and Algorithms for The Construction and Analysis of Systems, Volume 1019 of Lecture Notes in Computer Science, pages 89–110, Springer, 1995.Google Scholar
  13. 13.
    S. Leue, Specifying Real-Time Requirements for SDL Specifications — a Temporal Logic-Based Approach, Research Paper, University of Waterloo, Canada, 1996.Google Scholar
  14. 14.
    P. Merlin and D. Farber, Recoverability of Communication Protocols — Implication of a Theoretical Study, IEEE Transactions on Software Communications Vol. 24, 1036–1043 (1976).Google Scholar
  15. 15.
    L. Popova: On Time Petri Nets. Journal of Information Processing and Cybernetics, Volume 1055 of Lecture Notes in Computer Science, Springer, 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Hans Fleischhack
    • 1
  • Josef Tapken
    • 1
  1. 1.Fachbereich InformatikCarl-von-Ossietzky-Universität OldenburgOldenburg

Personalised recommendations