inf456 - Realzeitsysteme (Vollständige Modulbeschreibung)

Einführung von formalen Methoden zur Spezifikation und Verifikation von zeitkritischen Systemen und deren Kombination. Es werden folgende Kenntnisse, Fertigkeiten und Kompetenzen vermittelt:

Kenntnisse:

• diskretes und kontinuierliches Zeitmodell, Logiken und Automatenmodelle zur Spezifikation von Realzeitsystemen (Duration Calculus, TCTL, Realzeitautomaten, PLC-Automaten), Entscheidbarkeits- und Unentscheidbarkeitsresultate für Realzeitsysteme, Model-Checker UPPAAL für Realzeitautomaten, Implementierung von Realzeitsystemen auf PLC-ähnlicher Hardware

Fertigkeiten:

• formale Spezifikation von Realzeitsystemen im Duration Calculus sowie mit Realzeitautomaten und PLC-Automaten, Verifikation konkreter Realzeitautomaten mit dem Model-Checker UPPAAL, Verifikation von Spezifikationen im Duration Calculus für diskrete Zeit mit dem Model-Checker DCVALID

Kompetenzen:

• Fähigkeit zur Spezifikation und Verifikation von Realzeitsystemen

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 eines 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 verschiedene 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. Dazu wird das in Oldenburg entwickelte Tool Moby/RT eingesetzt.

essentiell

• • E.-R. Olderog, H. Dierks: Real-Time Systems: Formal Specification and Automatic Verification, Cambridge University Press, 2008

empfohlen:

• • 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://docencia.etsit.urjc.es/moodle/file.php/31/documentos/RTSbook.pdf ).

Am Ende des Semesters und nach Absprache mit dem Lehrenden

Semesterbegleitende fachpraktische Übungen und mündliche Prüfung