Folge 3: Beschreibung von Lotos (Language of Temporal Ordering Specification)

Formale Methoden zur Beschreibung von Protokollen

18.10.1985

Diese Folge beschäftigt sich mit "Lotos" (Language of Temporal Ordering Specification), einer formalen, Spezifikationsmethode, die in den Jahren 1981 bis 1984 von Experten der ISO entwickelt wurde. Die dieser formalen Spezifikationsmethode (Formal Description Technique = FDT) zugrundeliegende Idee ist es, ein System allein dadurch zu beschreiben, daß die von außen sichtbaren Ereignisse und ihre zeitliche Reihenfolge dargestellt werden.

Lotos ist eine formale Spezifikationsmethode, die eine abstrakte Beschreibung des von außen sichtbaren Verhaltens eines Systems ermöglicht. Den Anstoß für die Entwicklung von Lotos gab die Notwendigkeit, für die OSI-Protokollspezifikationen der ISO formale Beschreibungsmethoden zur Verfügung zu haben. Jedoch ist diese FDT allgemein für die Spezifikation von Kommunikationssystemen verwendbar.

Das Sprachmodell beruht auf einem von R. Milner an der Universität von Edinburgh entwickelten Modell kommunizierender Systeme (Calculus of Communicating Systems, CCS). Die Darstellung der abstrakten Datentypen basiert auf der Sprache ACT ONE, einer algebraischen Spezifikationssprache, die an der Technischen Universität Berlin entwickelt wurde.

Besonderer Wert wurde bei der Entwicklung dieser FDT darauf gelegt, daß ihr ein geschlossenes mathematisches Modell zugrunde liegt, das es ermöglicht, verschiedene in Lotos beschriebene Systeme auf ihre von außen beobachtbare Äquivalenz zu überprüfen (zum Beispiel Vergleich der in Lotos ausgedrückten Beschreibung der Realisierung eines Protokolls mit der auch in Lotos durchgeführten Spezifikation des Protokolls). Weiterhin soll ein solches mathematisches Modell das Testen von Protokollimplementierungen auf Einhaltung der Protokollspezifikation unterstützen.

Das Lotos zugrundeliegende Modell sieht das zu beschreibende Gesamtsystem als aus mehreren Prozessen bestehend an. Die Prozesse sind unabhängig voneinander und können an genau definierten Interaktionspunkten miteinander kommunizieren.

An diesen Interaktionspunkten werden Ereignisse ausgetauscht. Der Austausch solcher Ereignisse (eine Interaktion) erfolgt immer synchron in beiden Prozessen, das heißt eine Interaktion, kann nur stattfinden, wenn beide Prozesse dazu bereit sind.

Prozesse können ihrerseits aus Unterprozessen bestehen, die jedoch für den Benutzer des übergeordneten Prozesses nicht sichtbar sind. Dadurch ist eine schrittweise Verfeinerung bei der Beschreibung eines Systems in Lotos möglich.

Das Verhalten eines Prozesses, das heißt die Reihenfolge der Interaktionen, die er durchfuhrt, ist in einer behaviour expression festgelegt. Diese "Verhaltensausdrücke" sind wie arithmetische Ausdrücke einer höheren Programiersprache aufgebaut. Jedoch sind hier Operatoren wie "Parallelausführung" oder "Auswahl" anstelle der gewohnten arithmetischen Operatoren zu finden.

Wir wollen im folgenden den Aufbau dieser behaviour expressions genauer beschreiben. Danach befassen wir uns noch mit den Variablen und Datentypen in Lotos.

Die in behaviour expressions zulässigen Operatoren wirken ihrerseits wieder auf behaviour expressions, so daß eine behaviour expression im allgemeinen aus mehreren untergeordneten behaviour expressions besteht. In der Terminologie von Lotos beschreibt eine behaviour expression das Verhalten eines Prozesses. Wenn sich eine behaviour expression aus mehreren Teilausdrücken zusammensetzt, ist dies so zu interpretieren, daß sich das beschriebene Gesamtverhalten aus der Zusammensetzung aller Verhaltensweisen, die durch die Teilausdrücke beschrieben werden, ergibt.

Tabelle 1 listet die Operatoren, die in behaviour expressions vorkommen können. Im weiteren werden wir sie einzeln erläutern.

____________________________________________________________

Operator Bedeutung

____________________________________________________________

for D choice B Summation (n-stellige Auswahl)

B1 >> B2 Enable

B1 [> B2 Disable

B1 II B2 Parallelausführung

B1 [] B2 Auswahl

[C] -> B Bedingte Ausführung (Guarding)

A ; B Action perfix Interaktion)

B N [G] Restriktion

____________________________________________________________

Tabelle 1: Operatoren in behaviour expressions

Dabei sind B, B1 und B2 ihrerseits wieder behaviour expressions. C ist ein Boolescher Ausdruck, D eine Laufvariablendeklaration, G eine Liste von Interaktionspunkten und A eine Interaktionsangabe.

Zunächst zur Parallelausführung. Der Operator zeigt an, daß die beiden Prozesse, die durch die Operanden beschrieben sind, zeitlich parallel ausgeführt werden. Das Verhalten des Gesamtprozesses setzt sich also aus dem Verhalten der Einzelprozesse zusammen.

Es gibt verschiedene Varianten des Paralleloperators, die sich darin unterscheiden, auf welche Weise die beiden Teilprozesse miteinander kommunizieren können. Der in Tabelle 1 angebenene Operator erlaubt die Kommunikation beider Prozesse über alle Interaktionspunkte, die sie beide gemeinsam benutzen. Andere (hier nicht aufgeführte) Operatoren verlangen die genaue Auflistung aller Interaktionspunkte, die die beiden Prozesse für Kommunikation untereinander benutzen können oder geben an, daß beide Prozesse nicht untereinander kommunizieren, sondern nur unabhängig voneinander mit der Umwelt kommunizieren.

"behaviour expressions" zur Auswahl

Der Auswahl- oder Summationsoperator in seiner zweistellig oder n-stelligen Form gibt an, daß mehrere behaviour expressions zur Auswahl stehen, um das Verhalten des Prozesses zu beschreiben. Welche der möglichen Verhaltensformen ausgewählt wird, hängt von dem nächsten auftretenden Ereignis ab. Die n-stellige Auswahl (for D choiceB) sieht für die Laufvariable vor, daß sie alle Werte eines Datentyps (in der Lotos-Terminologie: einer Sorte) oder die Namen von verschiedenen Interaktionspunkten annehmen kann. Es stehen dann alle Ausprägungen der folgenden behaviour expression mit den verschiedenen Werten für die Laufvariable zur Auswahl.

Der Enable-Operator ist als Hintereinanderausführung von Subprozessen zu interpretieren. Es wird, zuerst der durch den linken Operanden beschriebene Prozeß ausgeführt. Nach seiner erfolgreichen Beendigung wird der rechte Prozeß gestartet, bei Ergebnis-Werte von links nach rechts übertragen werden können.

Der Disable-Operator wird im Sinne eines Interrupt benutzt. Im Normalfall bestimmt der linke Operand das Verhalten des Gesamtausdrucks. Wenn jedoch ein Ereignis auftritt, das vom rechten Operanden akzeptiert werden kann (wenn dieser also in Interaktion treten kann), wird der linke Prozeß (irreversibel) unterbrochen und der rechte Operand bestimmt alleine das nachfolgende Verhalten.

Bei der bedingten Ausführung kann das durch den rechten Operanden beschriebene Verhalten nur dann wirksam werden, wenn der als linker Operand angegebene Boolesche Ausdruck wahr ist. Ist jedoch der durch den rechten Operanden beschriebene Prozeß einmal "angelaufen" (hat er also seine erste Interaktion durchgeführt), so ist die Bedingung im weiteren Verlauf nicht mehr wirksam.

Der Restriktionsoperator dient dazu, für den linken Operanden Interaktionspunkte einzufahren die nach außen hin nicht sichtbar werden. Das ist dann nützlich, wenn im linken Operanden Subprozesse enthalten sind, die miteinander kommunizieren sollen, ohne daß dies nach außen sichtbar werden soll.

Die Action-Prefix-Schreibweise schließlich dient der Angabe der Interaktionen selbst, die von dem beschriebenen Prozeß ausgeführt werden sollen. Sie ist so zu interpretieren, daß die Interaktion; die als linker Operand angegeben ist, zuerst durchgeführt werden muß, bevor der rechte Operand das Verhalten des Gesamtprozesses bestimmt. Der rechte Operand wird seinerseits im allgemeinen wieder Interaktionen enthalten, so daß auf diese Weise eine zeitliche Reihenfolge von Interaktionen beschrieben wird.

Den Operatoren ist eine Priorität zugeordnet, die in Tabelle 1 von oben nach unten zunimmt. Daher müssen sich, auch behaviour expressions mit mehr als einem Operator einfach schreiben und interpretieren. Wenn einmal eine andere Gruppierung als die durch die Prioritäten implizierte benötigt wird, ist die Klammerung, wie aus der Arithmetik bekannt, vorgesehen.

Es gibt nur wenige atomare behaviour expressions, die auf unterster Ebene eines komplexen Ausdrucks überigbleiben. Sie sind im folgenden aufgeführt.

stop führt dazu, daß ein Prozeß stehenbleibt. Er kann danach keine Interaktion mehr durchfuhren. Von außen ist nichts mehr von seiner Existenz zu sehen. Der Umgebung des Prozesses wird auch keine Mitteilung über sein Stehenbleiben gemacht.

exit dagegen zeigt die erfolgreiche Beendigung eines Prozesses an. Sie kann verwendet werden, um dem Enable-Operator anzuzeigen, daß sein linker Operand erfolgreich beendet wurde und nun der rechte Operand zu starten ist. exit kann benutzt werden, um Ergebnisse des Prozesses in die Außenwelt zu transportieren.

Weiterhin kann auf unterer Ebene einer behaviour expression der Start eines an anderer Stelle definierten Prozesses angegeben sein. Diesem Prozeß können Parameter in Form von Variablen und Namen von Interaktionspunkten übergeben werden. Syntaktisch gleicht eine solche Prozeßinkarnation einem Funktionsaufruf in einer höheren Programmiersprache.

Es bleibt noch anzugeben, in welcher Form die Interaktionen spezifiziert werden. Dazu wollen wir noch einmal kurz auf das zugrundeliegende Konzept eingehen. Interaktionen finden immer paarweise zwischen zwei Prozessen und gleichzeitig in beiden Prozessen statt. Die Angabe einer Interaktion erfolgt in der Form IP !Ausdruck ?Variable. . .

Dabei ist IP der Name eines Interaktionspunktes. "!Ausdruck" und, "?Variable" können in beliebigen Reihenfolge und beliebig oft wiederholt (oder auch überhaupt nicht) auftreten. Dabei ist !Ausdruck so zu interpretieren, daß der im Ausdruck berechnete Wert am Interaktionspunkt zur Verfügung gestellt wird. ?Variable dient dazu, in der Variablen den Wert abzulegen, den ein Interaktionspartner zur Verfügung gestellt hat. Die Zuordnung der Parameter von beiden Interaktionspartnern geschieht durch die Reihenfolge der Parameter.

Voraussetzung für eine Interaktion ist, daß beide Partner den gleichen Interaktionspunkt angeben. Ferner muß, falls bei diesen Partnern an gleicher Stelle der Parameterliste ein !Ausdruck steht, der Wert der beiden Ausdrücke übereinstimmen. Das kann dazu benutzt werden, nur bestimmte Ereignisse an einem Interaktionspunkt auszuwählen. In unserem Beispiel, das im nächsten Beitrag dieser Serie folgt, wird bei jeder Interaktion eine Ereigniskennung in dieser Weise benutzt.

Wesentlich ist bei dem Konzept der Interaktionen die Synchronität und die fehlende Unterscheidung nach Sender und Empfänger. Es können Interaktionen auftreten, bei denen beide Partner nur !Ausdrücke haben oder bei denen bei beiden Partnern !Ausdrücke und ?Variablen vorkommen, also bidirektionaler Informationsaustausch erfolgt.

Nun wollen wir wie angekündigt noch auf die Variablen und Datentypen in Lotos eingehen. Es ist wichtig zu wissen, daß Lotos eine rein applikative Sprache ist. Das heißt das wesentliche Konzept ist die Anwendung von (möglicherweise rekursiven) Funktionen auf Variablen. Eine Variable, der in Lotos einmal ein Wert zugewiesen wurde, kann diesen Wert nicht m(...)ändern. Es gibt auch keine Wertzuweisungen im Sinne der herkömmlichen Programmiersprachen, vielmehr erhalten Variablen einen Wert nur in Interaktionen, Funktionsaufrufen und ähnliche zugewiesen.

In Lotus abstrakte Datentypen

Die Datentypen sind in Lotos als abstrakte Datentypen spezifiziert. Ein Datentyp besteht also aus einer oder mehreren Sorten (Wertemengen) und aus Operationen darauf. Sowohl die Sorten als auch die Operationen darauf werden in einer abstrakten algebraischen Notation beschrieben. Hierfür ist in Lotos, wie oben bereits erwähnt, der Formalismus von ACT ONE vorgesehen, jedoch ist auch jeder andere Formalismus zur Spezifikation abstrakter Datentypen verwendbar. Wir wollen hier darauf nicht näher eingehen, da auch bei der Spezifikation unseres Beispielprotokolls mittels Lotos abstrakte Datentypen nur in geringem Umfang und in trivialen Ausprägungen vorkommen werden.

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