Formale Techniken der Software-Entwicklung
Aktuelles
- Zu den Übungsblättern 4 und 6 gibt es jetzt (endlich, sorry!) Musterlösungen.
- Die Mündlichen Prüfungen finden am 21. und 22.7. statt. Falls Sie auf UniWorX zur Vorlesung angemeldet sind, sollten Sie eine E-Mail mit Informationen zur Anmeldung und individuellen Terminvergabe bekommen haben. Falls nicht, wenden Sie sich bitte umgehend an den Übungsleiter.
- Übungsblatt 6 ist online. Es wird am 06.06.2014 besprochen.
- Das vierte Übungsblatt ist online. Es wird am 23.05. besprochen.
- Die Übung am 09.05.2014 entfällt.
- Der dritte Foliensatz ist online.
- Der zweite Foliensatz ist online.
- Das zweite Übungsblatt ist online. Es wird am 25.04. besprochen.
- Der erste Foliensatz und das Übungsblatt sind online (siehe unten).
Inhalte
Die Entwicklung zuverlässiger Soft- und Hardware stellt immer noch ein großes Problem dar. Aufgrund der Komplexität moderner Systeme gibt es viele Fehler, die nur in wenigen Systemzuständen oder in bestimmten Interaktionen mit der Umgebung auftreten. Durch Tests sind diese Fehler nur schwer zu finden. Für kritische Systeme bietet sich daher der Einsatz von Techniken an, die es Entwicklern ermöglichen, Eigenschaften systematisch zu spezifizieren und das fertige System aus der Spezifikation zu generieren oder die Eigenschaften des Systems gegenüber der Spezifikation zu verifizieren.
In dieser Vorlesung werden logische Grundlagen und formale Techniken der Software-Entwicklung behandelt. Neben dem grundlegenden Verständnis für formale Methoden liegt ein Schwerpunkt auf praktisch anwendbaren Techniken und Werkzeuge zur formalen Spezifikation und Verifikation. Geplant sind die folgenden Themen:
- Boole'sche Logik und Erfüllbarkeit, SAT Solving (mit CVC/Yices)
- Einführung in die Prädikatenlogik und Logiken höherer Ordnung (mit Alloy)
- Spezifikation von Systemen (mit PVS)
- Logik-Programmierung, Constraint-Programmierung und Constraint-Solving (mit Eclipse)
- Ausblick in die Behandlung von zeitbasiertem Verhalten, Model Checking
Termine
Vorlesung (3-stündig)
- Mo 9ct-12 Uhr, Richard-Wagner-Str. 10, Raum 101
Übung (2-stündig)
- Fr 12ct-14 Uhr, Richard-Wagner-Str. 10, Raum 101
Mündliche Prüfungen
- Die Termine für die mündlichen Prüfungen stehen noch nicht fest.
Personen
Dozent
Übungsbleitung
Materialien
Vorlesung
Übung
Hörerkreis
Benötigte Vorkenntnisse
Literatur
