Stud.IP Uni Oldenburg
University of Oldenburg
29.06.2022 02:09:38
inf456 - Real-Time Systems (Complete module description)
Original version English Download as PDF
Module label Real-Time Systems
Module code inf456
Credit points 6.0 KP
Workload 180 h
Institute directory Department of Computing Science
Applicability of the module
Responsible persons
Hein, Andreas (Module responsibility)
Olderog, Ernst-Rüdiger (Authorized examiners)
Prerequisites
Skills to be acquired in this module
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
Module contents
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.
Reader's advisory
essentiell
    • E.-R. Olderog, H. Dierks: Real-Time Systems: Formal Specification and Automatic Verification, Cambridge University Press, 2008
empfohlen:
Links
Languages of instruction
Duration (semesters) 1 Semester
Module frequency unregelmäßig
Module capacity unlimited
Modullevel / module level AS (Akzentsetzung)
Modulart / typ of module Ergänzung/Professionalisierung
Lehr-/Lernform / Teaching/Learning method VL + Ü
Vorkenntnisse / Previous knowledge
Course type Comment SWS Frequency Workload of compulsory attendance
Lecture
3 42
Exercises
1 14
Total time of attendance for the module 56 h
Examination Time of examination Type of examination
Final exam of module
Am Ende des Semesters und nach Absprache mit dem Lehrenden
KL