Verifikation Hybrider- und Echtzeitsysteme


Vorlesung mit Übungen
Wintersemester 1997/98


Vorlesung: Dienstag, 9 Uhr
Übung: Montag, 14:00 s.t Uhr

Hybride Systeme bestehen aus interagierenden diskreten und kontinuierlichen Komponenten. Man findet sie beispielweise in der Luft- und Raumfahrt, Bahnregelung oder Chemietechnik. Derartige Systeme sind oft sicherheitskritisch und müssen deshalb formal analysiert werden. In der Vorlesung wird die Theorie der hybriden und Echtzeitautomaten präsentiert sowie Fragen der Modellierung und Analyse hybrider Systeme diskutiert. Themenstichworte sind: Hybride Automaten und Echtzeitautomaten: Anwendung in der Modellierung und Verifikation. Temporale Logik: Zusammenhang mit Automaten und Anwendung in der Verifikation. Modelchecking Algorithmen: Enumerativ und symbolisch und deren Umsetzung in Werkzeugen.
Die Zielgruppe der Vorlesung sind Studierende mit Haupt- und Nebenfach Informatik

Vorläufiges Skript

Übungen

Tools

Folgenes ist eine Liste von Werkzeugen für die mechanische Überprüfung hybrider und Echtzeitsysteme. Alle Tools sind lokal installiert. Für die Nutzung dieser Tools, erweitere man seinen Pfad um ~kondisk/bin. Unter ~/kondisk finden sich auch Dokumentationen und Beispiele zu den einzelnen Tools

Bei Fragen, email an {yl|ms}@informatik.uni-kiel.de


Maintained by: Martin Steffen
Last modified: 20 November 1997