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

Fortgeschrittenenpraktikum

Erweiterung des USE-Tools

Inhalt

USE ist ein Tool zur Spezifikation von Informationssystemen. Eine USE-Spezifikation besteht hierbei aus einer Beschreibung eines Modells, welche um OCL-Ausdrücke erweitert werden kann. Die OCL-Ausdrücke spezifizieren zusätzliche Integritätsbedingungen für das Modell. Um Informationen über einen Systemzustand zu erhalten, können zu jedem Zeitpunkt OCL-Ausdrücke eingegeben und ausgewertet werden.

Im ersten Teil dieses Fortgeschrittenenpraktikums wurde der im USE-Tool integrierte Auswerter für OCL-Ausdrücke um eine korrekte Auswertung verschiedener Features erweitert, welche Bestandteil von OCL 2.0 sein werden. Insbesondere können auch Ausdrücke ausgewertet werden, welche prinzipiell mehrere verschiedene Werte als Ergebnis der Auswertung zulassen.

Im zweiten Teil wurde ein Generator für Beweisverpflichtungen (Proof obligations) in das Tool integriert. Beweisverpflichtungen spielen dann eine Rolle, wenn bewiesen werden soll, dass eine konkrete Realisierung eines Systems einer zuvor erarbeiteten Spezifikation genügt. Indem bestimmte Aspekte der Realisierung (z. B. Programmiersprache) festgelegt werden, stellen Beweisverpflichtungen ein Mittel zur Vereinfachung dieses Prozesses dar.

Materialien

• Erweitertes USE-Tool

Bearbeiter: Michael Maier
Aufgabensteller: Priv.-Doz. Dr. Rolf Hennicker
Betreuer: Dr. Alexander Knapp
Abgabe: November 2003