Universität Bremen  
  Universität Bremen FB3 TZI BISS  
  AG BS > Lehre > SoSe 2005 > Deutsch
English
 

Theorie Reaktiver Systeme, Sommersemester 2005
 
Diese Seite gibt weitere Informationen zur Vorlesung. Wir bemühen uns diese Informationen so aktuell wie möglich zu halten.

Inhalt dieser Seite

Termine

Vorlesung: 
 Di. 10-12 Uhr MZH 7230 Prof. Dr. Jan Peleska ab 12.4.2005
Übung: 
 Mi. 8-10 Uhr MZH 6240 Ulrich Hannemann ab 13.4.2005

Überblick

In dieser Veranstaltung werden die theoretischen Grundlagen für Spezifikationsformalismen erarbeitet, welche sich besonders für nebenläufige reaktive Systeme ("Embedded Systems") eignen. Im Schwerpunkt befassen wir uns mit den Möglichkeiten der semantischen Modellierung, und der Zuordnung semantischer Modelle zu gegebenen Spezifikationsformalismen. Das Verständnis für diese Grundlagen ist auf vielen Gebieten nicht nur nützlich, sondern unbedingt erforderlich: In der Forschung wird das hier vermittelte Wissen beim Entwurf neuer Spezifikationsformalismen und Entwicklung zugehöriger Beweistheorien benötigt. Für die Praxis eröffnet die Kenntnis semantischer Modelle neue Möglichkeiten zur automatischen Verifikation und Validierung von Anforderungen mittels Modellprüfung, für die automatischen Softwaregenerierung aus Spezifikationen, sowie für das automatisierte Testen. Die Vorlesung eignet sich besonders als Grundlage für die Veranstaltung "Spezifikation eingebetteter Systeme".

Veranstaltungsinhalte

  • 1. Modelle der operationellen Semantik: Zustands-Transitionssysteme - markierte Transitionssysteme ("Labelled Transition Systems LTS") - Transitionssysteme mit Codierung der Refusal-Information
  • 2. Induktive Definitionen -- Nachweis universeller Eigenschaften durch strukturelle Induktion über Syntax und operationelle Semantik.
  • 3. Äquivalenz und Bisimilarität -- Beweistheorien: Konsistenz - Vollständigkeit -- Herleitung aus dem semantischen Modell, dargestellt am Beispiel algebraischer Gesetze in Prozessalgebren (CSP) -- Algorithmus auf endlichen LTS
  • 4. Testing Equivalence -- may Tests und must Tests -- Konstruktion minimaler Testmengen
  • 5. Modelle der denotationellen Semantik: Trace Modell, Failures-Modell -- Failures Refinement - Trace Refinement

Übungszettel

Übungszettel Ausgabe Abgabe
Zettel 1 13.04.2005 26.04.2005 Hinweis: Bei Aufgabe 1 ist die zusätzliche Voraussetzung "P terminiert" notwendig!
Zettel 2 26.04.2005 10.05.2005
Zettel 3 10.05.2005 25.05.2005 Hier ist die ausführliche Behandlung des Beispiels aus der Übung vom 11. Mai
Zettel 4 24.05.2005 7.06.2005 Version 1.2: Zwei minimale Präzisierungen
Zettel 5 7.06.2005 21.06.2005
Zettel 6 21.06.2005 05.07.2005

Leistungsnachweise

Einen benoteten Leistungsnachweis erhaltet Ihr bei erfolgreich erbrachter Prüfungsleistung:
  • Entweder durch erfolgreiches Bearbeiten von Übungsaufgaben inkl. bestandenem Fachgespräch - dabei müssen alle Serien bearbeitet sowie dabei 60 % der Punkte erreicht werden -,
  • oder durch eine bestandene mündliche Prüfung (alias mündliche Modulprüfung).
Der erste Prüfungstermin ist Montag, der 11. Juli .
Weitere Prüfungen können am 29. Juli stattfinden, sowie sp&aml;ter nach Vereinbarung. Bitte meldet Euch mit Terminwunsch bei Ulrich per e-mail an.

Literatur

  • Syntax und operationelle Semantik von Timed CSP: pdf
  • A.W. Roscoe:
    "The Theory and Practice of Concurrency",
    Prentice Hall, 1998
    Zur Vertiefung der CSP Theorie.
  • Robin Milner:
    "Communication and Concurrency",
    Prentice-Hall, 1989
  • 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.
 
   
Autor: jp 		 
  AG Betriebssysteme, Verteilte Systeme 
Zuletzt geändert am: 2. November 2022   Impressum