Universität Bremen  
  Universität Bremen FB3 TZI BISS  
  AG BS > Lehre > WS 2007/2008 > Deutsch
English
 

Theorie Reaktiver Systeme, Wintersemester 2007/08

 


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


Aktuelles

  • Termine zur Prüfung können per e-mail vereinbart werden. Bitte gebt dabei die gewünschte Prüfungsform, die relevante Prüfungsordnung sowie den Bedarf eines Beisitzers an.
  • Die Evaluationsbögen bitte in das Postfach Nummer 33 in der 6. Ebene MZH einwerfen.


Inhalt dieser Seite


Termine

Vorlesung: 
Mi. 13 - 15 Uhr, MZH 4194, Dr. Ulrich Hannemann ab 24.10.2007
Übung: 
Mo. 17:00 Uhr - 18:30 Uhr, MZH 8090, Dr. Ulrich Hannemann ab 5.11.2007

Ü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

In den Übungen wurden zusätzlich noch Ergänzungen zu den Themen
  • Strukturelle Induktion
  • Fixpunkte
  • Trace Expressions
vermittelt.

Übungszettel



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

  • 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