MOVES: Software Modeling and Verification (Info 2)

MOVES: Software Modeling and Verification
(Informatik 2)

Prof. Dr. Ir. Joost-Pieter Katoen

Computer Science / RWTH / I2 / Teaching / Seminar / MSC2002

Printer-friendly

Seminar Message Sequence Charts
Sommersemester 2002
Lehrstuhl für Informatik II
Hauptstudium

Bemerkungen

Seminaristen, die ihren Platz nicht wahrnehmen wollen, werden gebeten, sich umgehend abzumelden. Das gebietet die Fairness angesichts einer langen Warteliste.

Zeitplan

Nehmen Sie bitte möglichst bald Kontakt mit ihrem Betreuer auf, um Ihre Teilnahme zu bestätigen, die Literatur zu sichten und den weiteren Zeitplan abzustecken. Der erste Vortrag findet in der ersten Vorlesungswoche statt. Bitte beachten Sie auch die allgemeinen Hinweise zur Ausarbeitung und zum Vortrag. Die folgenden Seiten bieten Latex-Makros zum Zeichnen von MSCs und Automaten an:

Soweit nicht anders angekündigt, finden die Vorträge jeweils donnerstags um 08:30 Uhr im Seminarraum des Lehrstuhls statt.

Rückfragen

Benedikt Bollig Tel. 0241/80-21210

Inhalt

Message Sequence Charts (MSCs) sind ein verbreiteter graphischer Formalismus zur Spezifikation verteilter Systeme. Ein MSC definiert eine Menge von Prozessen und eine Abfolge von Kommunikationsaktionen zwischen diesen Prozessen. Mengen von MSCs können dabei das gewünschte oder unerwünschte Verhalten eines verteilten Systems modellieren. Die Seminarvorträge sollen Charakterisierungen solcher Mengen und Möglichkeiten ihrer Analyse vorstellen.

Termine

Nr.	Datum	Thema	Literatur	Referent	Betreuer
Einführung in MSCs
1	fällt aus	Konzepte in MSCs	[R98]		Michael Weber
MSC-Sprachen
2	25. April	Reguläre MSC-Sprachen	[HMKT00a]	Christian Käunicke	Benedikt Bollig
3	fällt aus	Message Sequence Graphs	[HMKT00b]		Darius Dlugosz
4	13. Mai	Endliche Automaten und High-Level MSCs	[MP01]	Holger Grosse-Plankermann	Benedikt Bollig
5	16. Mai	Kompositionelle MSCs	[GMP01]	Stephan Swiderski	Benedikt Bollig
Analyse von MSCs
6	03. Juni	Inferenz von MSCs	[AEY00]	Markus Schlütter	Benedikt Bollig
7	06. Juni	Validierung von Message Sequence Graphs	[MPS98]	Carsten Kern	Benedikt Bollig
8	13. Juni	MSCs und Testen	[T01]	Roman Schätzle	Benedikt Bollig
9	fällt aus	Shared-variables interaction diagrams	[AG01]		Benedikt Bollig
10	27. Juni	Model Checking für Systeme mit beschränktem Puffer	[MR00]	Christoph Hempsch	Thomas Noll
11	04. Juli	Model Checking von Message Sequence Graphs	[M01]	Niels Duhme	Benedikt Bollig
12	11. Juli	Model Checking von erweiterten Message Sequence Graphs	[MM01]	Matthias Hensler	Benedikt Bollig
13	18. Juli	Puffer-Beschränkung für MSCs	[LM02]	Martin Habbecke	Benedikt Bollig

Literatur

[R98]

M.A. Reniers. Message Sequence Chart: Syntax and Semantics. PhD Thesis, Eindhoven University of Technology, 1998. (Kapitel 2)

[HMKT00a]

J. G. Henriksen, M. Mukund, K. Narayan Kumar, and P. S. Thiagarajan. Regular collections of message sequence charts. In Proc. of the 25th International Symposium on Mathemtical Foundations of Computer Science (MFCS'00), 2000.

[HMKT00b]

J. G. Henriksen, M. Mukund, K. Narayan Kumar, and P. S. Thiagarajan. On message sequence graphs and finitely generated regular MSC languages. In Proc. of the 27th International Colloquium on Automata, Languages and Programming (ICALP'00), 2000.

[MP01]

A. Muscholl and D. Peled. From Finite State Communication Protocols to High-Level Message Sequence Charts. In Proc. of the 28th International Colloquium on Automata, Languages and Programming (ICALP'01), 2001.

[GMP01]

E. Gunter and A. Muscholl and D. Peled. Compositional Message Sequence Charts. In Proc. of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'01), 2001.

[AEY00]

R. Alur and K. Etessami and M. Yannakakis. Inference of message sequence charts. In Proc. of the 22nd International Conference on Software Engineering, 2000.

[MPS98]

A. Muscholl and D. Peled and Z. Su. Deciding properties of message sequence charts. In Proc. of the 1st International Conference on Foundations of Software Science and Computation Structures (FOSSACS'98), 1998.

[T01]

Stephan Tobies et al. Formal Test Purposes and the Validity of Test Cases, 2001. unpublished.

[AG01]

R. Alur and R. Grosu. Shared variables interaction diagrams. In Proc. of the 16th IEEE International Conference on Automated Software Engineering, 2001.

[MR00]

B. Meenakshi and R. Ramanujam. Reasoning about message-passing in finite state environments.In Proc. of the 27th International Colloquium on Automata, Languages and Programming (ICALP'00), 2000.

[M01]

P. Madhusudan. Reasoning about Sequential and Branching Behaviours of Message Sequence Graphs. In Proc. of the 28th International Colloquium on Automata, Languages and Programming (ICALP'01), 2001.

[MM01]

P. Madhusudan and B. Meenakshi. Beyond Message Sequence Graphs. In Proc. of the 21st Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'01), 2001.

[LM02]

M. Lohrey and A. Muscholl. Bounded MSC Communication. In Proc. of the 5th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'02), 2002. to appear.

Webmaster

Disclaimer

Last modified: 2002-12-19 16:31 UTC