• Semantische Alternativen für eingebettete Echtzeitsysteme bewerten können

• Verständnis für die Grundkonzepte des Model Checkings entwickeln

• Große (unendliche) Zustandsräume durch Abstraktion beherrschbar machen können

• Semantische Modellierung zur Automatisierung bei Verifikation und Test einsetzen können

1. Modelle der operationellen Semantik: Zustands-Transitionssysteme, markierte Transitionssysteme („Labelled Transition Systems LTS“), Markierte Transitionssysteme mit Zeit („Timed LTS“), Transitionssysteme mit Codierung der Refusal-Information – Finite State Machines (FSM) – Interleaving-Semantics versus „true Parallelism“ : Harel’s StepSemantik für Statecharts – Kripke-Strukturen

2. Äquivalenz und Verfeinerung: Bisimilarität – Simulationsbeziehung - Verfeinerungen

3. Fundamentale Modelleigenschaften: Deadlockfreiheit – Livelockfreiheit - Safety- und Liveness-Eigenschaften – Fairness

4. Modell-orientierte Spezifikationsformalismen und ihre Semantik: Timed Automata – Hybrid Automata – Timed CSP

5. Implizite Spezifikationsformalismen und ihre Semantik: Trace Logik mit und ohne Zeit – Temporallogiken: Linear Time Logic (LTL), Computation Tree Logic (CTL), Timed Computation Tree Logic (TTCL)

6. Nachweis universeller Eigenschaften durch strukturelle Induktion über Syntax und operationelle Semantik.

7. Modellprüfung

8. Modellabstraktion

i.d.R. Bearbeitung von Übungsaufgaben und Fachgespräch oder mündliche Prüfung

• Edmund M. Clarke, Orna Grumberg and Doron A. Peled: “Model Checking”, The MIT Press, 1999

• Christel Baier and Joost-Pieter Katoen: “Principles of Model Checking”, The MIT Press, 2008

• K. Apt, E.-R. Olderog: “Verification of Sequential and Concurrent Programs”, Springer, 1991