Abstract
We describe an approach for the verification of quantitative temporal properties of SDL specifications, which adapts techniques developed for timed automata [2]. With respect to other verification approaches applied to SDL, our approach broadens the class of analyzable specifications and improves the handling of non-deterministic systems, such as open systems communicating with an unspecified environment. Compared to the initial framework of timed automata, the application of these verification techniques to SDL raises two interesting issues, discussed in the paper. They are: expressing the semantics of time in SDL in terms of timed automata concepts, and employing a user friendly automata-based property specification language (GOAL [1]) to express and verify temporal properties. The paper also presents a verification tool prototype for SDL which implements these ideas.
Work supported by the European project INTERVAL IST-1999-11557, Formal Design, Validation and Testing of Real-Time Telecommunications Systems (http://www.cordis.lu/ist/projects/99-11557.htm) and by the French RNRT Project PROUST (http://www-verimag.imag.fr/PROUST/).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
B. Algayres, Y. Lejeune, and F. Hugonnet. GOAL: Observing SDL behaviors with GEODE. In R. Braek and A. Sarma, editors, SDL’95 with MSC in CASE. Elsevier Science B.V., 1995.
R. Alur, C. Courcoubetis, and D.L. Dill. Model checking in dense real time. Information and Computation, 104(1):2–34, 1993.
S. Bornot and J. Sifakis. Relating time progress and deadlines in hybrid systems. In International Workshop HART’97, volume 1201 of LNCS. Springer-Verlag, 1997.
S. Bornot, J. Sifakis, and S. Tripakis. Modeling urgency in timed systems. Technical report, Verimag, Grenoble, 1998.
M. Bozga, J.C. Fernandez, L. Ghirvu, S. Graf, J.P. Krimm, L. Mounier, and J. Sifakis. IF: An intermediate representation for sc SDL and its applications. In R. Dssouli, G.v. Bochmann, and Y. Lahav, editors, SDL’ 99. The Next Milenium. Proceedings of the 9th SDL Forum, Montreal, Canada, 1999. Elsevier.
Marius Bozga, Susanne Graf, Alain Kerbrat, Laurent Mounier, Iulian Ober, and Daniel Vincent. SDL for real-time: What is missing? The 2nd Workshop on SDL and MSC, 2000.
M. Diefenbruch, E. Heck, J. Hintelmann, and B. Müller-Clostermann. Performance evaluation of SDL systems adjunct by queueing models. In R. Braek and A. Sarma, editors, Proceedings of SDL Forum’95. Elsevier Science B.V., 1995.
A. En-Nouaary, R. Dssouli, and F. Khendek. From timed scenarios to SDL: specification, implementation and testing of real-time systems. In R. Dssouli, G.v. Bochmann, and Y. Lahav, editors, SDL’ 99. The Next Milenium. Proceedings of the 9th SDL Forum, Montreal, Canada, 1999. Elsevier.
Y. Gurevich. Evolving algebra: The lipari guide. In E. Börger, editor, Specification and Validation Methods. Oxford University Press, 1995.
Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya. What’s decidable about hybrid automata? Journal of Computer and System Sciences, 57(1):94–124, 1998.
John E. Hopcroft and Jeffrey D. Ullman. Introduction to Automata Theory, Languages, and Computation. Adisson-Wesley, 1979.
ITU-T. Annex F (11/00) to recommendation Z.100-Specification and Description Language (SDL)-Formal definition of SDL-to be published.
ITU-T. Recommendation Z.100 (11/99)-Specification and Description Language (SDL).
I. Ober. Extending SDL with timed automata concepts. Technical report, VERILOG, 1999.
J.-L. Roux. SDL performance analysis with ObjectGEODE In A. Mitschele-Thiel, B. Müller-Clostermann, and R. Reed, editors, Workshop on Performance and Time in SDL and MSC, Erlangen, Germany, February 1998. Friedrich-Alexander Universität, Erlangen-Nürnberg.
SpaceWire Working Group. SpaceWire-Serial point-to-point links. European Space Agency document UoD-DICE-TN-9201, Issue D, May 2000. http://www.estec.esa.nl/tech/spacewire.
TELELOGIC A.B., Malmö, Sweden. Telelogic TAU SDL Suite Reference Manuals, 1999.
Stavros Tripakis. The Formal Analysis of Timed Systems in Practice. PhD thesis, Joseph Fourier University, Grenoble, 1998.
VERILOG, Toulouse, France. ObjectGEODE 4.1 Reference Manuals, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ober, I., Kerbrat, A. (2001). Verification of Quantitative Temporal Properties of SDL Specifications. In: Reed, R., Reed, J. (eds) SDL 2001: Meeting UML. SDL 2001. Lecture Notes in Computer Science, vol 2078. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48213-X_12
Download citation
DOI: https://doi.org/10.1007/3-540-48213-X_12
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42281-5
Online ISBN: 978-3-540-48213-0
eBook Packages: Springer Book Archive