Modul "Integration semantischer Modelle"

 

1 Organisatorisches

Form: 1 VL + 3 SE    (6 ECTS-Punkte)

Veranstalter:

W. Damm, E.-R. Olderog, H. Hungar

Vorlesung:

Dienstag 14-16, A3 2-209    Beginn: 20.4.2004

Seminar:

als Blockseminar in den Semesterferien
(beschränkte Teilnehmerzahl)

 

2 Ziele

Verschiedene semantische Modelle für zeitkritische und hybride Systeme werden in einer einführenden Vorlesung vorgestellt und deren Integration in der anschließenden Seminarphase diskutiert.

 

3 Inhalt

Zur Beschreibung von zeitkritischen und hybriden Systemen sind eine Vielzahl semantischer Modelle vorgeschlagen worden, insbesondere Automaten (Timed Automata, hybride Automaten), Logiken (TCTL, Duration Calculus), Prozessalgebren (Timed CSP, Hybrid CSP) und so genannte synchrone Sprachen (State-Charts, LUSTRE, Esterel). Es geht darum, einzelne dieser formalen Modelle kennenzulernen und zu erarbeiten, wie Brücken zwischen diesen Modellen gebaut werden können, um sie in einen Software-Entwicklungsprozess für die Steuerung von zeitkritsichen oder hybriden Systemen integrieren zu können.

Diese Lehrveranstaltung besteht aus den folgenden drei Teilen:

• Vorlesung
  Zu Beginn des Semesters werden in einer Vorlesung folgende semantische Modelle vorgestellt: Automaten (Timed Automata und hybride Automaten), Prozessalgebren (Timed CSP und Hybrid CSP) und synchrone Sprachen (Esterel).
• Seminarvorträge
  Anschließend haben die TeilnehmerInnen Gelegenheit, einen eignen Seminarvortag zum Thema der Integration dieser Modelle auszuarbeiten. Die Literatur dazu liegt vor. In einem Blockseminar in den Semesterferien werden diese Vorträge gehalten.
• schriftliche Ausarbeitung
  Zu jedem Seminarvortrag wird von den TeilnehmerInnen eine schriftliche Ausarbeitung von 10 Seiten Umfang angefertigt, die die Essenz des Vortrags widerspiegelt. Eine Rohfassung der Ausarbeitung soll zum Zeitpunkt des Vortrags vorliegen. Die endg"ultige Fassung der Ausarbeitung wird nach dem Vortrag unter Ber"ucksichtigung der Diskussion des Vortrags angefertigt.

3.1 Bewertung

Die Bewertung dieses Moduls setzt sich aus drei gleichwertigen Teilen zusammen: einer mündlichen Prüfung über die Vorlesung, den eigenen Vortrag sowie die schriftliche Ausarbeitung dazu.

3.2 Vorbesprechung

Die Lehrveranstaltung beginnt am
Dienstag, den 20.4.04, um 14.15 Uhr im Raum A3 2-209
mit einer Vorbesprechung.

 

4 Literatur

[1]

R. Alur. Timed automata. In Verification of Digital and Hybrid Systems, NATO ASI Series. Springer Verlag, 1998.

[2]

R. Alur, C. Courcoubetis, T.A. Henzinger, and Pei-Hsin Ho. Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. In R.L. Grossmann, A. Nerode, A.P. Ravn, and H. Rischel, editors, Hybrid Systems, volume 736 of Lecture Notes in Computer Science, pages 209-229. Springer Verlag, 1993.

[3]

R. Alur and D.L. Dill. A theory of timed automata. Theoretical Computer Science, 126(2):183-235, 1994.

[4]

R. Alur and T.A. Henzinger. Modularity for timed and hybrid systems. In CONCUR 97: Concurrency Theory, volume 1243 of Lecture Notes in Computer Science, pages 74-88. Springer Verlag, 1997.

[5]

A. Benveniste and G. Berry. The synchronous approach to reactive and real-time systems. Proc. of the IEEE, 79(9):1270-1282, 1991.

[6]

J. Davies. Specification and Proof in Real-Time CSP. Cambridge University Press, 1993.

[7]

J. Davies and S. Schneider. A brief history of Timed CSP. Theoretical Computer Science, 138:243-271, 1995.

[8]

T.A. Henzinger. Masaccio: A formal model for embedded components. In Proceedings of the First IFIP International Conference on Theoretical Computer Science, Lecture Notes in Computer Science. Springer-Verlag, 2000.

[9]

Xiaojun Liu, Jie Liu, J. Eker, and E.A. Lee. Heterogeneous modeling and design of control systems. In Tariq Samad and Gary Balas, editors, Software-Enabled Control: Information Technology for Dynamical Systems. Wiley-IEEE Press, 2003.

[10]

N.A. Lynch, R. Segala, and F. Vaandrager. Hybrid I/O automata. Information and Computation, 185(1):105-157, 2003.

[11]

M.Rönnkö, A.P. Ravn, and K. Sere. Hybrid action systems. Theoretical Computer Science, 290:937-973, 2003.

[12]

Chaochen Zhou, Wang Ji, and A.P. Ravn. A formal description of hybrid systems. In R. Alur, T. Henzinger, and E. Sontag, editors, Hybrid Systems III, volume 1066 of Lecture Notes in Computer Science, pages 511-530. Springer Verlag, 1996.