Die Erreichbarkeitsanalyse zur Validierung komplexer Kommunikationsprotokolle

Unzuverlässige oder fehlerhafte Software in Programmen und Kommunikationsprotokollen hat immer wieder Softwarekrisen hervorgerufen. Unentdeckte Entwurfsfehler gefährden auf der Ebene der Implementierung das korrekte Verhalten von Rechensystemen und Datenverbindungen und können zu katastrophalen wirtschaftlichen Schäden oder nichttolerierbaren Risiken führen. Um dem Protokollentwickler zu helfen, vorhandene Fehler frühzeitig zu finden und zu beseitigen (Validierung) sowie die Defektfreiheit von Protokollen nachzuweisen (Verifikation), gibt es das systematische Verfahren der Erreichbarkeitsanalyse, mit dessen Hilfe schon auf der Ebene des Entwurfs alle möglichen Verhaltensweisen eines Kommunikationsprotokolls simulativ untersucht werden können. Allerdings ist dieses Verfahren für realistische und komplexe Protokolle wegen der großen Datenmengen und langen Rechenzeiten nicht ohne weiteres praktikabel einsetzbar. In diesem Buch wird die Erreichbarkeitsanalyse verfeinert. Es werden neue Modelle und Algorithmen hergeleitet, mit deren Hilfe die Datenmengen und Rechenzeiten soweit reduziert werden können, dass die Erreichbarkeitsanalyse für realistische Protokolle praktisch anwendbar wird. Diese Verfahren bilden die Grundlage für das neu entwickelte Validierungswerkzeug PROVAL (Protokoll-Validierung). Mit PROVAL ist die Validierung komplexer, realistischer Protokolle möglich, wie exemplarisch am Beispiel des OSI-Protokolls für verteilte Transaktionsverarbeitung (OSI-TP) gezeigt wird.