Theorie reaktiver Systeme

i. d. R. angeboten alle 2 Semester

• 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

• 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