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

Theorie Reaktiver Systeme, Sommersemester 2009
 

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: Do. 8 - 10 Uhr (Beginn um 8:30), MZH 7260, Prof. Dr. Jan Peleska
 
 Übung: Mo. 8 - 10 Uhr (Beginn um 8:30), MZH 1400, Prof. Dr. Jan Peleska

Überblick

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

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, Abgabe 2009-04-30 (in der Vorlesung): Bearbeiten Sie Exercise 1 und Exercise 2 aus dem Vorlesungsmanuskript
  • Übungsblatt 2, Abgabe 2009-05-07 (in der Vorlesung): Bearbeiten Sie Exercise 3 und Exercise 4 aus dem Vorlesungsmanuskript (Seite 10).
  • Übungsblatt 3, Abgabe 2009-05-18 (in der Vorlesung): Bearbeiten Sie Exercise 5 aus dem Vorlesungsmanuskript (Seite 12).
  • Übungsblatt 4, Abgabe 2009-06-04 (in der Vorlesung): Bearbeiten Sie Exercise 6 aus dem Vorlesungsmanuskript (Seite 18).
  • Übungsblatt 4, Abgabe 2009-06-18 (in der Vorlesung): Bearbeiten Sie Exercise 7 aus dem Vorlesungsmanuskript (Seite 25).
  • Übungsblatt 5, Abgabe 2009-06-25 (in der Vorlesung): Bearbeiten Sie Exercise 8 aus dem Vorlesungsmanuskript (Seite 28).
  • Übungsblatt 4, Abgabe 2009-07-06 (in der Vorlesung): Bearbeiten Sie Exercise 9 aus dem Vorlesungsmanuskript (Seite 31).

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 50% 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   Impressum