The Semantics of Programming Languages: A transformational/ operational approach using Abstract State Machines

R. Eschbach, R. Gotzhein, A. Prinz

International Workshop on Abstract State Machines, Monte Verita, Switzerland, March 2000, TIK-Report Nr. 87, ETH Zurich, pp. 131-151


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 dis- tributed 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 ocial 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.



Zu den Kontaktdetails des Verantwortlichen dieser Seite

This page in english. Diese Seite auf englisch.