Theorie Reaktiver Systeme, Wintersemester 2007/08

Aktuelles

• Termine zur Prüfung können per e-mail vereinbart werden. Bitte gebt dabei die gewünschte Prüfungsform, die relevante Prüfungsordnung sowie den Bedarf eines Beisitzers an.
• Die Evaluationsbögen bitte in das Postfach Nummer 33 in der 6. Ebene MZH einwerfen.

Inhalt dieser Seite

• Termine
• Überblick
• Veranstaltungsinhalte
• Übungszettel
• Leistungsnachweise
• Literatur

Termine

Überblick

Veranstaltungsinhalte

• Modelle der operationellen Semantik: Zustands-Transitionssysteme - markierte Transitionssysteme ("Labelled Transition Systems (LTS)") - Beispiel: Semantik einer while-Sprache
  Vorlesung
  Literatur: [Apt, Olderog 91]
• Operationelle Semantik von CSP
  Literatur: [Schneider2000]
• Äquivalenz und Bisimilarität
  Literatur: [Milner89], Kapitel 4.2.
• Bisimilarität
  Die Beispielanwendung des Algorithmus ist separat notiert.
• Traces und Traceäquivalenz
  Literatur: [Schneider2000]
• Tests und Testäquivalenz
  
• Bisimilarität und Testäquivalenz
  
• Fortsetzung Bisimilarität und Testäquivalenz, Head Normal Form
  
• Refinement, Safety Tests
  
• Requirement Coverage, Robustness
  
• Acceptance Trees, Failures Semantik
  
• Ergänzungen zur Failures Semantik, Axiomatische Sicht und eine kurze Erwähnung der Failures/Divergences Semantik
  
• Timed CSP
  
• Semantik von Timed CSP
  

• Strukturelle Induktion
• Fixpunkte
• Trace Expressions

Übungszettel

• Übungsblatt 1, Abgabe am 14.11.2007
• Übungsblatt 2, Abgabe am 28.11.2007
• Übungsblatt 3, Abgabe am 12.12.2007 nach Absprache
• Übungsblatt 4, Abgabe am 9.1.2008 nach Absprache
• Übungsblatt 5, Abgabe am 6. 2. 2008

Leistungsnachweise

Für ein Fachgespräch ist die erfolgreiche Bearbeitung der Übungsblätter notwendig. Diese dürfen in Dreiergruppen bearbeitet werden, dabei müssen mindestens 50% der Punkte erreicht werden.

Literatur

• C.A.R. Hoare:
  "Communicating Sequential Processes",
  Prentice Hall, 1985
  
• A.W. Roscoe:
  "The Theory and Practice of Concurrency",
  Prentice Hall, 1998
  Zur Vertiefung der CSP Theorie.
• S. Schneider:
  "Concurrent and Real-Time Systems- The CSP Approach
  J.Wiley, 2000
  Zur Vertiefung der CSP Theorie.
• Robin Milner:
  "Communication and Concurrency",
  Prentice-Hall, 1989
  
• K. Apt, E.-R. Olderog:
  "Verification of Sequential and Concurrent Programs",
  Springer, 1991
  
• J. Peleska:
  "Formal Methods and the Development of Dependable Systems",
  Christian-Albrechts-Universität zu Kiel 1996.
  Eine Postscript-Version liegt zum Download lokal auf den Seiten der Universität Bremen.
• Yoshinao Isobe, Markus Roggenbach:
  "A complete axiomatic semantics for the CSP stable-failures model", CONCUR 2006, Lecture Notes in Computer Science 4137, pp. 158 - 172, 2006