Theorie Reaktiver Systeme, Sommersemester 2010

Diese Seite gibt weitere Informationen zur Vorlesung. Wir bemühen uns diese Informationen so aktuell wie möglich zu halten.

Aktuelles

In 17. KW finden die Vorlesung am Mo. 26.04.2010 in MZH 1450 (regulärer Übungstermin) und die Übung am Do. 29.04.2010 in MZH 1470 (regulärer Vorlesungstermin) statt.

Termine

	Vorlesung:	Do. 8 - 10 Uhr,	MZH 1470,	Prof. Dr. Jan Peleska
	Übung:	Mo. 8 - 10 Uhr,	MZH 1450,	Elena Vorobev

In dieser Veranstaltung werden die theoretischen Grundlagen für Spezifikationsformalismen erarbeitet, welche sich besonders für nebenläufige reaktive Echtzeitsysteme (Concurrent Embedded Real-Time 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".

Skript zur Vorlesung

(Letzte Aktualisierung: 2010-06-21)

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

Übungszettel

Übungsblatt 1: Bearbeiten Sie Exercise 1 aus dem Vorlesungsmanuskript
Abgabe: bis 2010-04-19, 09:30 Uhr
Übungsblatt 2: Bearbeiten Sie Exercise 2 aus dem Vorlesungsmanuskript
Abgabe: bis 2010-04-26, 09:30 Uhr
Übungsblatt 3: Bearbeiten Sie Exercises 4 und 5 aus dem Vorlesungsmanuskript
Abgabe: bis 2010-05-10, 09:30 Uhr
Übungsblatt 4: Bearbeiten Sie Exercise 6 aus dem Vorlesungsmanuskript
Abgabe: bis 2010-05-25, 09:30 Uhr
Übungsblatt 5: Bearbeiten Sie Exercise 8.a aus dem Vorlesungsmanuskript
Abgabe: bis 2010-06-14, 09:30 Uhr
Übungsblatt 6: Bearbeiten Sie Exercise 11 aus dem Vorlesungsmanuskript
Abgabe: bis 2010-06-28, 09:30 Uhr
Übungsblatt 7: Bearbeiten Sie Exercise 10 aus dem Vorlesungsmanuskript
Abgabe: bis 2010-07-05, 09:30 Uhr

Leistungsnachweise

Es können Fachgespräche oder Modulprüfungen abgelegt werden.

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

Autor: jp

AG Betriebssysteme, Verteilte Systeme

Zuletzt geändert am: 2. November 2022