inf456 - Realzeitsysteme (Vollständige Modulbeschreibung)
Modulbezeichnung | Realzeitsysteme |
Modulkürzel | inf456 |
Kreditpunkte | 6.0 KP |
Workload | 180 h |
Einrichtungsverzeichnis | Department für Informatik |
Verwendbarkeit des Moduls | |
Zuständige Personen |
|
Teilnahmevoraussetzungen | |
Kompetenzziele | Einführung von formalen Methoden zur Spezifikation und Verifikation von zeitkritischen Systemen und deren Kombination. Es werden folgende Kenntnisse, Fertigkeiten und Kompetenzen vermittelt: Kenntnisse:
|
Modulinhalte | 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. |
Literaturempfehlungen | essentiell
|
Links | |
Unterrichtsprachen | |
Dauer in Semestern | 1 Semester |
Angebotsrhythmus Modul | unregelmäßig |
Aufnahmekapazität Modul | unbegrenzt |
Modulart | Ergänzung/Professionalisierung |
Modullevel | AS (Akzentsetzung) |
Lehr-/Lernform | VL + Ü |
Lehrveranstaltungsform | Kommentar | SWS | Angebotsrhythmus | Workload Präsenz |
---|---|---|---|---|
Vorlesung | 3 | 42 | ||
Übung | 1 | 14 | ||
Präsenzzeit Modul insgesamt | 56 h |
Prüfung | Prüfungszeiten | Prüfungsform |
---|---|---|
Gesamtmodul | Am Ende des Semesters und nach Absprache mit dem Lehrenden |
Semesterbegleitende fachpraktische Übungen und mündliche Prüfung |