Die Vorlesung beschäftigt sich mit formalen Methoden zur Modellierung und Analyse von Echtzeitsystemen. Es werden automatentheoretische Ansätze (Zeitautomaten) zur Modellierung und entsprechend erweiterte Temporallogiken (z.B. Echtzeit LTL) zur Formulierung von Eigenschaften von Echtzeitsystemen untersucht. Insbesondere das Model-Checking Problem ist Gegenstand der Vorlesung. Praktische Beispiele werden mit dem UPPAAL System in den Übungen behandelt.
dn