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