On the Formal Semantics of SDL-2000: A Compilation Approach Based on an Abstract SDL Machine

R. Eschbach, U. Glässer, R. Gotzhein, A. Prinz

in: Y. Gurevich, P.W. Kutter, M. Odersky, L. Thiele (Eds.): Abstract State Machines - Theory and Applications, Lecture Notes in Computer Science 1912, Springer, 2000


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, and has been broadly used in industry for many years. Efforts to define the semantics of SDL-2000 formally have started early in 1998. By now, a draft formal semantics is available, which is determined to become the offcial formal SDL semantics after its approval in 2000. It is based on the formalism of Abstract State Machines (ASMs), which has been selected for several reasons including intelligibility and executability.

The formal semantics of SDL addresses the static semantics, transformation rules, and the dynamic semantics. The approach taken to define the dynamic semantics is particularly interesting. Although basically being operational, it differs from existing approaches in several ways. In this paper, we address and highlight some of these differences, using a simplified specification language called SSL instead of SDL. In defining a formal dynamic semantics for SSL, we formally describe an abstract machine, a compilation function mapping SSL specifications to code of this machine, and an operational definition of the set of initial states, using ASM as the underlying formalism. Furthermore, we present in some detail the semantics of SSL procedure calls.

Full paper


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

This page in german. Diese Seite auf deutsch.