SDL Formal Semantics Project
- Bo Ai, Beijing University of Posts & Telecommunications (static semantics)
- Robert Eschbach, University of Kaiserslautern (dynamic semantics)
- Uwe Glässer, Microsoft Research (ASM expert, dynamic semantics)
- Reinhard Gotzhein, University of Kaiserslautern (ITU SG 10 Associate Rapporteur, dynamic semantics)
- Martin von Löwis of Menar, Humboldt University Berlin (SDL expert, data semantics)
- Andreas Prinz, DResearch, Berlin (SDL expert, project management, static and dynamic semantics)
- Ying Wang, Beijing University of Posts & Telecommunications (static semantics)
- Weilei Zhang, Beijing University of Posts & Telecommunications (static semantics)
- Yuhong Zhao, Beijing University of Posts & Telecommunications (static semantics)
- ITU-T Recommendation Z.100: Languages for Telecommunications Applications - Specification and Description Language, International Telecommunication Union (ITU), Geneva, 1999
- ITU-T Recommendation Z.100 Annex F: SDL Formal Semantics Definition, International Telecommunications Union (ITU), Geneva, 2000
- Glässer, U., Gotzhein, R., Prinz, A.: The Formal Semantics of SDL-2000 - Status and Perspectives, Computer Networks, Elsevier Sciences (accepted, to appear in 2003)
- Eschbach, R., Glässer, U., Gotzhein, R., von Löwis, M., Prinz, A.: Formal Definition of SDL-2000: Compiling and Running SDL Specifications as ASM Models, Journal of Universal Computer Science 7 (11), 2001, Springer, pp. 1025-1050
- Glässer, U., Gotzhein, R., Prinz, A.: Towards a New Formal SDL Semantics Based on Abstract State Machines, in: R. Dssouli, G.v. Bochmann, Y. Lahav (eds.), SDL'99 - The Next Millenium, Proc. of the 9th SDL FORUM, Elsevier Science B.V., Juli 1999
- Eschbach, R., Glässer, U., Gotzhein, R., Prinz, A.: On the Formal Semantics of SDL-2000: A Compilation Approach Based on an Abstract SDL Machine, in: Y. Gurevich, M. Odersky, P. Kutter, L. Thiele (Eds.), Abstract State Machines - Theory and Applications, Lecture Notes in Computer Science, Volume 1912, Springer-Verlag, 2000
Access and Further Information
To obtain access to Z.100 including Annex F, permission of the
ITU (International Telecommunication Union)
is required. Alternatively, access to these documents can be obtained
by becoming member of the SDL
Forum Society. For more information, contact Jeanne Reed at
Information on Abstract State Machines can be found on the ASM Homepage.
Formal Semantics for SDL-2000 Based on ASMs Now Approved by ITU
In November 1999, a new version of SDL (Specification and Description Language) called SDL-2000 has passed ITU, an international standardization body for telecommunication. SDL is a fairly complex, graphical formal description technique for the development of distributed systems, which has been broadly used in industry for more than 20 years. With its object-oriented features, its direct support for reuse, its integration with other development languages such as MSC and UML, its commercial tool support, and being an international standard, SDL satisfies the primary needs of many system developers.
Efforts to define the semantics of SDL-2000 formally have started at the beginning of 1998. By the end of 1998, a group of international experts had been formed, which decided to apply the Abstract State Machine formalism introduced by Yuri Gurevich. This decision has been driven by a number of design objectives including intelligibility, maintainability, expressiveness and executability. After 2 years of intensive collaboration, work has been successfully completed. In November 2000, the formal semantics document (about 350 pages) has been officially approved by ITU, and has become Annex F to Z.100, the SDL standard.
Work on the formal semantics for SDL-2000 has provided many insights. Starting from the concrete grammar, static checks of well-formedness conditions as well as transformations to replace certain language constructs had to be made precise. In fact, it turned out that these aspects became crucial to the approval of the document by ITU, and that substantial resources were needed to complete this part. In the final stage, this work has been funded by Ericsson, Motorola and Telelogic.
The dynamic semantics is given to syntactically correct SDL specifications satisfying the well-formed conditions, after all transformations have been applied. For a given SDL specification, it defines the corresponding set of computations. Due to the complexity of SDL-2000, structuring of the formal definition soon became a crucial issue. The dynamic semantics builds on a so-called SDL Abstract Machine, which is defined using ASM. Next, the transitions of the SDL specification are compiled into code executable on this machine. Finally, a distributed operating system, which initializes and executes the agents of the SDL system, is defined.
While developing the formal semantics definition, there have been numerous discussions with the SDL experts in order to reach a common understanding of the Z.100 document, to solve ambiguities, and to remove inconsistencies. These discussions had substantial impact on Z.100, in particular on the abstract syntax, the transformations, and the informal semantics. Different from the past, it is now official policy that if there is an inconsistency between the main body of Z.100 and Annex F, then neither the main body of Z.100 nor Annex F take precedence when this is corrected.
Work on the formal semantics of SDL-2000 has not just been an academic exercise, but took place in a real-life setting. The successful application of mathematical formalism to real-world problems and their approval by an international standardisation organisation is a strong selling point for having formalisms at all.
|Superordinated page: Research|
|research activities, projects and organisations|
|Go to the contact details of the person in charge of this page|
|This page in german. Diese Seite auf deutsch.|