FB3
TZI
BISS
Theorie Reaktiver Systeme, Wintersemester 2006/07
Diese Seite gibt weitere Informationen zur Vorlesung. Wir bemühen uns diese Informationen so aktuell wie möglich zu halten.
Aktuelles
Inhalt dieser Seite
Termine
| Vorlesung: |
Mo. 15 - 17 Uhr | GW2 B1400 | Dr. Ulrich Hannemann | ab 30.10.2006 |
| Übung: |
Do. 8-10 Uhr | SFG 2030 | Dr. Ulrich Hannemann | ab 2.11.2006 |
Ü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
- Modelle der operationellen Semantik:
Zustands-Transitionssysteme -
markierte Transitionssysteme ("Labelled Transition Systems LTS") -
Beispiel: Semantik einer while-Sprache
Literatur: [Apt, Olderog 91] - Operationelle Semantik von CSP
Literatur: pdf aus [Schneider2000] - Äquivalenz und Bisimilarität
Literatur: [Milner89], Kapitel 4.2. - Algebraischer Gesetze in Prozessalgebren (CSP): Herleitung aus dem semantischen Modell -- Algorithmus auf endlichen LTS
- Sequenzen, Traces, Trace-Äquivalenz
Literatur: verstreut in [Hoare85],[Roscoe98] und [Schneider00] - Test Äquivalenz, may Tests,
must Tests
- Hierarchie Bisimilarität, Test Äquivalenz, Trace
Äquivalenz - Testäquivalenz von "late branching" und "early
branching" - Head normal form
- Refinement - Safety - Requirement
Coverage - Robustness - Hennessy Test Cases
- Requirement
Coverage Tests - Robustness Tests
-
Refusals, Failure-Semantik und Zusammenhang mit Tests
-
Divergenzen, Modellierung von Uhren, Timed CSP
-
Berechnungen in Timed CSP, Timed Traces, Timed Automata
Übungszettel
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 50 % der Punkte erreicht werden -,
- oder durch eine bestandene mündliche Prüfung (alias mündliche Modulprüfung) über Vorlesung, Übungen und Aufgabenblätter.
Literatur
- Syntax und operationelle Semantik von Timed CSP: pdf
- 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.
Autor: jp
| Zuletzt geändert am: 2. November 2022 |  |