5. Folge: Beschreibung von Estelle

Die formale Spezifikationsmethode Estelle wurde etwa zeitgleich zu Lotos ebenfalls von der ISO entwickelt. Estelle basiert auf einem Systemmodell, das mittels kommunizierender Module das Gesamtverhalten eines Systems beschreibt. Dabei werden die einzelnen Module durch erweiterte endliche Automaten (extended finite state machines) beschrieben. Die hierzu in Estelle verfügbaren Konzepte werden in dieser Folge im einzelnen erläutert.

Wie Lotos entstand auch Estelle aus der Notwendigkeit, formale Beschreibungsmethoden für die OSI-Protokollspezifikationen zur Verfügung zu haben. Während Lotos eine sehr abstrakte, algebraische FDT darstellt, ähnelt Estelle weitgehend einer modernen prozeduralen Programmiersprache. Dieser Unterschied mag ein Grund für die Koexistenz zweier von der ISO entwickelter FDTs sein.

Das Systemmodell von Estelle

Im Systemmodell von Estelle wird das Verhalten von Modulen durch erweiterte endliche Automaten (extended finite state machines) beschrieben. Zu den bei endlichen Automaten üblichen Zuständen, Ereignissen, Transitionen und damit verknüpften Aktionen kommen in Estelle Bedingungen (Prädikate), Ereignisse mit Parametern, Prioritäten zwischen den Transitionen und interne, das heißt nicht von (äußeren) Ereignissen abhängige Transitionen hinzu.

Letztere werden als spontane Transitionen bezeichnet. Bei ihnen kann durch Angabe einer Zeitspanne der Zeitpunkt festgelegt werden, zu dem sie nach Erfüllung ihrer sonstigen Voraussetzungen frühestens oder spätestens durchgeführt werden sollen. Dadurch können zeitüberwachte Wartezustände einfach spezifiziert werden.

Darüber hinaus können zu einem gegebenen Zeitpunkt mehrere Transitionen schaltbar (enabled) sein. Unter den verschiedenen Möglichkeiten wird diejenige mit der höchsten Priorität oder bei gleichen (oder fehlenden) Prioritäten eine beliebige ausgewählt und durchgeführt. Dadurch ergibt sich ein nicht-deterministisches Automaten-Modell.

Jedes Modul wird in Estelle durch eine Substrukturierung in Untermodule oder unmittelbar durch einen endlichen Automaten beschrieben. Bei der Substrukturierung kann jedes Modul ein oder mehrere Untermodule haben, die sich eventuell wieder in Untermodule gliedern. Auf diese Art entsteht eine Hierarchie von Modulen, durch die in Estelle die Interaktionsmöglichkeiten und das Benutzen exportierter Variablen durch andere Module festgelegt ist. Nur Module mit einer Vater-Kind-Beziehung und Module, die denselben unmittelbaren Vorfahren haben, können untereinander in Interaktion treten und exportierte Variablen benutzen. Die Interaktionsfähigkeit mit einem anderen Modul kann allerdings innerhalb eines Moduls an Untermodule weitergereicht werden.

Module können miteinander interagieren, das heißt Interaktions-Primitive austauschen. Dazu kann jedes Modul einen oder mehrere (externe1) Interaktionspunkte haben, die zusammen mit dem Modul definiert werden und Bestandteil der äußeren Sichtbarkeit eines Moduls sind.

Darüber hinaus kann ein Modul einen Teil seiner internen Daten und/ oder Prozeduren nach außen sichtbar machen (exportieren), so daß diese von anderen Modulen benutzt werden können. Auf das Problem der Synchronisation, das sich dabei prinzipiell stellt, kommen wir weiter unten zurück.

Das Interagieren zweier Module setzt eine Verbindung zwischen ihnen voraus. Estelle benutzt zur Verbindung zwischen Modulen Kanäle, welche die möglichen Interaktionen zweier über sie verbundener Module festlegen.

Dazu werden Kanal-Typen definiert, welche die Möglichkeiten zwischen den Endpunkten eines Kanals, das heißt zwischen den über diesen Kanal verbundenen Interaktionspunkten bestimmen, sowie die unterschiedlichen Zuständigkeiten der Endpunkte für die einzelnen Interaktionen festlegen. Mit jedem Kanal-Typ werden deshalb zwei Rollen definiert, die das mögliche Verhalten der Endpunkte im Hinblick auf das Absetzen und Entgegennehmen von Interaktions-Primitiven definieren. Typische Rollen sind Service-User und Service-Provider.

Bei der Definition eines Interaktionspunktes wird der Kanal-Typ angegeben und die Rolle bestimmt, die er bei einer möglichen Verbindung übernimmt. Dies stellt sicher, daß nur "zueinander passende" Interaktionspunkte über einen Kanal verbunden werden können.

In Estelle werden abstrakte Modul-Typen und konkrete Instanzen von Modul-Typen unterschieden. Die Definition eines Modul-Typs erfolgt in zwei Schritten. Zunächst werden in einer Modul-Header-Definition die nach außen sichtbaren, statischen Eigenschaften eines Moduls festgelegt. Dies sind die Modul-Klasse (siehe unten), die externen Interaktionspunkte, formalen Parameter und die exportierten internen Variablen des Moduls. Im zweiten Schritt werden in einer oder mehreren Modul-Body-Definitionen die dynamischen Eigenschaften eines Moduls festgelegt. Darunter ist das Verhalten beziehungsweise die Gesamtheit aller möglichen Verhaltensweisen eines Modul-Typs zu verstehen.

Eine Instanz eines Modul-Typs wird durch Ausführen eines Init-Statements erzeugt. Dabei wird eine bestimmte Verhaltensweise für das Modul ausgewählt; wenn in der Definition eines Modul-Typs mehrere angegeben sind. Das so geschaffene Modul existiert als konkrete Ausprägung eines Modul-Typs solange, bis es von dem Modul, das es kreiert hat, durch Ausführen eines Release-Statements wieder beendet wird. Durch die Angabe mehrerer Modul-Body-Definitionen für einen Modul ist es möglich, daß verschiedene Instanzen desselben Modul-Typs unterschiedliche konkrete Verhaltensweisen haben.

Mit jedem Interaktionspunkt eines Moduls ist eine Eingabewarteschlange (Queue) fest verknüpft, die zum Modul gehört. Sie nimmt die Interaktionen für einen Interaktionspunkt auf und speichert sie bis zur Verarbeitung durch das Modul. Alle Queues in Estelle sind FlFO-Queues, das heißt die jeweils älteste Interaktions-Primitive wird im Modul bearbeitet und aus der Queue entfernt. Das Einordnen einer Interaktions-Primitive in eine Queue erfolgt dadurch, daß das mit einem Interaktionspunkt über einen Kanal verbundene Modul an seinen Endpunkt des Kanals, das heißt an seinen Interaktionspunkt, eine Ausgabe macht. In Estelle ist hierfür das Output-Statement vorgesehen. Durch die Festlegung, daß es an jedem Interaktionspunkt eine Queue für die eintreffenden Interaktionen gibt, ist die "atomare" Interaktion in Estelle grundsätzlich asynchron. Natürlich kann durch einen geeigneten Synchronisationsmechanismus auch synchrone Kommunikation von Prozessen spezifiziert werden.

Interaktionspunkte werden durch ein Connect- oder ein Attach-Statement mit anderen Interaktionspunkten verknüpft. Die Unterschiede zwischen beiden können anschaulich so beschrieben werden, daß durch attach ein Kanal lediglich an einem Endpunkt "verlängert", das heißt der Partner an einem Endpunkt durch einen "Stellvertreter" ersetzt wird, wogegen durch connect eine Verbindung zwischen zwei Endpunkten und damit zwei Kommunikationspartnern hergestellt wird und dadurch ein Kanal überhaupt erst kreiert wird. Eine bestehende Verbindung von Interaktionspunkten kann durch disconnect oder detach wieder aufgehoben werden.

Estelle unterstützt grundsätzlich die Spezifikation paralleler Prozesse. Zur Synchronisation stehen zunächst die Interaktionsmöglichkeiten zwischen Modulen zur Verfügung. Darüber hinaus gibt es noch die Möglichkeit einer impliziten Synchronisation. Hierfür existieren zwei Modul-Klassen in Estelle, Prozesse und Aktivitäten. Prozesse können prinzipiell parallel ablaufen, wogegen Aktivitäten nur sequentiell ablaufen können.

Durch Definition der Modul-Klasse für jedes Modul wird eine implizite Synchronisation erreicht. Weiterhin ist festgelegt, daß unabhängig von der Modul-Klasse ein Vater-Modul niemals parallel zu einem seiner Kind-Module abläuft. Durch weitere Festlegungen für die implizite Synchronisation und Nutzungsregeln für gemeinsame Daten wird garantiert, daß ein Zugriff auf gemeinsame Daten ausschließlich wechselseitig erfolgt, so daß hierfür keine besonderen Synchronisierungs-Mechanismen in einer Spezifikation definiert zu werden brauchen.

Estelle benutzt in der hier zugrundegelegten Form eine Erweiterung von Pascal. Der Grundumfang von ISO-Pascal ist vollständig in Estelle enthalten. Somit ist eine weitgehende Möglichkeit zu bekannten, imperativen Programmiersprachen gegeben.

Ähnlich wie ein Pascal-Programm hat eine Estelle-Spezifikation einen strukturierten Aufbau. Sie besteht aus einem Deklarationsteil, in dem alle auf äußerstem Niveau benötigten Typen und Variablen definiert werden, sowie je einem Initialisierungs-, Transitions- und Terminierungsteil für das Gesamtsystem, die jeweils auch leer sein können.

Im Deklarationsteil werden zusätzlich zu den von Pascal bekannten Deklarationen die Modul- und Kanaltypen definiert. Der formale Aufbau dieser Deklarationen ist in Bild dargestellt.

Bei der Modul-Header-Definition ist neben dem Modultypnamen die Modulklasse, process oder activity, anzugeben, sowie optional die Listen der externen Interaktionspunkte, der formalen Parameter und der exportierten Variablen. Bei jedem Interaktionspunkt ist diejenige Rolle eines Kanaltyps angegeben, die er im Fall einer Verbindung mit einem anderen Interaktionspunkt übernimmt. In der Modul-Body-Definition wird angegeben, zu welchem Modultyp sie gehört. Im Modul-Body, der wiederum aus Deklarations-, Initialisierungs-, Transitions- und Terminierungsteil besteht, wird das Verhalten des Moduls beschrieben.

Bei der Kanal-Typ-Definition sind die verschiedenen Rollen aufgeführt. Danach werden für jede Rolle die Interaktions-Primitiven aufgezählt, die ein Endpunkt, der diese Rolle übernimmt, absetzen kann. Dabei kann jede Interaktions-Primitive Parameter haben, die in der Form

Parametername: Parametertyp

in einer Parameterliste angegeben werden.

Im Initialisierungs- beziehungsweise Terminierungsteil werden diejenigen Aktionen angegeben, die beim Start beziehungsweise bei der Terminierung des Gesamtsystems oder eines Moduls durchzuführen sind. Typische Aktionen sind Kreieren oder Terminieren von Untermodulen und Herstellen oder Auflösen von Verbindungen zwischen Modulen. Eine spezielle Aktion im Initialisierungsteil ist das Setzen der Zustandsvariablen für den endlichen Automaten des Gesamtsystems oder des Moduls auf ihren Anfangswert.

Die Zustandsübergänge des endlichen Automat en weden im Transitionsteil definiert. Der formale Aufbau einer Transition in Estelle ist in Bild 2 dargestellt, jedoch sind dabei nicht alle Variationsmöglichkeiten berücksichtigt.

Darin sind alle Bestandteile bis auf trans begin end; optional und auch in der Reihenfolge weitgehend frei. Weiterhin gibt es Möglichkeiten zur abkürzenden Zusammenfassung mehrerer Transitionen, die einen Teil ihrer Klauseln gemeinsam haben, zum Beispiel from Ausgangszustand. Weitere Möglichkeiten zur verkürzten Schreibweise werden im Beispiel in der nächsten Folge angegeben. Die lokalen Definitionen in einer Transition gelten nur für die Statements zwischen begin und end.

Nachdem wir den formalen Aufbau einer Spezifikation kurz dargestellt haben, wollen wir noch auf die Möglichkeiten eingehen, gewisse Details bei der Spezifikation in Estelle offen zu lassen oder nur soweit wie nötig anzugeben. Eine davon ist der Zusatz primitive bei einer Funktions- oder Prozedurdefinition, der bei implementationsabhängigen Hilfsroutinen zum Einsatz kommt. Eine weitere Möglichkeit ist die Verwendung von . . . anstelle einer expliziten Angabe einer Konstanten.

Die Ungenauigkeit der Spezifikation, die durch die Benutzung diese Möglichkeiten entsteht, kann durch Benutzung eines bindenden Kommentars wieder soweit wie notwendig eingeschränkt werden. Ein solcher Kommentar wird anstelle von (* *) durch (/ /) begrenzt und stellt im Unterschied zum herkömmlichen Kommentar nicht nur erklärende Dokumentation dar, sonder enthält Hinweise, die bei einer Implementation zu beachten sind. Folgendes Beispiel soll dies erläutern:

const number_of_buffers = ...;

(/ number_of_buffers > 3 *

window_size /)

Dadurch bleibt die konkrete Anzahl von Puffern bei der Spezifikation zwar offen, es wird jedoch die bei einer Implementation zu treffende Festlegung der Konstante eine Nebenbedingung angegeben.

Anmerkungen:

1) Im Gegensatz dazu gibt es interne Interaktionspunkte, die außerhalb eines Moduls nicht sichtbar sind.

2) Es ist auch eine Version von Estelle in der Entwicklung, die SDL anstelle von Pascal als Grundlage hat.

*Die Autoren Klaus-Peter Fischer (Dipl.-Math.) und Stephan Hesse (Dipl.-lnform.), sind Software-Entwickler speziell für Kommunikationssysteme sowie Berater auf diesem Gebiet bei der Telenet GmbH, Geschäftsstelle Rhein-Main.

(wird fortgesetzt)

Rückblick

In den vier vorhergehenden Folgen dieser aus sieben Kapiteln bestehenden Serie wurde auf die Notwendigkeit von Spezifikationsmethoden im Hinblick auf das künftige ISDN sowie OSI-Kommunikationsprotokolle hingewiesen. Anhand von Beschreibungen und Beispielen sind bisher die Methoden SDL (Formal Description Technique) und Lotos (Language of Temporal Ordering Specification) zum Zuge gekommen. Folge 6 wird ein Beispiel in Estelle (siehe oben die Beschreibung) beinhalten, und die Schlußfolge wird die abschließende Diskussion der aufgeführten Methoden bringen.

Die bisherigen Folgen sind erschienen in CW 40/85, Seite 22 ff; CW 41/85, Seite 26; CW 42/85, Seite 26 ff und CW 43/85 Seite 24 ff.