Folge 6: Estelle-Spezifikationen des Beispielprotokolls

Formale Methoden zur Beschreibung von Protokollen

08.11.1985

Diese Folge behandelt die Estelle-Spezifikation des Beispielprotokolls. Dabei kommt nur ein Teil der Möglichkeiten von Estelle zum Tragen, da aus Gründen der Überschaubarkeit auf eine weitergehende Detaillierung im Beispiel verzichtet werden muß. Dennoch lassen sich einige Merkmale von Estelle daran aufzeigen.

Die Spezifikation in unserem Beispiel bettet die darin definierte Version des vereinfachten D-Kanal-Protokolls, das in der ersten Folge dieser Artikelserie erläutert wurde, in eine Umgebung mit einem nicht näher spezifizierten User und einem nicht näher spezifizierten Link-Layer ein. Das Modul, welches das D-Kanal-Protokoll realisiert, wird dabei nochmals unterteilt, so daß die in Bild 1 gezeigte Modulkonfiguration entsteht.

Die Spezifikation beginnt mit dem Deklarationsteil (Bild 2). Zunächst sind die zur Verbindung mit einem User und dem Link-Layer notwendigen Kanäle definiert, die hier als Network access point und Link access point bezeichnet sind.

Für jeden Kanal-Typ sind die Rollen user und provider und die jeweils definierten Interaktions-Primitive, die hier gerade den Dienstprimitiven entsprechen, angegeben. In unserem Beispiel haben die Dienstprimitive keine Parameter.

Darauf folgen die Definitionen der Modul-Typen, nämlich User type, Link type und D channel type. Für alle drei ist die Modulklasse als process definiert. Die Modultypen haben weder formale Parameter, noch exportieren sie irgendeine Variable. User type und Link type haben jeweils einen, D channel type hat zwei Interaktionspunkte, die mit N bzw. L bezeichnet sind. Bei den Interaktionspunkten ist jeweils eine Rolle eines Kanaltyps spezifiziert. Aufgrund der Angaben liegt bereits an dieser Stelle der Spezifikation fest, daß nur die jeweils mit N und L bezeichneten Interaktionspunkte miteinander verbunden werden können.

Für jeden Modultyp ist danach eine Modul-Body-Definition angegeben. Dabei sind die Definitionen für User type und Link type als external deklariert. Dadurch wird angezeigt, daß sie nicht Bestandteil dieser Spezifikation sind. Auf diese Weise ist es möglich, bei der Spezifikation in Estelle weitgehend flexibel vorzugehen. Eine konkretisierte Modul-Body-Definition kann in einer anderen Spezifikation für User body und Link body vorgenommen werden.

Die Modul-Body-Definition für D channel type ist im Beispiel in konkretisierter Form angegeben. Sie müßte an dieser Stelle der Spezifikation folgen, ist aber aus Gründen der Übersichtlichkeit in Bild 3 enthalten.

Die darauf folgenden drei Variablendeklarationen auf äußerstem Niveau im Bild 2 bilden den Abschluß des Deklarationsteils der Spezifikation. Der Typ der Variablen ist jeweils ein weiter oben definierter Modul-Typ. Solche Variablen werden in Estelle benutzt, um eine Instanz eines Moduls zu repräsentieren. Sie haben standardmäßig den Wert undefined und bekommen in einem Init-Statement, durch welches die Modulinstanz kreiert wird, erst einen konkreten Wert zugewiesen.

An dieser Stelle der Spezifikation sind alle notwendigen Deklarationen erfolgt, insbesondere die Kanal- und Modultypen definiert. Es existiert jedoch weder ein Modul noch ein Kanal. Erst im nachfolgenden Initialisierungsteil der Spezifikation werden die einzelnen Module kreiert und die Verbindung zwischen ihnen hergestellt.

Die drei Init-Statements erzeugen je eine Instanz jedes Modultyps und weisen den Variablen Link, User und D-channel einen konkreten Wert zu. Diese Variablen können im weiteren ähnlich wie Pointer-Variablen in PASCAL zum Referenzieren der so kreierten Modulinstanzen benutzt werden. In den beiden Connect-Statements geschieht dies, um die Interaktionspunkte der Module, die miteinander verbunden werden sollen, zu bezeichnen.

Die Ausführung eines Connect-Statements kann verstanden werden als das Kreieren einer Instanz eines Kanals, dessen Typ durch die Definition der beiden angegebenen Interaktionspunkte impliziert wird. So betrachtet erzeugt das erste connect

eine Instanz des Kanaltyps Network access point und das zweite connect eine Instanz vom Typ Link access point. Mit der Initialisierung des Gesamtsystems ist die Spezifikation für das Beispiel beendet.

Nun wenden wir uns der Spezifikation von D channel body zu (Bild 3). Sie beginnt mit den lokalen Deklarationen. Als erstes wird dort der interne Kanal-Typ Internal interface und der interne Modul-Typ. Analyse Create type mit externer Modul-Body-Definition deklariert.

Ein Modul dieses Typs soll im Beispiel die Umsetzung von PDUs (Protocol-Data-Units) des D-Kanal-Protokolls in Interaktions-Primitive desselben Namens und umgekehrt bewerkstelligen. Dies ist im vorliegenden Fall trivial, so daß auf die Angabe einer expliziten Modul-Body-Definition verzichtet wird.

Der interne Kanal-Typ dient dazu diese Interaktionen zwischen dem Analyse-Create-Modul und dem D channel-Modul auszutauschen.

Im Anschluß an die Definitionen der Kanal- und Modultypen werden die möglichen Werte für den Zustand des erweiterten endlichen Automaten festgelegt, der das Verhalten von D channel body definiert Dies geschieht durch Definition der Variablen mit dem reservierten Namen state als Pascal-enumerated-type.

Weitere Deklarationen definieren einen internen Interaktionspunkt vom Typ Internal interface, für den die Rolle user festgelegt wird, und eine Modul Variable vom Typ Analyse Create type.

Danach folgt die Definition von zwei Funktionen, compatible und busy. Sie sind nach Pascal-Konvention definiert, jedoch durch die Zusätze pure und primitive ergänzt, die in PASCAL nicht vorgesehen sind. Durch den Zusatz pure wird angegeben, daß die Funktionen keine Seiteneffekte haben. Der Zusatz primitive anstelle des Funktionsblocks gibt an, daß es sich um Hilfsfunktionen handelt, die eine triviale Aufgabe erfüllen und implementationsabhängig spezifiziert werden. Es wird angenommen, daß die Routinen die gleichnamigen Bedingungen des D Kanal-Protokolls abprüfen und als Booleschen Wert zurückliefern sollen.

Auf den Deklarationsteil folgt der Initialisierungsteil, eingeleitet durch initialize, der beim Erzeugen einer Instanz des Modultyps durchgeführt wird. Der Zustand des endlichen Automaten wird hier auf seinen Anfangswert Null gesetzt was durch die to-Klausel bewirkt wird, und danach das interne Modul Analyse-Create generiert dessen externer Interaktionspunkt I mit dem gerade definierten inneren Interaktionspunkt verbunden wird. Dies erfolgt durch ein connect-Statement.

Da dieses Modul PDUs empfangen und senden soll, die in Interaktionen des Link access point eingebunden sind, muß der Datenstrom vom und zum Link-Layer, der am Interaktionspunkt L des D-channel-Moduls erwartet wird, zu diesem Modul weitergeleitet werden. Dies geschieht durch das attach-Statement.

Im Anschluß an die Initialisierung wird das dynamische Verhalten des Moduls mittels eines erweiterten endlichen Automaten spezifiziert. Die möglichen Zustandsübergänge des Automaten sind im Transitionsteil der Modul-Body-Definition angegeben, der an dieser Stelle der Spezifikation folgen müßte, zur besseren Überschaubarkeit allerdings in Bild 4 dargestellt ist.

Der Transitionsteil wird eingeleitet durch trans, wobei in einer Transition jeweils durch das Schlüsselwort from der Ausgangs-, durch to der Zielzustand und durch when das auslösende Ereignis in Form einer Interaktion an einem Interaktionspunkt angegeben ist. Danach wird die auszuführende Aktion zwischen begin und end spezifiziert. Bei der Definition der Transitionen sind einige Abkürzungsmöglichkeiten von Estelle ausgenutzt, zum Beispiel mehrere Ausgangszustände für eine Transition.

Besonders erläutert werden muß der Teil der Beschreibung, der die im Zustand Null auf ein eintreffendes Set-up folgenden Zustandsübergänge betrifft. Eingeleitet durch das Schlüsselwort provided ist dort bei jeder Transition eine Bedingung hinzugefügt. Durch provided otherwise wird wie in einem chase-Statement der Komplementärfall zu allen übrigen explizit aufgeführten Bedingungen derselben Schachtelungsebene angesprochen. Die durch provided eingeleitete Bedingung muß erfüllt sein, damit eine Transition ausgeführt werden kann.

In allen nicht-trivialen Aktionen des Transitionsteils dieses Beispiels wird eine Interaktion durchgeführt. Im output-Statement, das hierfür in Estelle vorgesehen ist, wird jeweils der Interaktionspunkt und die auszuführende Interaktion angegeben in der Form

output lokaler Interaktionspunkt.

Interaktionsprimitive Durch ein output-Statement wird die Interaktionsprimitive in die Eingabewarteschlange des Interaktionspunktes am anderen Ende des Kanals gestellt, mit dem der lokale Interaktionspunkt verbunden ist.

Mit der Definition des endlichen Automaten ist die Spezifikation von D channel body abgeschlossen.

Es soll nochmals hervorgehoben werden, daß mit dem Kreieren eines Moduls die Ausführung des jeweils in der Modul-Body-Definition angegebenen Initialisierungsteils verbunden ist. Im Beispiel bedeutet dies, daß beim Erzeugen des Moduls D channel (Bild 2) implizit das interne Modul Analyse Create kreiert wird, die Verbindung der Interaktionspunkte innerhalb von D channel hergestellt werden und sich der endliche Automat von D channel im Zustand Null befindet, so daß sich die in Bild 1 dargestellte Konfiguration ergibt.

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