Entwicklung korrekter Systeme
Stammvorlesung Realzeitsysteme
Auf dieser Seite
Inhalt
In dieser Stammvorlesung geht es um die Spezifikation von zeitkritischen Systemen. Beispiele solcher Systeme sind Steuerungen von Eisenbahnen, Robotern oder auch Gasbrennern. Bei allen diesen Systemen kommt es darauf an, daß sie bestimmte Zeitbedingungen einhalten. Bei der automatischen Steuerung einer Bahnüberganges müssen zum Beispiel spätestens 4 Sekunden nachdem die Streckensensoren einen Zug gemeldet haben, die Schranken geschlossen sein. Sind die Schranken geöffnet, sollen sie 15 Sekunden lang offen bleiben, damit Fahrzeuge den Bahnübergang sicher überqueren können
Um solche Zeitanforderungen beschreiben zu können, wurden verschiedenene Spezifikationsmethoden entwickelt. Eine besonders attraktive Methode ist der seit 1991 von Zhou Chaochen entwickelte "Duration Calculus". Es handelt sich um eine Logik und einen Kalkül, mit dem unter anderem die Dauer (engl. duration) von Zuständen gemessen werden kann. Zu Beginn dieser Vorlesung wird der Duration Calculus vorgestellt und dessen Anwendung an Hand von Beispielen erläutert. Anschließend wird eine weitere Spezifikationsmethode vorgestellt: die von Alur & Dill eingeführten Realzeitautomaten (engl. Timed Automata).
Nach der Spezifikation von Anforderungen an ein Realzeitsystem schließt sich die Verifikation von entwickelten Programmen an. Dabei werden die eingeführten Spezifikationsmethoden Duration Calculus und Timed Automata dazu benutzt, das Realzeitverhalten der Programme zu beschreiben. Anschließend kann man dann auf der Basis dieser Verhaltensbeschreibungen die Korrektheit beweisen.
Die Vorlesung führt an aktuelle Forschungsarbeiten heran und bietet somit eine gute Basis für Studien- und Diplomarbeiten im Bereich der Theoretischen Informatik.
F-Praktikum!
In diesem Wintersemester wird begleitend zur Vorlesung ein Fortgeschrittenenpraktikum Realzeitsystem von H. Dierks angeboten, das sehr zu empfehlen ist. Interessenten wenden sich bitte direkt an Herrn Dierks.
Übungsaufgaben
Sie haben hier die Möglichkeit, die aktuellen Übungsblätter zu dieser Lehrveranstaltung im Postscript- oder DVI-Format abzurufen. Wir bitten Sie jedoch im Interesse aller, die Übungsblätter nicht gedankenlos auszudrucken, insbesondere nicht auf den Laserdruckern der ARBI. Photokopien sind unter Berücksichtigung aller Kosten in der Regel günstiger als Laserdrucke!
Dieses Angebot richtet sich hauptsächlich an diejenigen, die auf anderem Wege kein Exemplar der Übungsblätter erhalten konnten.