Abstract
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.
The work was partly supported by the Swiss National Science Foundation and the Swiss Federal Office for Education and Scientific Research (while the author was with the University of Berne, Switzerland), and by the National Science and Engineering Research Council of Canada.
Chapter PDF
References
M. Abadi and L. Lamport. An old-fashioned recipe for real time. In [12], pages 1–27, 1992.
B. Alpern and F. B. Schneider. Recognizing safety and liveness. Distributed Computing, 2: 117–126, 1987.
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.
R. Alur and D. Dill. The theory of timed automata. In [12], pages 45–73, 1992.
R. Alur and T. A. Henzinger Logics and models of real-time: A survey. In [12], pages 45–73, 1992.
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.
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.
F. Belina, D. Hogrefe, and A. Sarma. SDL with Applications from Protocol Specification. Prentice Hall International, 1991.
D. Brand and P. Zafiropulo. On communicating finite-state machines. Journal of the ACM, 30 (2): 323–342, April 1983.
CCITT. Recommendation Z.100: CCITT Specification and Description Language (SDL). CCITT, Geneva, 1992.
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.
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.
S. R. Faulk and D. L. Parnas. On synchronisation in hard-real-time systems. Communications of the ACM, 31 (3): 274–287, March 1988.
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.
G. J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall International, 1991.
R. Koymans. Specifying Message Passing and Time-Critical Systems with Temporal Logic. PhD thesis, Technical University of Eindhoven, 1989.
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.
J.-Y. Le Boudec. The asynchronous transfer mode: a tutorial. Computer Network and ISDN Systems, 24: 279–309, 1992.
M. T. Liu. Protocol engineering. In M. C. Yovitis, editor, Advances in Computers, volume 29, pages 79–195. Academic Press, Inc., 1989.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, 1992.
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.
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.
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.
K. J. Turner, editor. Using Formal Description Techniques. John Wiley & Sons, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Leue, S. (1996). Specifying Real-Time Requirements for SDL Specifications — A Temporal Logic-Based Approach. In: Dembiński, P., Średniawa, M. (eds) Protocol Specification, Testing and Verification XV. PSTV 1995. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-34892-6_2
Download citation
DOI: https://doi.org/10.1007/978-0-387-34892-6_2
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2925-1
Online ISBN: 978-0-387-34892-6
eBook Packages: Springer Book Archive