edoc-Server der Humboldt-Universität zu Berlin

Habilitationsschrift

Autor(en): Andreas Prinz
Titel: Formal Semantics for SDL – Definition and Implementation
Gutachter: Egon Börger; Joachim Fischer; Klaus Bothe
Erscheinungsdatum: 23.05.2001
Volltext: pdf (urn:nbn:de:kobv:11-10022308)
Fachgebiet(e): Informatik
Schlagwörter (ger): Formale Semantik, SDL, Spezifikationssprache, ASM, Compilerbau, lex, yacc, kimwitu
Schlagwörter (eng): formal semantics, SDL, specification language, abstract state machines, compiler construction, lex, yacc, kimwitu
Einrichtung: Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II
Zitationshinweis: Prinz, Andreas: Formal Semantics for SDL – Definition and Implementation; Habilitationsschrift, Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II , publiziert am 23.05.2001, urn:nbn:de:kobv:11-10022308
Metadatenexport: Um den gesamten Metadatensatz im Endnote- oder Bibtex-Format zu speichern, klicken Sie bitte auf den entsprechenden Link. Endnote   Bibtex  
print on demand: Wenn Sie auf dieses Icon klicken, können Sie ein Druckexemplar dieser Publikation bestellen.
Diese Seite taggen: Diese Icons führen auf so genannte Social-Bookmark-Systeme, auf denen Sie Lesezeichen anlegen, persönliche Tags vergeben und Lesezeichen anderer Nutzer ansehen können.
  • connotea
  • del.icio.us
  • Furl
  • RawSugar

Abstract (ger):
In dieser Habilitationsschrift wird die formale Semantik der standardisierten Spezifikationssprache SDL (Specification and Description Language) beschrieben. Da SDL eine sehr umfangreiche Sprache ist, wurde eine repräsentative eingeschränkte Sprache RSDL (Restricted SDL) ausgewählt, um die Konzepte der formalen Definition von SDL darzustellen. Die vorliegende Habilitationsschrift umfaßt zwei große Teile: die Definition der formalen Semantik von RSDL und ihre Implementierung. Die formale Definition der Semantik von RSDL ist verständlich, leicht mit der informalen Beschreibung zu vergleichen und repräsentiert die grundsätzliche Vorstellung von RSDL. Für die Beschreibung werden zwei Teile unterschieden, nämlich die statische Semantik und die dynamische Semantik. Die statische formale Sprachdefinition besteht aus einer konkreten Syntax, einer Menge von Korrektheitsbedingungen, einer Menge von Transformationsregeln und einer abstrakten Syntax als Basis für die dynamische Semantik. Das Ergebnis der statischen Beschreibung ist eine Repräsentation der Spezifikation in abstrakter Syntax. Die Formalisierung der dynamischen Semantik beginnt mit der abstrakten Syntax. Aus dieser abstrakten Syntax wird ein Verhaltensmodell abgeleitet, das auf der mathematischen Theorie der Abstrakten Zustandmaschinen ASM (Abstract State Machines) basiert. Um die Definition der Semantik besonders übersichtlich zu gestalten, wird eine Spezielle Abstrakte Maschine (SAM) unter Nutzung von ASM definiert. Diese abstrakte Maschine stellt eine abstrakte SDL-Maschine dar. Die formale Semantik beschreibt die Eigenschaften von SDL exakt. Um jedoch herauszufinden, ob die Semantik korrekt ist, muß sie mit der Sprachbeschreibung und den Intentionen der Sprachentwickler verglichen werden. Dies geschieht am einfachsten durch eine korrekte Implementierung der Semantik. Die Implementierung der formalen Semantik basiert auf einer Repräsentation der Eingabe als abstrakter Syntaxbaum. Um die Semantik mit minimalem Aufwand zu implementieren, werden existierende Werkzeuge verwendet. Der Compiler wird mit den Standardwerkzeugen lex und yacc generiert. Nach der Syntaxanalyse wird die weitere Verarbeitung über dem abstrakten Syntaxbaum der Eingabe definiert. Die Verarbeitung von abstrakten Syntaxbäumen wird durch ein Werkzeug namens kimwitu erledigt. Mit der hier vorgestellten Technologie wurde die formale Semantik von RSDL implementiert. Entsprechend wird die formale Semantik von SDL implementiert.
Abstract (eng):
In this habilitation thesis the formal semantics of the standardised specification language SDL (Specification and Description Language) is described. Because of the size of the language SDL a representative subset of the language called RSDL (Restricted SDL) was selected to present the concepts of the formal definition. In this thesis two major parts are covered: the definition of the formal semantics and its implementation. The RSDL formal semantics is intelligible, easily comparable with the informal description and represents the general understanding of RSDL. We distinguish between two phases of the definition, namely the static semantics and the dynamic semantics. The static semantics comprises the definition of a concrete grammar, a set of correctness constraints, a set of transformation rules and an abstract syntax as basis for the dynamic semantics. The result of the static semantics is a representation of the specification in abstract syntax. The dynamic semantics starts with the abstract syntax. From here a behaviour model is derived based on the theory of Abstract State Machines (ASM). In order to keep the presentation intelligible a special abstract machine is defined using ASM. This abstract machine in fact represents an abstract SDL-machine. The formal semantics describes the properties of SDL exactly. However, in order to check the correctness of the formalisation, it has to be compared with the informal language description and the intentions of the language designers. This is most easily done using a correct implementation of the semantics. The implementation of the semantics is based on a representation of the input as an abstract syntax tree. For implementing the semantics with minimal effort existing tools are used. The compiler is produced using the standard tools lex and yacc. After parsing the remaining processing is defined over abstract syntax trees, which is covered by a tool called kimwitu. The formal semantics of RSDL is implemented using these tools. The same approach is applicable for SDL.
Zugriffsstatistik: Die Daten für die Zugriffsstatistik der einzelnen Dokumente wurden aus den durch AWStats aggregierten Webserver-Logs erstellt. Sie beziehen sich auf den monatlichen Zugriff auf den Volltext sowie auf die Startseite. Die Zugriffsstatistik wird nicht standardisiert erfasst und kann maschinelle Zugriffe enthalten.
 
Bei Formatversionen eines Dokuments, die aus mehreren Dateien bestehen (insbesondere HTML), wird jeweils der monatlich höchste Zugriffswert auf eine der Dateien (Kapitel) des Dokuments angezeigt.
 
Um die detaillierten Zugriffszahlen zu sehen, fahren Sie bitte mit dem Mauszeiger über die einzelnen Balken des Diagramms.
Startseite: 4 Zugriffe PDF: 5 Zugriffe PDF: 7 Zugriffe PDF: 2 Zugriffe PDF: 8 Zugriffe Startseite: 3 Zugriffe PDF: 7 Zugriffe PDF: 5 Zugriffe PDF: 3 Zugriffe PDF: 1 Zugriffe Startseite: 2 Zugriffe PDF: 7 Zugriffe Startseite: 1 Zugriffe PDF: 5 Zugriffe Startseite: 2 Zugriffe PDF: 6 Zugriffe Startseite: 3 Zugriffe PDF: 17 Zugriffe PDF: 10 Zugriffe Startseite: 1 Zugriffe PDF: 10 Zugriffe Startseite: 4 Zugriffe PDF: 21 Zugriffe Startseite: 5 Zugriffe PDF: 18 Zugriffe PDF: 9 Zugriffe Startseite: 3 Zugriffe PDF: 23 Zugriffe Startseite: 1 Zugriffe PDF: 12 Zugriffe PDF: 12 Zugriffe Startseite: 4 Zugriffe PDF: 18 Zugriffe Startseite: 22 Zugriffe PDF: 15 Zugriffe Startseite: 12 Zugriffe PDF: 8 Zugriffe Startseite: 6 Zugriffe PDF: 15 Zugriffe Startseite: 1 Zugriffe PDF: 14 Zugriffe Startseite: 4 Zugriffe PDF: 13 Zugriffe Startseite: 6 Zugriffe PDF: 16 Zugriffe Startseite: 1 Zugriffe PDF: 11 Zugriffe Startseite: 7 Zugriffe PDF: 17 Zugriffe Startseite: 13 Zugriffe PDF: 25 Zugriffe Startseite: 4 Zugriffe PDF: 28 Zugriffe Startseite: 17 Zugriffe PDF: 32 Zugriffe Startseite: 24 Zugriffe PDF: 19 Zugriffe Startseite: 7 Zugriffe PDF: 19 Zugriffe Startseite: 6 Zugriffe PDF: 16 Zugriffe
Jul
11
Aug
11
Sep
11
Oct
11
Nov
11
Dec
11
Jan
12
Feb
12
Apr
12
May
12
Jun
12
Jul
12
Aug
12
Sep
12
Oct
12
Nov
12
Dec
12
Jan
13
Feb
13
Mar
13
Apr
13
May
13
Jun
13
Jul
13
Aug
13
Sep
13
Oct
13
Nov
13
Dec
13
Jan
14
Feb
14
Mar
14
Apr
14
May
14
Jun
14
Monat Jul
11
Aug
11
Sep
11
Oct
11
Nov
11
Dec
11
Jan
12
Feb
12
Apr
12
May
12
Jun
12
Jul
12
Aug
12
Sep
12
Oct
12
Nov
12
Dec
12
Jan
13
Feb
13
Mar
13
Apr
13
May
13
Jun
13
Jul
13
Aug
13
Sep
13
Oct
13
Nov
13
Dec
13
Jan
14
Feb
14
Mar
14
Apr
14
May
14
Jun
14
Startseite 4       3       2 1 2 3   1 4 5   3 1   4 22 12 6 1 4 6 1 7 13 4 17 24 7 6
PDF 5 7 2 8 7 5 3 1 7 5 6 17 10 10 21 18 9 23 12 12 18 15 8 15 14 13 16 11 17 25 28 32 19 19 16

Gesamtzahl der Zugriffe seit Jul 2011:

  • Startseite – 163 (4.66 pro Monat)
  • PDF – 454 (12.97 pro Monat)
 
 
Generiert am 25.07.2014, 18:02:39