Aktuell
- 2006-04-13: Termin der Klausureinsicht: Montag, 24. Apr, 11:00 Uhr (in meinem Zimmer, E5 im Keller).
Inhaltsüberblick
Termine
| Mo 11-13 Uhr |
Oe 0.37 |
Vorlesung |
| Di 12-14 Uhr |
Oe 1.27 |
Vorlesung |
| Fr 10-12 Uhr |
Oe 1.27 |
Übung |
Thema der Vorlesung
Ein bedeutsames und derzeit noch unbefriedigend beherrschtes Problem im Entwicklungsprozess technischer Systeme ist die Zuverlässigkeit der produzierten Software. Diese ist gegeben, wenn ein Softwaresystem im Sinne der Aufgabenstellung funktioniert und auch auf Fehler angemessen reagiert. Besonders in sicherheitskritischen Anwendungsgebieten, wie etwa bei medizinischen Anwendungen, bei Zahlungssystemen, elektronischer Kommunikation, Zugangskontrollsystemen, aber auch Gasbrennersteuerungen im Haushalt, ist es entscheidend, dass die verwendeten Programmsysteme zuverlässig und sicher arbeiten. Die Vorlesung gibt eine Einführung in Methoden und Techniken zum Entwurf sicherer Systeme. Besonderes Gewicht wird dabei auf Techniken der Spezifikation und der Verfeinerung von Spezifikationen gelegt, die die Grundlage für moderne Validierungs- und Verifikationswerkzeuge bilden. Insbesondere werden folgende Themen behandelt:
- Daten-orientierte Spezifikationsentwicklung (Abstrakte Datentypen, Wechsel der Datenstruktur, CASL)
- Spezifikation dynamischer Systeme (Transitionssysteme, modell-basierte Spezifikationen, Invarianten, Vor- und Nachbedingungen, Z)
- Verifikation und Verfeinerung nebenläufiger Systeme (Eigenschaften von Abläufen, Temporale Logik, Model Checking, TLA)
Die Vorlesung wendet sich an Studierende im Haupt- und Nebenfach Informatik. Der Schein gilt für die Diplom-Hauptprüfung im Haupt- und Nebenfach Informatik. Der Schein gilt auch für die Hauptprüfung für das Lehramt an Gymnasien im Erweiterungsfach Informatik.
Personen
Die Vorlesung wird im Wintersemester 2005/06 gehalten von
Die Übungen werden betreut von
