Viele der (eingebetteten) Software-Systeme mit denen wir im Alltag konfrontiert sind, haben zeitkritische Funktionalitäten. Beispielsweise sollte ein Airbag bei einem Unfall innerhalb einer bestimmten, sehr kurzen, Zeitspanne aktiviert werden. Ebenso erwarten wir von den diversen Apps auf unseren Smartphones schnelle Antwortzeiten, um sie komfortabel und zielbringend zu nutzen.

Bei der Modellierung von Software-Systemen ist somit „Zeit“ ein entscheidender Faktor. In dieser Vorlesung werden verschiedenen Mechanismen beschrieben sogenannte Realzeitsysteme zu formalisieren. Neben der Modellierung steht auch die Analyse der Systeme im Fokus der Vorlesung. Es werden insbesondere folgende Themen behandelt:

• Timed Automata (eine Erweiterung endlicher Automaten um Zeit)
• Model-Checking von Timed Automata mit Hilfe von UPPAAL
• Timed Games (Zwei Spieler versuchen eigene Ziele in einem zeitkritischen Spiel zu erreichen)
• Interval Temporal Logic (eine Logik die über Zeitintervalle spricht)
• Erweiterungen und Anwendungen von Timed Systems

Die wöchentliche Vorlesung besteht sowohl aus theoretischen als auch angewandten Anteilen. Die angewandten Anteile bestehen aus freiwilligen Übungsaufgaben, die in der Vorlesung besprochen werden.