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
