Arbeitsgruppe Rechnernetze Fachbereich Informatik, Universität Kaiserslautern

Personelle Zusammensetzung

Kurzbeschreibung der Arbeitsgruppe

Forschungsvorhaben

Gegenstand dieses Forschungsvorhabens, das dem SFB 501-Teilprojekt B4 "Generische Kommunikationssysteme" zugeordnet ist, ist die Bereitstellung einer Entwicklungsumgebung zur Konfigurierung formaler Protokollentwurfsspezifikationen im Sinne eines Protokollbaukastensystems. Wesentlicher Bestandteil des Protokollbaukastensystems ist eine Sammlung wiederverwendbarer und formal fundierter Protokollbausteine sowie ein zugehöriges Prozeßmodell zur Erfassung der Entwicklungsmethodik.

Angelehnt an das aus der objektorientierten Softwaretechnik bekannte Entwurfsmusterkonzept, liegen die Protokollbausteine in Form sog. SDL Muster vor, die generische Lösungsstrukturen für wiederkehrende, kommunikationsspezifische Teilaufgaben auf Basis der von der ITU standardisierten Beschreibungstechnik SDL (Specification and Description Language) darstellen. Zur Definition von SDL Mustern wurde ein Beschreibungsrahmen entwickelt, der neben einer natürlichsprachlichen Formulierung des zu lösenden Entwurfsproblems und der generischen SDL Lösungsstruktur auch Anforderungen an die einbettende Kontextspezifikation, resultierende Mustereigenschaften sowie erlaubte Verfeinerungen der Musterinstanz nach deren Einbettung umfaßt. Die initiale Mustersammlung sowie das zugehörige Prozeßmodell wurden durch verschiedene Fallstudien aus dem Kommunikationsbereich erprobt und weiterentwickelt. Desweiteren kamen sie auch im SFB 501 Praktikum (in Kooperation mit SFB 501-Teilprojekt B5) zur Steuerung einer Modelleisenbahn zum Einsatz. Der bestehende Konfigurierungsprozeß unterstützt einen inkrementellen Protokollentwurf auf Basis von SDL Mustern und umfaßt außerdem eine anschließende Validierung der formalen Entwurfsspezifikation sowie eine automatische Prototypengenerierung. Ein musterbasierter Entwurfsschritt gliedert sich dabei weiterhin in Selektion, Adaption und Komposition von Protokollbausteinen. Eine Werkzeugunterstützung zur Verwaltung und Anwendung von SDL Mustern ist in Arbeit.

In Kooperation mit den SFB 501-Teilprojekten A1 und B1 wurde eine Instrumentierung des Konfigurierungsprozesses erarbeitet, die als Grundlage für eine experimentelle Evaluierung und systematische Weiterentwicklung des Protokollbaukastensystems dient und in laufenden Fallstudien zum Einsatz kommt. Die gewonnenen Erkenntnisse und analysierten Meßdaten sollen in der zentralen SFB-Erfahrungsdatenbank des SE-Labors abgelegt werden und dienen als Grundlage für nachfolgende Software-Entwicklungsprojekte.

Im Rahmen dieses Forschungsvorhabens, das dem Teilprojekt B4 des SFB 501 zugeordnet ist, wird das Protokollbaukastensystem des Forschungsschwerpunktes "Generische Entwicklung von Kommunikationsprotokollen" für die Maßschneiderung echtzeitfähiger Kommunikationssubsysteme weiterentwickelt und zusätzlich durch die Realisierung echtzeitfähiger Kommunikationsplattformen auf unterschiedlichen Basistechnologien (Token-Ring, CAN, ATM) praktisch erprobt.

Dabei konnte z.B. ein früher entwickeltes Quality of Service (QoS)-Architekturmmodell als wertvoller Bestandteil eines generischen Systemanalysemodells etabliert werden. Ebenso führten Erfahrungen mit der musterbasierten Spezifikation verschiedener Ressourcenreservierungsprotokolle (Eigenentwicklungen auf Basis dezentral verwalteter Ressourcen und ein Reengineering des Internet-Stream Protokolls ST2+) zur Erweiterung des Baukastens um einen Framework für Reservierungsprotokolle.

Mit dem Entwurf und der Implementierung eines CAN-basierten Echtzeitkommunikationssubsystems wurden die im Teilprojekt SFB 501/ B4 entwickelten unterschiedlichen Generik-Konzepte (Protokollbaukasten, inkrementelles Prozeßmodell zur Konfigurierung von Kommunikationsprotokollen, QoS-Architekturmodell) erstmalig in einer realen Produktentwicklung durchgängig und integriert eingesetzt. Dabei konnten Teile des implementierten Kommunikationssubsystems automatisch aus der konfigurierten SDL Entwurfsspezifikation generiert werden.

Bei der Entwicklung zuverlässiger Softwaresysteme ist der Einsatz formaler Beschreibungstechniken (FDTs) unerläßlich. Durch ihre formale Syntax und Semantik erlauben sie eine präzise Beschreibung der spezifizierten Systeme und bilden so die Grundlage für die Verifikation funktionaler und nicht-funktionaler Aspekte. Bei der praktischen Implementierung solcher Softwaresysteme wird jedoch meist auf Handkodierung zurückgegriffen, obwohl dies sehr aufwendig ist und die Übertragbarkeit der nachgewiesenen Eigenschaften der Spezifikation auf die handkodierte Implementierung in Frage stellt. Zwar existieren bereits Werkzeuge zur automatischen Generierung von Prototypen direkt aus formalen Spezifikationen, doch haben diese den Ruf, ineffiziente Kodierungen zu erzeugen. Es gibt jedoch kaum empirische Daten über den tatsächlichen Effizienzgewinn durch eine Handimplementierung gegenüber einer automatisch generierten Implementierung.

Ziel dieses DFG-Forschungsprojekts ist es, Methoden und Werkzeuge zur effizienten Implementierung von formal spezifizierten Softwaresystemen zu entwickeln und zu vergleichen. Im Vordergrund steht dabei die FDT Estelle, die speziell zum Entwurf von Kommunikationsproto- kollen entwickelt wurde. Es wird zunächst in einer Bestandsaufnahme die Leistungsfähigkeit existierender Compiler anhand praktischer Fallbeispiele untersucht und mit vergleichbaren Handimplementierungen in Beziehung gesetzt. Eines dieser Fallbeispiele ist das Hochgeschwindigkeitprotokoll Xpress Transport Protocol (XTP). Mit Hilfe der dabei gewonnenen Erkenntnisse und Methoden werden zeitintensive Konstrukte identifiziert und ihre automatische Implementierung optimiert. Grundlage dafür ist der in der Arbeitsgruppe neu entwickelte Kodegenerator XEC (eXperimental Estelle Compiler), der speziell auf die Analyse und Optimierung des Laufzeitverhaltens der generierten Prototypimplementierungen zugeschnitten ist und die automatische Generierung effizienter Implementierungen erlaubt.

Estelle ist eine formale Beschreibungstechnik zur Spezifikation verteilter informationsverarbeitender Systeme, insbesondere von Kommunikationsdiensten und -protokollen. Von der International Standardization Organization (ISO) entwickelt, besitzt Estelle seit 1989 den Status einer internationalen Norm. Forschungsaktivitäten der AG Rechnernetze in diesem Bereich sind auf den praktischen Einsatz und die Weiterentwicklung von Estelle ausgerichtet. Einige der im Berichtszeitraum durchgeführten Arbeiten werden nachfolgend aufgeführt.

Die formale Beschreibungstechnik (FDT) Estelle dient speziell zur Beschreibung von Kommunikationsprotokollen zwischen verteilten, konkurrierenden, kommunizierenden Systemen. Eine der Schwächen von Standard-Estelle ist die Tatsache, daß Estelle nur (topologisch) geschlossene Systeme beschreiben kann. Offene Systeme können nur eingebettet in eine Umgebung dargestellt werden. Dies macht es unmöglich, einzelne Komponenten wie Protokollmaschinen oder Netzwerkdienste abstrakt, also unabhängig von einer konkreten Umgebung formal zu spezifizieren und den Einsatz dieser offenen Systeme in verschiedenen Umgebungen separat zu beschreiben.

Im Rahmen eines DFG-Projekts wird die Estelle Erweiterung "Open Estelle" entwickelt, die diese Schwäche beseitigen soll. Sie soll eine formale Beschreibung offener Systeme (unabhängig von einer konkreten Umgebung) und deren Einsatz in verschiedenen Umgebungen erlauben. Die Beschreibung der offenen Systeme muß formal sein, d.h. sie muß eine formale Syntax und eine formale Semantik besitzen. Dies erlaubt die Ableitung von Eigenschaften offener Systeme unabhängig von ihrem konkreten Einsatz. Open Estelle soll außerdem den Einsatz automatisch generierter Prototypen formal spezifizierter Systeme in existierenden realen Umgebungen unterstützen. Die formale Semantik von Open Estelle wird dabei die Grundlage für die Entwicklung eines Implementierungsbegriffs für offene Systeme bilden.

Messungen an Protokollen zeigten, daß gegenwärtig bei automatisch generierten Implementationen die Transitionsauswahl und die Kommunikation zwischen verteilten Modulen viel Laufzeit kosten. Der Spezifikationsstil der "leichtgewichtigen Submodule" reduziert die Zahl der Transitionen und der Module und damit die Laufzeitkosten. Weiterhin ermöglicht er in Estelle auch bisher nicht übliche Kommunikationsformen. Darüberhinaus wurde die Transformation einer Spezifikation in einen laufzeiteffizienteren Stil weiter ausgearbeitet. Die zugehörige kleine, kompatible Spracherweiterung erlaubt im übrigen allgemein zusätzliche Strukturierungsmöglichkeiten für Spezifikationen.

Im Bereich der Signalisierung in Telefonsystemen ("Anruf-Ablaufsteuerung") kommt es seit kurzem zu verstärkten Bemühungen der Hersteller, die existierenden Systeme zu öffnen und zu sogenannten Intelligenten Netzwerken (IN) auszubauen. Ziel ist es, auf der Grundlage der vorhandenen Basissysteme ein weites Spektrum von neuen Diensten und Leistungsmerkmalen (Features) schnell und kostengünstig einführen zu können, auch durch Drittanbieter. Dabei zeigt sich immer drängender das Problem, daß diese Vielzahl an neuen Features auch in unerwünschter Weise interagiert und sich in ihrer Funktionalität gegenseitig behindert. Die mathematische Formalisierung der bisher in der Literatur nur unscharf verwendeten Begriffe "Feature" und "Feature-Interaktionen" wurde abgeschlossen. Auf ihr basieren automatentheoretische Kriterien, die geeignet sind, solche Interaktionen aufzuspüren, und Methoden, um sie aufzulösen. In Fallstudien wurden eine Reihe von Features zu einem in Estelle spezifizierten Telefonsystem hinzugefügt. Dieses und ein bereits früher spezifiziertes Telefonsystem wurden mit den Werkzeugen Confine und Decfine nach den Kriterien erfolgreich und vollständig analysiert, wobei außer den bekannten auch einige vorher unbekannte Feature-Interaktionen gefunden wurden. Anschließend konnten die Interaktionen aufgelöst werden. Auf diese Weise wurde die Durchführbarkeit des vorgeschlagenen Ansatzes für Telefonsysteme nichttrivialer Größe erfolgreich nachgewiesen.

Ähnlich strukturierte Anteile in Anforderungs- bzw. Dienstspezifikationen lassen sich in Form von wiederverwendbaren Mustern abstrahieren. Ein für den Anforderungsbereich erarbeitetes Vorgehensmodell enthält einen zyklischen Prozeß, in den u.a. Teilaufgaben wie die Erstellung einer Sammlung von Anforderungsmustern sowie deren Wiederverwendung (durch Selektion, Adaption, Komposition) eingebettet sind.

Ziel der Mustersammlung ist es, die bei der Entwicklung gesammelten Erfahrungen zu sichern und für die Verwendung in nachfolgenden Anwendungsentwicklungen zugänglich zu machen. Um die Wiederverwendbarkeit der Anforderungsmuster in der Mustersammlung zu verbessern, wurde ein Beschreibungsrahmen vorgegeben. Die Verwendung dieses Rahmens vereinheitlicht die Musterbeschreibungen durch die Vorgabe bestimmter Felder für die formale Musterdefinition sowie deren Übersetzung in natürliche Sprache, Hinweise für potentielle Anwendungsfälle und semantische Eigenschaften. Die Mustersammlung enthält derzeit vorwiegend Muster zur Beschreibung von unterschiedlichen zeitlichen Invarianzen und von Antwortzeitschranken.

Für die musterbasierte Spezifikation von Anwendungsanforderungen und (Echtzeit-)Kommunikationsdiensten wird als formale Beschreibungstechnik eine "echtzeitfähige" temporale Logik verwendet. Die Entscheidung für eine eigenschaftsorientierte Technik unterstützt zum einen die erwünschte Abstraktion von Entwurfsdetails, zum anderen ermöglicht sie eine größere Nähe zwischen den oft eigenschaftsorientiert formulierten Anwendungsanforderungen und Kommunikationsdiensten und erleichtert so den Übergang von der Anforderung zum Dienst.

Zur Ableitung des Kommunikationsdienstes werden die Anwendungsanforderungen auf eine verteilte Architektur, die auch explizite Komponenten zur Kommunikation beinhaltet, abgebil- det. Aus dieser detaillierteren Beschreibung lassen sich die Anforderungen an das Kommunikationssystem extrahieren. Zum Nachweis der Korrektheit ist zu zeigen, daß die resultierende Beschreibung die ursprünglichen Anwendungsanforderungen erfüllt. Dazu wird ein auf logischer Implikation aufbauender Korrektheitsbegriff verwendet.

Bei kompositionalen und inkrementellen Ansätzen zur Systementwicklung können auf jeder Beschreibungsebene (Anforderungen, Dienste, Protokolle) unerwünschte Konflikte zwischen den komponierten Bausteinen auftreten. Es werden gegenwärtig Kriterien zur Konflikterkennung- und behandlung bei Anforderungs- und Kommunikationsdienstbausteinen erforscht. Die Verwendung temporaler Logik ermöglicht die Rückführung des Konfliktbegriffes auf den Erfüllbarkeitsbegriff für die komponierten Formeln. Im allgemeinen müssen hierbei recht komplexe Zeitverhältnisse, Abhängigkeiten zwischen den Prädikaten sowie architekturelle Randbedingungen berücksichtigt werden. Unter Verwendung solcher Richtlinien ist es möglich, eine Klassifikation in konfliktfreie und konfliktgefährdete Kompositionen vorzunehmen und bestehende Konflikte z.B. über die Vergabe von Prioritäten zu behandeln.

Die vorgestellten Arbeiten sind angesiedelt im SFB 501-Teilprojekt B4 in Kooperation mit Teilprojekt C1.

Veröffentlichungen

Mitarbeit in Gremien

• Gotzhein, R.: Internationaler Workshop "Advanced Intelligent Networks (AIN'97)" in Cesena, Italien, 4. - 5.7.1997
• Gotzhein, R.: Internationale Konferenz "Formal Methods for Open Object-based Distributed Systems", Canterbury, UK, 21. - 23.7.1997
• Gotzhein, R.: International IFIP-Konferenz "Formal Description Techniques / Protocol Specification, Testing, and Verification (FORTE/PSTV'97)", Osaka, Japan, 18.-21.11.1997

• Geppert, B.: SDL Forum Society
• Gotzhein, R.: SDL Forum Society
• Rößler, F.: SDL Forum Society

Rechnerausstattung

Die Arbeitsgruppe verfügt über ein Cluster von SUN-Workstations sowie über rechnergestützte Werkzeuge zur Entwicklung von Kommunikationssystemen.

Praktika

Im Mittelpunkt des Praktikums steht die Anwendung und Vertiefung von Kenntnissen, die im Rahmen der Kernveranstaltung "Rechnernetze" vermittelt werden. Es werden eine Reihe von Kommunikationsprotokollen in der formalen Beschreibungssprache Estelle spezifiziert und mit Hilfe des rechnergestützten Werkzeugs EDT simuliert. Ferner werden die Protokolle methodisch getestet und unter Verwendung des Werkzeugs Pet/Dingo verteilt ausgeführt. Arbeitsumgebung ist der SUN-Cluster der AG Rechnernetze.

Kontakte zu ausländischen Universitäten

• Kanada: Universite de Montreal, Montreal, Quebec
• Frankreich: Institut National des Telecommunications, Evry

Fachbereich Informatik

AG Rechnernetze

Veröffentlichungen

Jahresbericht 1997

rn_www@rn.informatik.uni-kl.de

13.04.98