Verifikation abstrakter Zustandsmaschinen

Abstract

Die Arbeit stammt aus dem Themengebiet der Anwendung formaler Methoden im Software Engineering. Als Grundlage wurde die Spezifikationssprache der Abstrakten Zustandsmaschinen (engl. abstract state machines, kurz ASMs) verwendet.

Inhalt der Arbeit ist die Entwicklung praktisch anwendbarer Werkzeugunterstützung für ASMs, sowohl für die Spezifikation, als auch für die Verifikation von Verfeinerungen. Diese macht die Entwicklung korrekter Software von einer abstrakten Anforderungsspezifikation bis hin zu einer durch schrittweise Verfeinerung gewonnenen Implementierung möglich. Der Inhalt gliedert sich in vier Teile: <br>- Definition einer 1:1-Einbettung von ASM-Spezifikationen in die Dynamische Logik (DL). Damit wird der formale Nachweis von ASM-Eigenschaften möglich. <br>- Modularisierung von Korrektheitsnachweisen für Verfeinerungen: Zwei Verfeinerungsbegriffe wurden in DL formalisiert. Ein allgemeines Modularisierungstheorem für den Korrektheitsnachweis von ASM-Verfeinerungen wurde entwickelt, das die bisher aus der Literatur bekannten Theoreme verallgemeinert. <br>- Implementierung der Ergebnisse im KIV-System, einem Spezifikations- und Verifikationswerkzeug für algebraische Spezifikationen und DL. <br>- Demonstration der praktischen Einsetzbarkeit der entwickelten Konzepte an einer großen Fallstudie aus dem Compilerbau: Diese behandelt die Übersetzung von Prolog-Programmen in Assemblercode der Warren Abstract Machine (WAM). Eine informelle Darstellung, die einen als ASM beschriebenen Prolog-Interpreter in 12 systematischen Verfeinerungen in die WAM transformiert, war vorgegeben. Die formale Spezifikation und Verifikation von 8 der 12 Verfeinerungen in 9 Monaten nahm eine großen Teil des Umfangs der Arbeit ein. Der Vergleich zu zwei anderen Fallstudien zum gleichen Thema zeigt, daß der notwendige Verifikationsaufwand durch die entwickelte Theorie für ASM-Verfeinerungen deutlich geringer war.