Stammvorlesung "Realzeitsysteme"

 

1 Organisatorisches

Form: 4 VL + 2 Ü    (9 ECTS-Punkte)

Vorlesung:    E.-R. Olderog

Montag 8-10, A7 Hörsaal F,    Beginn: 8.4.2002
Dienstag 14-16, A7 Hörsaal F

Übungen:    J. Hoenicke

Montag 12-14, A5 1-160

Auch als Modul für den Schwerpunkt "Eingebettete Systeme" geeignet.

 

2 Ziele

Es werden formale Methoden zur Spezifikation und Verifikation von zeitkritischen Systemen eingeführt.

 

3 Inhalt

Beispiele zeitkritischer Systeme sind Steuerungen von Eisenbahnen, Robotern oder auch Gasbrennern. Bei allen diesen Systemen kommt es darauf an, dass 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 1994 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.

 

4 Literatur

• E.-R. Olderog, H. Dierks und M. Schenke, Skript Realzeitsysteme, Ausgabe 2002.
• C. Heitmeyer and D. Madrioli, editors. Formal Methods for Real-Time Computing Wiley, 1996.
• M. Joseph, editor. Real-time Systems -- Specification, Verification and Analysis. Prentice Hall, 1996 (siehe http://www.tcs.com/techbytes/htdocs/book_mj.htm )

 

5 Übungsaufgaben

Hier wird die Möglichkeit geboten, die aktuellen Übungsblätter zu dieser Lehrveranstaltung im Postscript- oder DVI-Format abzurufen. Wir bitten 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, bzw. die die Aufgaben während der Bearbeitung am Bildschirm betrachten möchten.

• 12.pdf   (96 KByte)
• 12.ps   (918 KByte)
• 11.pdf   (22 KByte)
• 11.ps   (52 KByte)
• 10.pdf   (113 KByte)
• 10.ps   (290 KByte)
• 09.pdf   (31 KByte)
• 09.ps   (110 KByte)
• 08.pdf   (26 KByte)
• 08.ps   (49 KByte)
• 07.pdf   (62 KByte)
• 07.ps   (64 KByte)
• 06.pdf   (44 KByte)
• 06.ps   (61 KByte)
• 05.pdf   (59 KByte)
• 05.ps   (58 KByte)
• 04.pdf   (51 KByte)
• 04.dvi   (3 KByte)
• 04.ps   (55 KByte)
• 03.ps   (34 KByte)
• 03.dvi   (3 KByte)
• 03.pdf   (41 KByte)
• 02.pdf   (59 KByte)
• 02.dvi   (6 KByte)
• 02.ps   (106 KByte)
• 01.ps   (23 KByte)