inf456 - Realzeitsysteme (Vollständige Modulbeschreibung)

inf456 - Realzeitsysteme (Vollständige Modulbeschreibung)

Originalfassung Englisch PDF Download
Modulbezeichnung Realzeitsysteme
Modulkürzel inf456
Kreditpunkte 6.0 KP
Workload 180 h
Einrichtungsverzeichnis Department für Informatik
Verwendbarkeit des Moduls
  • Master Engineering of Socio-Technical Systems (Master) > Embedded Brain Computer Interaction
  • Master Engineering of Socio-Technical Systems (Master) > Systems Engineering
  • Master Informatik (Master) > Theoretische Informatik
Zuständige Personen
  • Olderog, Ernst-Rüdiger (Modulverantwortung)
  • Lehrenden, Die im Modul (Prüfungsberechtigt)
Teilnahmevoraussetzungen

Theoretische Informatik I + II

Kompetenzziele

Einführung von formalen Methoden zur Spezifikation und Verifikation von zeitkritischen Systemen und deren Kombination.
Fachkompetenzen
Die Studierenden:

  • lernen Zeitmodelle und Realzeiteigenschaften kennen
  • spezifizieren und verifizieren Realzeitsysteme
  • modellieren Realzeitsysteme mit Realzeitautomaten und PLC-Automaten
  • wenden den Model-Checker UPPAAL zur Verifikation von Realzeiteigenschaften an
  • spezifizieren Realzeitsysteme im Duration Calculus
  • lernen Entscheidbarkeits- und Unentscheidbarkeitsresultate für Realzeitsysteme kennen

Methodenkompetenzen
Die Studierenden:

  • erkennen Logik und Automaten als adäquate Beschreibungsformen für Realzeitsysteme     

Sozialkompetenzen
Die Studierenden:

  • arbeiten in kleinen Gruppen an Lösungen von Aufgaben
  • präsentieren Lösungen von Aufgaben vor Gruppen

Selbstkompetenzen
Die Studierenden:

  • erlernen Ausdauer bei der Bearbeitung schwieriger Aufgaben
  • erlernen Präzision bei der Spezifikation von Problemen
Modulinhalte

Beispiele zeitkritischer Systeme sind Steuerungen von Eisenbahnen, Robotern oder auch Gasbrennern. Bei 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 attraktive Methode ist der seit 1991 von Zhou Chaochen entwickelte "Duration Calculus''. Es handelt sich dabei um eine Logik mitsamt Kalkül, in der die Dauer (engl. duration) von Zuständen beschrieben werden kann. In der Vorlesung wird der Duration Calculus vorgestellt und dessen Anwendung an Hand von Beispielen erläutert. Als weitere Spezifikationsmethode werden die 1994 von Alur & Dill eingeführten Realzeitautomaten (engl. Timed Automata) vorgestellt. Nach der Spezifikation von Anforderungen an ein Realzeitsystem schließt sich die Verifikation von entwickelten Programmen an. Dabei werden die Spezifikationsmethoden Duration Calculus und Timed Automata dazu benutzt, um das Realzeitverhalten der Programme zu beschreiben. Anschließend kann auf der Basis dieser Verhaltensbeschreibungen die Korrektheit beweisen werden.
Themen: 

  • diskretes und kontinuierliches Zeitmodell
  • Logiken und Automatenmodelle zur Spezifikation von Realzeitsystemen (Prädikatenlogik, Duration Calculus, Timed CTL, Realzeitautomaten, PLC-Automaten)
  • Entscheidbarkeits- und Unentscheidbarkeitsresultate für Realzeitsysteme
  • Model-Checker UPPAAL für Realzeitautomaten,
  • formale Spezifikation von Realzeitsystemen im Duration Calculus sowie mit Realzeitautomaten und PLC-Automaten
  • Verifikation konkreter Realzeitautomaten mit dem Model-Checker UPPAAL
  • Transformation von Duration Calculus für diskrete Zeit in reguläre Sprachen
  • Implementierbarkeit von Realzeitsystemen auf PLC-ähnlicher Hardware
Literaturempfehlungen

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 ).
Links
Unterrichtsprachen Deutsch, Englisch
Dauer in Semestern 1 Semester
Angebotsrhythmus Modul unregelmäßig
Aufnahmekapazität Modul unbegrenzt
Lehr-/Lernform V + Ü
Vorkenntnisse Theoretische Informatik I + II
Lehrveranstaltungsform Kommentar SWS Angebotsrhythmus Workload Präsenz
Vorlesung 3 SoSe oder WiSe 42
Übung 1 SoSe oder WiSe 14
Präsenzzeit Modul insgesamt 56 h
Prüfung Prüfungszeiten Prüfungsform
Gesamtmodul

Am Ende der Vorlesungszeit

Fachpraktische Übungen und mündliche Prüfung.