Ludwig-Maximilians-Universität München, Institut für Informatik
Lehr- und Forschungseinheit für Programmierung und Softwaretechnik

Diplomarbeit

Validierung von Spezifikationen für graphische Modelle durch Model Checking und andere formale Methoden

Inhalt

Message Sequence Charts sind ein Mittel, um das gewünschte Verhalten von technischen Systemen und Teilsystemen zu spezifizieren. In den Phasen Design und Implementierung werden heute graphische Modelle und automatische Codegenerierung eingesetzt, um zu lauffähigen Systemen zu gelangen. Über Tracing im simulierten und realen System können Laufzeitdaten - teilweise sogar unter Echzeitbedingungen - aufgezeichnet werden.

Es sollen die Möglichkeiten zur Verkn�pfung obiger Daten und Phasen mit Hilfe formaler Methoden erarbeitet werden. Speziell am Beispiel von Message Sequence Charts sollen die Spezifikationen mit dem Tracingoutput automatisch verglichen werden und Unterschiede samt Begründung graphisch angezeigt werden. Dazu kommen Model Checking und/oder andere geeignete formale Methoden zum Einsatz. Das CASE-Tool Trice der Firmal Protos Software GmbH steht als Testplattform zur Verfügungg, dort können die erarbeiteten Methoden integriert und an realen Beispielen getestet werden.

Als zusätzliche, fakultative Aufgabe kann per formalen Methoden ein Link zwischen den Spezifikationen und graphischen Modellen geschaffen werden. Damit könnten beispielweise erste Modelle automatisch aus MSCs generiert werden, die dann allerdings vom Entwickler noch verfeinert werden müssen.

Bearbeiter: Nikolay Dinov
Aufgabensteller: Prof. Dr. Martin Wirsing
Betreuer: Dr. Alexander Knapp, Dr. Klaus Birken (Protos Software GmbH)