Formale Techniken in der Software-Entwicklung
Aktuelles
Inhalte
Ein bedeutsames und derzeit noch unbefriedigend beherrschtes Problem im Entwicklungsprozess technischer Systeme ist die Zuverlässigkeit der Software. Diese ist nur dann gegeben, wenn ein Softwaresystem im Sinne der Anforderungen korrekt funktioniert und auch auf Fehler angemessen reagiert. Besonders in sicherheitskritischen Anwendungsgebieten, wie etwa bei medizinischen Systemen, Transport (Bahn, Flugzeug, Auto), aber Automatisierungstechnik und Robotik, ist es entscheidend, dass die verwendeten Programmsysteme zuverlässig und sicher arbeiten. In einigen dieser Bereiche sind formale Methoden mittlerweile vorgeschrieben oder empfohlen.
Die Vorlesung betrachtet Methoden und Techniken zum Entwurf sicherer Systeme, die es erlauben das Verhalten eines Systems präzise zu beschreiben und zu prüfen. Der Einsatz formaler Methoden wird anhand von zwei verbreiteten Werkzeugen, Maude und Uppaal, gezeigt und vertieft. Für eine mehr daten-orientierte Spezifikation und Verfeinerung von Systemen mit abstrakten Datentypen und Termersetzung wird Maude verwendet. Uppaal wird zur Modellierung, Simulation und Verifikation von nebenläufigen Systemen eingesetzt, die auf Basis von gezeiteten Zustandsautomaten modelliert werden.
Die wesentlichen Themen der Vorlesung sind wie folgt:
- Daten-orientierte Spezifikationsentwicklung (Abstrakte Datentypen, Wechsel der Datenstruktur)
- Spezifikation dynamischer Systeme (Transitionssysteme, modell-basierte Spezifikationen)
- Verifikation und Verfeinerung nebenläufiger Systeme (Eigenschaften von Abläufen, Temporale Logik, Spezifikation von Zeitverhalten, Model Checking)
Hörerkreis
Studierende im Haupt- und Nebenfach Informatik.
ETCS-Punkte
Master Informatik: 6 ETCS-Punkte
Benötigte Vorkenntnisse
Grundkenntnisse in Informatik und Logik.
Termine
Vorlesung (3-stündig)
- Montag 9-12 Uhr, Oettingenstr. 67, 115
Übung (2-stündig)
- Freitag 12-14 Uhr, Oettingenstr. 67, 123
- Beginn am 20.4 !
Personen
Dozent
Übungsleiter
Materialien
- Vorlesung
