Die folgende Beschreibung enthält die

in der formalen Beschreibungstechnik LOTOS und zwar in Full LOTOS. Die Protokollbeschreibung beschränkt sich wie bei den anderen Beschreibungen auf die virtuelle Kommunikation zwischen den Protokollinstanzen. Die Beschreibung der Datenformate ist wiederum in die Dienst- und die Protokollspezifikation integriert.

XDT - Dienstspezifikation

Die XDT-Dienstspezifikation beschreibt das Verhalten an der Dienstschnittstelle mit den Dienstzugangspunkten Sender_SAP und Receiver_SAP, die hier abkürzend durch S und R bezeichnet werden. Die Spezifikation verwendet den ressourcen-orientierten Stil, weil dadurch die Abhängigkeiten zwischen den Abläufen an den Dienstzugangspunkten genauer dargestellt werden können. Die Spezifikation besteht aus drei Hauptprozessen sender, association und receiver (siehe Abbildung 1). Sie sind folgendermaßen verknüpft:

Abbildung 1: Struktur der LOTOS-XDT-Dienstspezifikation

Die Prozesse sender und receiver beschreiben den Austausch der Dienstprimitive an den Gates S und R. Sie enthalten zwei Unterprozesse CONNECT und DATA_ TRANSFER, die die Protokollphasen darstellen. Letztere sind monolithisch beschrieben. Der Prozess association verbindet die beiden Dienstzugangspunkte und transportiert die Daten der XDATrequ-Primitive vom Sender zum Empfänger, wo sie als XDATind-Primitive dem Empfänger übergeben werden. Der Prozess association ist mit den Prozessen sender und receiver über die nichtsichtbaren Gates SA und RA verbunden. Er ist ebenfalls monolithisch spezifiziert.

Es werden zwei Datentypen eingeführt: DataType und SPType. Der Datentyp DataType beschreibt Platzhalter fur die Nutzerdaten, die mittels des XDT-Dienstes transportiert werden sollen. SPType definiert die Dienstprimitive und Funktionen zu ihrer Behandlung. Des Weiteren werden die Datentypen Boolean und NaturalNumber aus der Standardbibliothek verwendet. Den Datentyp NaturalNumber erweitern wir um die Aquivalenzrelation = und die Ordnungsrelation >. Zusätzlich führen wir noch die Konstanten 1 und 2 ein, um diese wie in den anderen Spezifikationen direkt als Sequenznummern einsetzen zu können. Diese Erweiterung benötigen wir allerdings erst in der Protokollspezifikation.

Die Prozesse sender und receiver setzen sich jeweils aus drei Unterprozessen zusammen. Die Unterprozesse CONNECT und DATA_TRANSFER beschreiben jeweils die Verbindungsaufbau- und die Datenübertragungsphase.

Die LOTOS-XDT-Dienstspezifikation unterscheidet sich noch in einem weiteren Aspekt von den anderen Spezifikationen. An jedem Interaktionspunkt werden neben den Reaktionen fur die erwarteten Ereignisse auch Reaktionen für nicht erwartete Ereignisse beschrieben. Dazu werden Identifizierungsfunktionen eingeführt, z. B. IsXDAT-requ, IsXDATind u. a., die den Wert true liefern, wenn das erwartete Ereignis anliegt. Diese Darstellung vermeidet Deadlocks bei nicht erwarteten Ereignissen, was die Robustheit der Spezifikation erhoht.

--- nach oben ---

XDT - Protokollspezifikation

Die Protokollspezifikation führt drei neue Datentypdefinitionen ein: XdtPduType, Xdt- BufferType und TimerMsgType. Die anderen Datentypen werden aus der Dienstspezifikation übernommen. Die XDT-PDUs werden im Datentyp XdtPduType spezifiziert, während der Datentyp XdtBufferType den Puffer für die DT-Kopien und die zugehörigen Operationen beschreibt. Der letzte Datentyp TimerMsgType beschreibt Timerereignisse. Des Weiteren werden die Signale ack_N, go_back_N, abort und end für die interne Kommunikation zwischen den Prozessen transfer_s und ack_handler auf der Sender- Seite eingeführt.

Der Puffer für die DT-Kopien wird durch den Datentyp XdtBufferType beschrieben. Er definiert die Operationen für das Eintragen und Entfernen der DT-PDUs sowie für das Abfragen der aktuellen Belegung. Es enthät maximal fünf DT-PDUS.

Zeit kann, wie wir oben gesehen haben, in LOTOS, nicht direkt dargestellt werden. Die Grundfunktionalität eines Timers (start, stop, timeout) kann jedoch modelliert werden. Zu diesem Zweck führen wir im Folgenden den Typ TimerMsgType, der die bekannten Funktionen eines Timers beschreibt. Den eigentlichen Timer-Prozess beschreiben wir weiter unten.

Die LOTOS-Spezifikation des XDT-Protokolls lehnt sich an die Struktur der XDT-Spezifikation in der Modellsprache an. Sie ist im ressourcen-orientierten Stil geschrieben. Die Spezifikation gliedert sich in die drei Prozesse sender, medium und receiver (siehe Abbildung 2), die über die internen Gates SM und RM miteinander verbunden sind:

Der Prozess sender mit dem Gate S zum Dienstnutzer beschreibt das Sender-Verhalten, der Prozess receiver mit dem Gate R entsprechend das Empfängerverhalten. Durch den Prozess medium wird die Kommunikation zwischen den Instanzen modelliert. Die Prozesse sender und receiver untergliedern sich entsprechend der Phasen des XDT-Protokolls weiter in die Prozesse CONNECT und DATA_TRANSFER, die nacheinander aktiviert werden

Die Prozesse CONNECT und DATA_TRANSFER enthalten weitere Prozesse. Abbildung 2 zeigt die Prozess-Struktur in den beiden Protokollphasen. Erläuterungen zu diesen Prozessen geben wir jeweils unmittelbar vor ihrer Beschreibung.

Abbildung 2: Prozess-Struktur der LOTOS-XDT-Spezifikation

Der Prozess DATA_TRANSFER setzt sich auf der Sender-Seite aus den Prozessen transfer_s, ack_handler und timer zusammen. Die Prozesse transfer_s und ack_ handler haben in etwa die gleichen Aufgaben wie in der Referenzspezifikation im Abschnitt 2.3. Da es in LOTOS keine gemeinsamen Variablen gibt, werden im Unterschied zur Referenzspezifikation alle Aktionen über dem DT-PDU-Puffer im Prozess transfer_s ausgeführt. Die beiden Prozesse tauschen dazu über das interne Gate Q die Signale ack_N, go_back_N, abort und end aus.

Der Prozess medium modelliert die Übertragung. Er besteht aus zwei gegenläufigen Kanälen. Bei der Übertragung können PDUs verloren gehen.

Der Empfänger-Teil entspricht in seiner Struktur der Referenzspezifikation. Er besteht ebenfalls aus zwei Prozessen CONNECT und DATA_TRANSFER für die Protokollphasen, zwischen denen die Variablen conn und eom übergeben werden.

--- nach oben ---