Hierarchische Modelle und Verifikationsverfahren für verteilte Systeme

Seminar zur Theoretischen Informatik

Sommersemester 2001

Zur Strukturierung von Programmen haben sich hierarchische Ansätze bestens bewährt. Ein Beispiel sind Prozeduren, die wiederum Prozeduren enthalten, ein anderes hierarchische Beschreibungen von Klassendiagrammen im Bereich der objektorientierten Programmierung. Auch im Bereich der Spezifikationssprachen und Modelle für verteilte Systeme eignen sich hierarchische Ansätze, um Systeme übersichtlich und kompakt zu beschreiben. In diesem Seminar sollen verschiedene Ansätze wie Hierarchische Petri-Netze, Statecharts und Hierarchische Message Sequence Charts etc. vorgestellt und diskutiert sowie darauf aufbauende Verifikationsverfahren erörtert werden.

Die folgende Tabelle gibt eine Übersicht der Einzelthemen. Die Vorträge finden jeweils montags um 14:00 Uhr im Seminarraum des Lehrstuhls für Informatik II statt.

Hier finden Sie allgemeine Hinweise zur Ausarbeitung und zum Vortrag.

Nr.	Datum	Thema	Literatur	Referent(in)	Betreuer
1	23.04.	Hierarchische Automaten als Modell für Statecharts	[MLS97]	Anahita Afshin Nia	Benedikt Bollig
2	14.05.	Modulare Verifikation von Petri-Netzen	[DDG+89]	Andreas Strack	Thomas Noll
3	28.05.	Reaktive Module	[AH96]	Alexander Nyßen	Thomas Noll
4	11.06.	Modulares Model Checking	[KV98]	Stefan Matzutt	Martin Leucker
5	18.06.	Automatische modulare Verifikation	[AAH+99]	Michael Matzutt	Martin Leucker
6	25.06.	Process Spaces	[Neg00]	Xiaoqiang Zhang	Martin Leucker
Reservethemen
-	-	Statecharts und ihre Semantik	[HN96]	-	-
-	-	Model Checking sequentieller hierarchischer Automaten	[AY98]	-	-
-	-	Verifikation paralleler hierarchischer Automaten	[BLA+99]	-	-
-	-	Kompositionelle Message Sequence Charts	[GMP01]	-	-
-	-	Hierarchische Petri-Netze	[Feh93, Buc94]	-	-

Literatur:

[HN96]: D. Harel, A. Naamad: The STATEMATE Semantics of Statecharts, ACM Transactions on Software Engineering 5(4), 1996, 293-333
[MLS97]: E. Mikk, Y. Lakhnech, M. Siegel: Hierarchical Automata as Model for Statecharts, LNCS 1345, 1997, 181-196
[AY98]: R. Alur, M. Yannakakis: Model Checking of Hierarchical State Machines, ACM Software Engineering Notes 23(6), 1998, 175-188
[BLA+99]: G. Behrmann, K. Larsen, H. Andersen, H. Hulgaard, J. Lind-Nielsen: Verification of Hierarchical State/Event Systems Using Reusability and Compositionality, LNCS 1579, 1999, 163-177
[GMP01]: E.L. Gunter, A. Muscholl, D. Peled: Compositional Message Sequence Charts, to appear in Proc. TACAS '01, available here
[Feh93]: R. Fehling: A Concept of Hierarchical {Petri} Nets with Building Blocks, LNCS 674, 1993, 148-168
[Buc94]: P. Buchholz: Hierarchical High-Level Petri Nets for Complex System Analysis, LNCS 815, 1994, 119-138
[DDG+89]: W. Damm, G. Döhmen, V. Gerstner, B. Josko: Modular Verification of Petri Nets, LNCS 430, 1989, 180-207
[Neg00]: R. Negulescu: Process Spaces, LNCS 1877, 2000, 199-213
[AH96]: R. Alur, T.A. Henzinger: Reactive Modules, Proc. 11th LICS, IEEE, 1996, 207-218
[KV98]: O. Kupferman, M.Y. Vardi: Modular Model Checking, LNCS 1536, 1998, 381-401
[AAH+99]: R. Alur, L. de Alfaro, T.A. Henzinger, F. Mang: Automating Modular Verification, LNCS 1664, 1999, 82-97

Thomas Noll, Letzte Änderung: 28.05.2001

Webmaster

Disclaimer

Last modified: 2002-11-08 14:35 UTC