SDL Formal Semantics Project


Project Members

Key References

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 admin@sdl-forum.org.
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.

gotzhein@informatik.uni-kl.de
 		20/12/2000




 Superordinated page: Research
research activities, projects and organisations

 Feedback
Go to the contact details of the person in charge of this page

 Deutsch
This page in german. Diese Seite auf deutsch.