Verifikation verteilter Systeme mit Produktnetzen

Die Verifikation eines verteilten Systems hat das Ziel, Fehler beim Entwurf eines solchen Systems frühzeitig zu erkennen. Basis dafür ist eine formale Systemspezifikation. Speziell im Bereich der Kommunikationsprotokolle muß eine solche Spezifikation alle beteiligten Instanzen umfassen. Beschrieben werden Produktnetze, die im Institut für Telekooperationstechnik der GMD in Darmstadt entwickelt und erprobt wurden. Es handelt sich dabei um ein formales Beschreibungsmittel für verteilte Systeme. Das sind beschriftete Petrinetze, die einerseits eine hinreichende Ausdrucksstärke zur Spezifikation realer Systeme gewährleisten und andererseits die Berechnung des Erreichbarkeitsgraphen (Menge aller möglichen Systemzustände mit ihren Übergängen) als Basis für die Analyse des dynamischen Verhaltens eines spezifizierten Systems ermöglichen. Zwei Beispiele für konkrete Produktnetze werden vorgestellt: die Spezifikation eines Kanals zum Transport von Nachrichten und das Produktnetz mit dem Alternating-Bit-Protokoll. Zur Unterstüzung von Spezifikation und Verifikation mit Produktnetzen wurde ein Werkzeug, die Produktnetzmaschine, entwickelt. Die Funktionsweise dieses Werkzeugs wird beschrieben.