Estelle

Einsatz und Weiterentwicklung von Estelle

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.

Open Estelle

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.

Spezifikationsstil und Laufzeiteffizienz

Die Laufzeiteffizienz von Implementationen, die automatisch aus Spezifikationen generiert wurden, ist oft unzureichend. Ein geeigneter Spezifikationsstil kann die Laufzeiteffizienz verbessern. Dies kann z.B. durch die Reduzierung "teurer" Struktur geschehen, oder durch das Ausnutzen aller probleminhärenten Nebenläufigkeit.

Zusicherungen

Es wurde untersucht, wie in Estelle Zusicherungen über Eigenschaften einer Spezifikation integriert werden können. Die explizite Angabe solcher Zusicherungen (Invarianten) kann einerseits die automatische Analyse unterstützen, und sie kann andererseits als Hilfe für das Testen genutzt werden. Es wurde eine kompatible Spracherweiterung entworfen, die es erlaubt, solche Zusicherungen in Spezifikationen einzufügen. Dabei wurde darauf geachtet, daß der Änderungsaufwand für existierende Werkzeuge wie etwa Kodegeneratoren gering bleibt.

	Übergeordnete Seite: Forschung
	Forschungsaktivitäten, Projekte und Organisationen

	Feedback
	Zu den Kontaktdetails des Verantwortlichen dieser Seite

	English
	This page in english. Diese Seite auf englisch.