inf456 - Realzeitsysteme (Vollständige Modulbeschreibung)

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

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

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 der Vorlesungszeit

Fachpraktische Übungen oder Klausur oder mündliche Prüfung