Specifying Real-Time Requirements for SDL Specifications — A Temporal Logic-Based Approach

  • Stefan Leue
Part of the IFIP Advances in Information and Communication Technology book series (IFIPAICT)


The expressiveness of many state-transition based formal description techniques, e.g. the ITU-TS standardised Specification and Description Language (SDL), does not capture hard real-time requirements. In telecommunications systems engineering, hard real-time requirements, however, are an important class of properties. They occur in the description of progress properties in telecommunications protocols as well as in the specification of real-time related of Quality of Service (QoS) requirements. We suggest integrating functional system properties, given as SDL specifications, with real-time requirements expressed in terms of real-time temporal logic formulas. We call the resulting specifications ‘complementary specifications’. First, we show the inexpressiveness of SDL with respect to hard real-time requirements. Next, we define a common model theoretic foundation which allows SDL specifications to be used jointly with temporal logic specifications. Then we give examples of commonly used real-time related QoS requirements, namely delay bound, delay jitter, and isochronicity. We also discuss the specification of various QoS mechanisms, like QoS negotiation, QoS monitoring and jitter compensation. Finally, we point at related formal verification problems.


Specification Specification and Description Language (SDL) Real-Time Requirements Metric Temporal Logic Model Theoretic Semantics Quality of Service 


  1. 1.
    M. Abadi and L. Lamport. An old-fashioned recipe for real time. In [12], pages 1–27, 1992.Google Scholar
  2. 2.
    B. Alpern and F. B. Schneider. Recognizing safety and liveness. Distributed Computing, 2: 117–126, 1987.CrossRefzbMATHGoogle Scholar
  3. 3.
    R. Mur, C. Courcoubetis, and D. L. Dill. Model checking for real-time systems. In Fifth Annual Symposium on Logic in Computer Science, pages 414–425, 1990.Google Scholar
  4. 4.
    R. Alur and D. Dill. The theory of timed automata. In [12], pages 45–73, 1992.Google Scholar
  5. 5.
    R. Alur and T. A. Henzinger Logics and models of real-time: A survey. In [12], pages 45–73, 1992.Google Scholar
  6. 6.
    R. Alur and T. A. Henzinger. Real-time system = discrete system + clock variables. In T. Rus and C. Rattray, editors, Theories and Experiences for Real-Time System Development, pages 1–30, 1994. To appear.Google Scholar
  7. 7.
    F. Bause and P. Buchholz. Protocol analysis using a timed version of SDL. In J. Quemada, J. Mañas, and E. Vazquez, editors, Formal Description Techniques, III, pages 269–285. North-Holland, 1991.Google Scholar
  8. 8.
    F. Belina, D. Hogrefe, and A. Sarma. SDL with Applications from Protocol Specification. Prentice Hall International, 1991.Google Scholar
  9. 9.
    D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 30 (2): 323–342, April 1983.MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    CCITT. Recommendation Z.100: CCITT Specification and Description Language (SDL). CCITT, Geneva, 1992.Google Scholar
  11. 11.
    K.-T. Cheng and A. S. Krishnakumar Automatic functional test generation using the extended finite state machine model. In Proceedings of the 30th Design Automation Conference DAC-93, pages 86–91, 1993.Google Scholar
  12. 12.
    J. W. de Bakker, C. Huizing, W.P. de Roever, and G.Rozenberg, editors. Real-Time: Theory in Practice, volume 600 of Lecture Notes in Computer Science. Springer-Verlag, 1992.Google Scholar
  13. 13.
    S. R. Faulk and D. L. Parnas. On synchronisation in hard-real-time systems. Communications of the ACM, 31 (3): 274–287, March 1988.CrossRefGoogle Scholar
  14. 14.
    T. A. Henzinger. The Temporal Specification and Verification of Real-Time Systems. Phd thesis, Stanford University, Department of Computer Science, August 1991. Also published as Report No. STAN-CS-91–1380.Google Scholar
  15. 15.
    G. J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall International, 1991.Google Scholar
  16. 16.
    R. Koymans. Specifying Message Passing and Time-Critical Systems with Temporal Logic. PhD thesis, Technical University of Eindhoven, 1989.zbMATHGoogle Scholar
  17. 17.
    A. S. Krishnakumar Reachability and recurrence in extended finite state machines: Modular vector addition systems. In C. Courcoubetis, editor, Computer Aided Verification: Proceedings of CAV’93, volume 697 of Lecture Notes in Computer Science, pages 111–122. Springer Verlag, 1993.Google Scholar
  18. 18.
    J.-Y. Le Boudec. The asynchronous transfer mode: a tutorial. Computer Network and ISDN Systems, 24: 279–309, 1992.CrossRefzbMATHGoogle Scholar
  19. 19.
    M. T. Liu. Protocol engineering. In M. C. Yovitis, editor, Advances in Computers, volume 29, pages 79–195. Academic Press, Inc., 1989.CrossRefGoogle Scholar
  20. 20.
    Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.Google Scholar
  21. 21.
    P. M. Melliar-Smith. Extending interval logic to real-time systems. In B. Banieqbal, H. Barringer, and A. Pnueli, editors, Proceedings of the Conference on Temporal Logic in Specifications, 1987, volume 398 of Lecture Notes in Computer Science, pages 224–242. Springer-Verlag, 1989.Google Scholar
  22. 22.
    M. Merritt, F. Modugno, and M. R. Tuttle. Time-constrained automata. In CONCUR 91: 2nd International Conference on Concurrency Theory, Lecture Notes in Computer Science 527, 1991.Google Scholar
  23. 23.
    H. Saito, T. Hasegawa, and Y. Kakuda. Protocol verification system for SDL specifications based on acyclic expansion algorithm and temporal logic. In K. R. Parker and G. A. Rose, editors, Formal Description Techniques, IV, pages 511–526. North-Holland, 1992.Google Scholar
  24. 24.
    K. J. Turner, editor. Using Formal Description Techniques. John Wiley & Sons, 1993.Google Scholar

Copyright information

© IFIP International Federation for Information Processing 1996

Authors and Affiliations

  • Stefan Leue
    • 1
  1. 1.Department of Electrical and Computer EngineeringUniversity of WaterlooWaterlooCanada

Personalised recommendations