Theorie Reaktiver Systeme, Sommersemester 2012

Aktuelles

Inhalt dieser Seite

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

Termine

Überblick

Veranstaltungsinhalte

Session 1: Beschreibungsformalismen - Begriffe und Grundlagen

• Eigenschaften von Beschreibungsformalismen (englische Attributbezeichnungen):
  • wide spectrum: Der Formalismus eignet sich für nahezu alle Anwedungsgebiete
  • domain-specific: Der Formalismus ist auf die Spezifikation von Eigenschaften einer spezifischen Anwendungsdomäne spezialisiert
  • explicit: Der Formalismus beschreibt Eigenschaften mit Hilfe eines Modells
  • implicit: Der Formalismus beschreibt Eigenschaften mit Hilfe logischer Zusicherungen
• Ausprägungen der Syntaxbeschreibung für Beschreibungsformalismen:
  • abstract syntax spezifiziert die Syntax, ohne die konkrete Ausprägung der atomaren Sprachelemente (Tokens oder Lexeme) anzugeben.
  • concrete syntax spezifiziert auch die konkrete Ausprägung (Codierung) der atomaren Sprachelemente
• Aspekte der semantischen Modellierung eines Formalismus:
  • static semantics: Logische Eigenschaften der Sprache, die sich durch statische Analyse bestimmen lassen, aber nicht mehr auf Basis der Grammatik (also nicht mehr rein syntaktisch) ausdrückbar sind; z.B. der Scope einer Variablen oder Typregeln
  • dynamic (behavioural) semantics: Erklärung des mit einer im Formalismus abgefassten Beschreibung verbundenen Verhaltens in Bezug auf die Änderungen von Zuständen und Ausgaben in Abhängigkeit von Ausführungsschritten oder von konkreter Zeit.
  • observational semantics erklärt das mit einer Beschreibung assoziierte Verhalten allein mit Hilfe von beobachtbaren Größen, z.B. Ein- und Ausgaben.
  • operationelle Semantik beschreibt Verhalten mit Hilfe eines Transitionssystems, welches die Änderungen des gesamten Zustands charakterisiert.
  • denotationelle Semantik assoziiert mit jeder syntaktisch zulässigen Beschreibung durch Abbildung auf mathematische Objekte (Denotations)
  • abstract semantics beschreibt das Verhalten auf einem abstrahierten Modell der Spezifikation; die Abstraktion bezieht sich auf Datentypen und auch auf Kontrollstrukturen der Beschreibung.

Weitere Sessions: siehe Skript zur Vorlesung (letzte Aktualisierung: 2012-07-18)

Übungszettel

• Übungsblatt 1: Bearbeiten Sie Exercise 1 aus dem Vorlesungsmanuskript
  Abgabe: am 2012-04-30 (1 Woche)
• Übungsblatt 2: Bearbeiten Sie Exercises 2 und 3 aus dem Vorlesungsmanuskript; für die Darstellung des Computation Tree in Exercise 3 soll das Tool dot verwendet werden
  Abgabe: am 2012-05-09 (1 Woche)
• Übungsblatt 3: Bearbeiten Sie Exercises 4 und 6 aus dem Vorlesungsmanuskript
  Abgabe: bis 2012-05-28 (2 Wochen)
• Übungsblatt 4: Bearbeiten Sie Exercise 7 aus dem Vorlesungsmanuskript
  Abgabe: bis 2012-06-11 (1 Woche)
• Übungsblatt 5: Bearbeiten Sie Exercise 8.a aus dem Vorlesungsmanuskript
  Abgabe: bis 2012-06-18 (1 Woche)
• Übungsblatt 6: Bearbeiten Sie Exercises 9, 10 und 11.a aus dem Vorlesungsmanuskript
  Abgabe: bis 2012-07-09 (2 Wochen)
• Übungsblatt 7: Bearbeiten Sie Exercises 12.a und 12.b aus dem Vorlesungsmanuskript
  Abgabe: bis 2012-07-23 (2 Wochen)

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 60% der Punkte erreicht werden.

Literatur

• 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
  
• 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