Statische Verifikation von Softwareprotokollen

Diese Arbeit stellt ein Verfahren zur statischen Überprüfung von Regeln über die erlaubten Ausführungsfolgen von Operationen in komponentenorientierten Softwaresystemen vor. Das Verfahren verifiziert die Implementierung eines Systems gegen eine in der Regel unvollständige Spezifikation der erlaubten Ausführungsfolgen - die Softwareprotokolle. Die Schwerpunkte liegen hierbei auf der Praktikabilität und Skalierbarkeit des Verfahrens, die durch eine effiziente Spezifikationstechnik, ein hierarchisches Verifikationsverfahren und eine adaptive Programmanalyse erreicht werden.