Spezifikationstechniken
Priv.-Doz. Dr. Lothar Schmitz
Herbsttrimester 2008
[Termine] [Aktuelles] [Ziel und Inhalt der Vorlesung]
[Vorlesungsfolien und Materialien] [Übung]
Termine
Es handelt sich um eine Vorlesung mit zwei Vorlesungsstunden und einer Übungsstunde wöchentlich (2 V + 1 SÜ TWS).
Die Vorlesungen und Übungen finden jeweils in einem Termin statt:
- montags 09:45 Uhr bis 12:00 Uhr im Raum 33/2111
Aktuelles
Der erste Termin ist am Montag, dem 06. Oktober.
Krankheitsbedingt fällt die Vorlesung am Montag, den 13. Oktober aus. Nächster Vorlesungstermin ist Montag, der 20. Oktober.
Ziel und Inhalt der Vorlesung
Ziel der Vorlesung ist es, Grundkenntnisse über wichtige Methoden und Werkzeuge zur formalen Spezifikation zu vermitteln und an Beispielen und Fallstudien deren praktischen Nutzen darzustellen.
Inhalte sind insbesondere:
- Einführung: Motivation und Überblick
- Fein-Design von Java-Programmen mit JML spezifizieren
- Grob-Design von UML-Programmen mit OCL spezifizieren
- Reaktive Software mit Temporaler Logik und Model Checking behandeln
- Realzeiteigenschaften mit Giotto spezifizieren
- Software-Systeme mit Alloy spezifizieren und validieren
- Software-Systeme mit Z spezifizieren und verfeinern
- Fallstudien zu Alloy, OCL und Z
- Grundbegriffe Algebraischer Spezifikationen
- Spezifikationen und Prototypen in Maude
- Zusammenfassung
Vorlesungsfolien und Materialien
Die Vorlesungsfolien sowie weitere Materialien finden Sie hochschulöffentlich im BSCW unter Spezifikationstechniken.
Übung
Die Übung wird dazu verwendet, gemeinsam Systeme auszuprobieren oder Beispiele ausführlicher durchzugehen. Zeitlich ist die Übung in die Vorlesung integriert.