Ludwig-Maximilians-Universität München, Institut für InformatikDie Übersetzung von UML-Modellen in SAL-Kontexte wurde im Rahmen des Prototyp-Werkzeugs HUGO/RT implementiert. Das Werkzeug kann nun UML-Zustandsmaschinen mit Hilfe eines der SAL-Modellüberprüfer automatisch verifizieren, d. h., überprüfen, ob Interaktionen, die in bestimmten Kollaborationen ausgedrückt werden, auch tatsächlich durch eine Menge von Zustandsmaschinen realisiert werden können. Ergänzend kann eine Prüfung auf mögliche Verklemmungen durchgeführt werden. Die Ergebnisse werden in einer vereinfachten UML-Syntax an den Benutzer zurückgegeben.
Die Menge von UML-Zustandsautomaten und eine UML-Kollaboration werden in einen SAL-Kontext mit einer Beweisverpflichtung übersetzt, anschließend wird einer der SAL-Modellüberprüfer aufgerufen, um die Verifikation der Beweisverpflichtung durchzuführen. Bei der Übersetzung wird die HUGO-interne Sprache SMILE verwendet. Sie beschreibt die Semantik der UML-Zustandsautomaten mit einfachen Konstrukten. Die SAL-Abbildung unterstützt alle Elemente der SMILE-Sprache bis auf die Stoppuhr-Elemente. Aus diesem Grund können keine zeitgesteuerten Zustandsautomaten in SAL verifiziert werden.
SAL erweitert das Werkzeug HUGO/RT um die Familie der symbolischen Modellüberprüfer. Das wichtigste Ziel der Arbeit war, den unendlichen SAL-Modellüberprüfer einsetzen zu können. Er ist in der Lage, mit unendlichen Typen zu arbeiten, was bis jetzt die anderen Modellüberprüfer nicht konnten. Mit den unbegrenzten Integer- und Realtypen kann man unendliche Zustandssysteme, solche wie hybride oder zeitgesteuerte Automaten und andere Formalismen des kontinuierlichen oder echtzeitlichen Verhaltens, darstellen. Eine weitere Verbesserung brachten die SAL-Datentypen. Mit ihrer Hilfe können UML-Ereignisse semantisch sauberer implementiert werden. Ein Ereignis und seine Parameter werden auf eine einzige SAL-Konstante abgebildet.
Allerdings wurde während der Implementierung festgestellt, dass der unendliche SAL-Modellüberprüfer mit den Datentypen noch nicht kompatibel ist. Der Verzicht auf die Datentypen löst das Problem nicht. Der unendliche begrenzte Modellüberprüfer ist nicht in der Lage, Systeme mit über 40 Zustandsübergängen zu behandeln. Deswegen muss man auf die nächste Version der SAL-Modellüberprüfer warten, um in den Genuss der Unendlichkeit zu kommen.
Mehrere Fallstudien bestätigten die Behauptung, dass die symbolische Modellüberprüfung eher für Hardware als für Software geeignet ist. Schon bei einer relativ kleinen Anzahl von logischen Variablen waren die Antwortzeiten der symbolischen Modellüberprüfung nicht zufriedenstellend. Der schnellere begrenzte Modellüberprüfer scheiterte an Zustandsautomaten, die länger als 40 Zustände waren. Und SMILE-Maschinen stellen in der Regel deutlich längere Zustandsautomaten dar.
Bearbeiter:
Alexander Harhurin
Aufgabensteller:
Prof. Dr. Martin Wirsing
Betreuer:
Dr. Alexander Knapp
Fertigstellung: 21. Juni 2005
Diplomarbeiten
Lehrstuhl
Institut
Universität