Joachim Thees

• Die formale Spezifikation von Kommunikationssystemen stellt durch die mit ihr verbundene Abstraktion und Präzision eine wichtige Grundlage für die formale Verifikation von Systemeigenschaften dar. Diese Abstraktion begrenzt jedoch auch die Ausdrucksfähigkeit der formalen Beschreibungstechnik und kann somit zu problemunangemessenen Spezifikationen führen. Wir untersuchen anhand der formalen Beschreibungstechnik Estelle zunächst zwei solche Aspekte. Beide führen speziell in Hinsicht auf die Domäne von Estelle, der Spezifikation von Kommunikationsprotokollen, zu schwerwiegenden Beeinträchtigungen der Ausdrucksfähigkeit. Eines dieser Defizite zeigt sich bei dem Versuch, in Estelle ein offenes System wie z. B. eine Protokollmaschine oder einen Kommunikationsdienst zu spezifizieren. Da Estelle-Spezifikationen nur geschlossene Systeme beschreiben können, werden solche Komponenten immer nur als Teil einer fest vorgegebenen Umgebung spezifiziert und besitzen auch nur in dieser eine formale Syntax und Semantik. Als Lösung für dieses Problem führen wir die kompatible syntaktische und semantische Estelle-Erweiterung Open-Estelle ein, die eine formale Spezifikation solcher offener Systeme und ihres Imports in verschiedene Umgebungen ermöglicht. Ein anderes Defizit in der Ausdrucksfähigkeit von Estelle ergibt sich aus der strengen Typprüfung. Wir werden zeigen, dass es in heterogenen, hierarchisch strukturierten Kommunikationssystemen im Zusammenhang mit den dort auftretenden horizontalen und vertikalen Typkompositionen zu einer unangemessenen Modellierung von Nutzdatentypen an den Dienstschnittstellen kommt. Dieses Problem erweist sich beim Versuch einer generischen und nutzdatentypunabhängigen Spezifikation eines offenen Systems (z. B. mit Open-Estelle) sogar als fatal. Deshalb führen wir die kompatible Containertyp-Erweiterung ein, durch die eine formale Spezifikation nutzdatentypunabhängiger und somit generischer Schnittstellen von Diensten und Protokollmaschinen ermöglicht wird. Als Grundlage für unsere Implementierungs- und Optimierungsexperimente führen wir den „eXperimental Estelle Compiler“ (XEC) ein. Er ermöglicht aufgrund seines Implementierungskonzeptes eine sehr flexible Modellierung des Systemmanagements und ist insbesondere für die Realisierung verschiedener Auswahloptimierungen geeignet. XEC ist zudem mit verschiedenen Statistik- und Monitoring-Funktionalitäten ausgestattet, durch die eine effiziente quantitative Analyse der durchgeführten Implementierungsexperimente möglich ist. Neben dem vollständigen Sprachumfang von Estelle unterstützt XEC auch die meisten der hier eingeführten Estelle-Erweiterungen. Neben der Korrektheit ist die Effizienz automatisch generierter Implementierungen eine wichtige Anforderung im praktischen Einsatz. Hier zeigt sich jedoch, dass viele der in formalen Protokollspezifikationen verwendeten Konstrukte nur schwer semantikkonform und zugleich effizient implementiert werden können. Entsprechend untersuchen wir anhand des Kontrollflusses und der Handhabung von Nutzdaten, wie die spezifizierten Operationen effizient implementiert werden können, ohne das Abstraktionsniveau senken zu müssen. Die Optimierung des Kontrollflusses geschieht dabei ausgehend von der effizienten Realisierung der Basisoperationen der von XEC erzeugten Implementierungen primär anhand der Transitionsauswahl, da diese speziell bei komplexen Spezifikationen einen erheblichen Teil der Ausführungszeit bansprucht. Wir entwickeln dazu verschiedene heuristische Optimierungen der globalen Auswahl und der modullokalen Auswahl und werten diese sowohl analytisch wie auch experimentell aus. Wesentliche Ansatzpunkte sind dabei verschiedene ereignisgesteuerte Auswahlverfahren auf globaler Ebene und die Reduktion der zu untersuchenden Transitionen auf lokaler Ebene. Die Überprüfung der Ergebnisse anhand der ausführungszeitbezogenen Leistungsbewertung bestätigt diese Ergebnisse. Hinsichtlich der effizienten Handhabung von Daten untersuchen wir unterschiedliche Ansätze auf verschiedenen Ebenen, die jedoch in den meisten Fällen eine problemunangemessene Ausrichtung der Spezifikation auf die effiziente Datenübertragung erfordern. Eine überraschend elegante, problemorientierte und effiziente Lösung ergibt sich jedoch auf Basis der Containertyp-Erweiterung, die ursprünglich zur Steigerung des Abstraktionsniveaus eingeführt wurde. Dieses Ergebnis widerlegt die Vorstellung, dass Maßnahmen zur Steigerung der effizienten Implementierbarkeit auch immer durch eine Senkung des Abstraktionsniveaus erkauft werden müssen.
• The formal specification of communication systems represents an important basis for the formal verification of system properties by means of the abstraction and the precision connected with it. This abstraction limits however also the Expressiveness of the formal description technique and can lead thus to problem-inadequate specifications. We examine two such aspects on the basis of the formal description technology Estelle first. Both lead (particularly in regard to the domain of Estelle, the specification of communication protocols) to serious impairments of the expression ability. One of these deficits shows up with the attempt to specify in Estelle an open system e.g. a protocol machine or a communication service. Since Estelle specifications can describe only closed systems, such components are specified in each case as part of a given environment and therefore possess only in this environment a formal syntax and semantics. As solution for this problem we introduce the compatible syntactic and semantic Estelle extension "Open Estelle", which makes a formal specification of such open systems and their import into different environments possible. Another deficit in the expressiveness of Estelle results from the strict type checking. We will show that in heterogeneous, hierarchically structured communication systems this leads to an inadequate modelling of user data types (SDU) at the service interfaces. Estelle permits no problem-appropriate modelling of such questions. Therefore we introduce the compatible extension "Container Type", by which a formal specification is made possible. As basis for our implementation and optimization experiments we introduce the "eXperimental Estelle of Compiler" (XEC). Due to its implementation concept it supports a very flexible modelling of the system management and is in particular suitable for the realization of different selection optimizations. XEC is equipped with different statistics and monitoring functionalities, by which an efficient quantitative analysis of the accomplished implementation experiments is possible. Apart from the complete language scope of Estelle XEC supports also most of the Estelle extensions introduced here. Apart from the correctness, the efficiency of automatically generated implementations is an important requirement in the field use. We develop different heuristic optimizations of the global selection and the module-local selection and evaluate these both analytically as well as experimentally. Substantial starting points are thereby different event-controlled selection procedures on global level and the reduction of the number of relevant transitions on local level. Regarding the efficient handling of data we examine different approaches on different levels, which however in most cases require a problem-inadequate specification on the efficient data communication. A surprisingly elegant, problem oriented and efficient solution results however on basis of the container type extension, which was originally introduced for the increase of abstraction.