Die Informatik des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Verwaltung des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Informatik des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Mathematik des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage des Fachbereiches 3 der Universität Bremen Hier geht es zur Homepage der Universität Bremen
Zeige Wirtschaftsinformatik-Format Pdf_icon Informatik-Format Pdf_icon Digitale Medien-Format Pdf_icon Systems Engineering-Format Pdf_icon

Informatik-Ansicht

Theorie reaktiver Systeme


Theory of Reactive Systems
Modulnummer
MB-699.03
Master
Pflicht/Wahl
Wahl Basis Ergänzung
Sonderfall
Zugeordnet zu Masterprofil
Basis Ergänzung
Sicherheit und Qualität
KI, Kognition, Robotik
Digitale Medien und Interaktion
Modulbereich : Mathematik und Theoretische Informatik
Modulteilbereich : 699 Spezielle Gebiete der Theoretischen Informatik
Anzahl der SWS
V UE K S Prak. Proj.
2 2 0 0 0 0 4
Kreditpunkte : 6 Turnus

i. d. R. angeboten alle 2 Semester

Formale Voraussetzungen : -
Inhaltliche Voraussetzungen : Theoretische Informatik 1
Vorgesehenes Semester : ab 1. Semester
Sprache : Deutsch/Englisch
Ziele :
  • 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

Inhalte :
  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

Unterlagen (Skripte, Literatur, Programme usw.) :
  • 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

Form der Prüfung : i.d.R. Bearbeitung von Übungsaufgaben und Fachgespräch oder mündliche Prüfung
Arbeitsaufwand
Präsenz 56
Übungsbetrieb/Prüfungsvorbereitung 124
Summe 180 h
Lehrende: Prof. Dr. J. Peleska Verantwortlich Prof. Dr. J. Peleska
Zurück

Zeige Wirtschaftsinformatik-Format Pdf_icon Informatik-Format Pdf_icon Digitale Medien-Format Pdf_icon Systems Engineering-Format Pdf_icon