[I2 logo] [RWTH logo] MOVES: Software Modeling and Verification
(Informatik 2)
Computer Science / RWTH / I2 / Teaching / Seminar / SPEC2002
Printer-friendly

Proseminar Spezifikationssprachen für Verteilte Systeme

Wintersemester 2002/2003
Lehrstuhl für Informatik II
Grundstudium

Aktuelles

Die Vorträge finden jeweils donnerstags von 11:45 Uhr bis ca. 13:00 Uhr im Hörsaal AS (Templergraben 64, gegenüber dem Hauptgebäude) statt.

Inhalt

Spezifikationssprachen können als vereinfachte Programmiersprachen betrachtet werden. Mit ihnen lassen sich die wesentlichen Eigenschaften eines (Hard- oder Software-) Systems formal beschreiben, ohne dieses im Detail angeben zu müssen. Sie werden z.B. bei der schrittweisen Entwicklung verteilter Systeme eingesetzt. Aufgrund ihrer formalen Semantik bilden sie eine gute Grundlage für die Verifikation der damit erstellten Spezifikationen.

TerminSeminaristBetreuerThemaLiteratur
1.fällt ausN.N.Michael WeberUML[SP99]
2.24.10.2002Gereon Frey,
Arndt Fröhlich
Michael WeberSDL[Hog89]
Kapitel 5
3.31.10.2002Sebastian Dahlen,
Piotr Kornatowski
Benedikt BolligEstelle[Hog89]
Kapitel 3
4.07.11.2002Katja Gruber,
Jennifer Herrmann
Benedikt BolligLOTOS[Hog89]
Kapitel 4
5.14.11.2002Brice Gaetan Ntchoumou,
Matthias Poser
Benedikt BolligZ[Wor92]
6.fällt ausN.N.Darius DlugoszVHDL[Maz95]
7.28.11.2002
 
Georg Richlofsky,
Sven Theissen
Benedikt BolligMessage Sequence Charts
(MSCs)
[Ren98]
Kapitel 2
8.05.12.2002Jonathan Heinen,
Nina Gholizadeh
Benedikt BolligPromela[Hol91]
9.12.12.2002Ergang Song,
Zhang Yan
Benedikt BolligVon MSCs zu Promela[Gre97]
S.65-S.89
10.19.12.2002Anna Lea Dyckhoff,
Azadeh Nikookhesal
Darius DlugoszJakarta[Bar01]
11.09.01.2003Ahmad Al-Nassre,
Omar Malass
Benedikt BolligCCS I[Mil99]
Kapitel 2-4
12.16.01.2003Ye Jun,
Xi Zhao
Benedikt BolligCCS II[Mil99]
Kapitel 5-7
13.23.01.2003Christian Charles,
Evamarie Storch
Benedikt BolligPetri-Netze[Rei86]
Kapitel 1-4
14.30.01.2003Haobo Song,
N.N.
Benedikt BolligSpezifikation und
Verifikation I
[Ber01]
Teile Kapitel 1-5
15.06.02.2003Mahir Kilic,
Martin Oczko
Benedikt BolligSpezifikation und
Verifikation II
[Ber01]
Teile Kapitel 6-11

Literatur

Literaturhinweise sind der folgenden Tabelle zu entnehmen. Weitere Literatur finden Sie in der Informatikbibliothek. Auch der Katalog der Zentralbibliothek mag nützlich sein. Nutzen Sie auch das Internet. Dort sind viele Programmbeschreibungen vorhanden.

[Bar01]
G. Barthe et al.: Jakarta: A Toolset for Reasoning about JavaCard. Proceedings of e-SMART'01, LNCS 2140, Springer, 2001.
[Ber01]
B. Berard et al.: Systems and software verification. Springer, 2001.
[Gre97]
J.-C. Gregoire et al. (eds.): The SPIN verification system. Proceedings of the 2. workshop held at DIMACS, 1997.
[Hol91]
G.J. Holzmann: Design and Validation of Computer Protocols. Prentice Hall, 1991.
[Hog89]
D. Hogrefe: Estelle, LOTOS und SDL - Standard-Spezifikationssprachen für verteilte Systeme. Springer, 1989.
[Ren98]
M.A. Reniers: Message Sequence Chart: Syntax and Semantics. PhD Thesis, Eindhoven University of Technology, 1998.
[Maz95]
S. Mazor, P. Langstraat: A Guide to VHDL. Kluwer Academic Publishers, 1995.
[Mil99]
R. Milner: Communicating and Mobile Systems: the pi-Calculus. Cambridge University Press, 1999.
[Rei86]
W. Reisig: Petrinetze. Eine Einführung. Zweite Auflage. Springer, 1986.
[SP99]
P. Stevens, R. Pooley: Using UML: software engineering with objects and components. Addison-Wesley, 1999.
[Wor92]
J.B. Wordsworth: Software Development with Z: A Practical Approach To Formal Methods in Software Engineering. Addison-Wesley, 1992.

Schein

Zum Erhalt des Scheins müssen Sie die folgenden drei Bedingungen erfüllen:
  • Sie halten einen Vortrag (jeweils ca. 30 Minuten);
  • vor dem Vortrag erstellen Sie eine Ausarbeitung (ca. 15 Seiten);
  • Sie nehmen an allen Vorträgen teil.
Vortrag und Ausarbeitung werden gemeinsam benotet. Diese Benotung wird auf dem Schein vermerkt; sie dient ausschließlich Ihrer Information und hat keinen Einfluss auf die Note des Vordiploms.

Betreuer

Jeder Teilnehmer bzw. jede Teilnehmergruppe hat einen wissenschaftlichen Mitarbeiter als Betreuer. Dieser berät Sie bei der Bearbeitung Ihres Themas. Sie sollten Ihren Betreuer mehrfach aufsuchen, um mit ihm Ihren Fortschritt zu besprechen. Sie sollten ihn mindestens kontaktieren um
  • die Literatur abzuholen;
  • ihm die von Ihnen gefundene Literatur zu zeigen;
  • ihm den Entwurf der Struktur der Ausarbeitung zu zeigen;
  • ihm einmal eine Ausarbeitung zu zeigen; diese wird er lesen und Ihnen anschließend Verbesserungsvorschläge machen;
  • ihm die Endversion der Ausarbeitung zu geben;
  • mit ihm die Struktur des Vortrags zu besprechen;
  • ihm einen Entwurf der Vortragsfolien zu zeigen.

Termine

Die Vorträge finden, beginnend mit der ersten Vorlesungswoche, wöchentlich statt. Es wird ferner erwartet, dass die folgenden Termine eingehalten werden:
  • Die angegebene Litaratur soll spätestens 10 Wochen vor dem Vortrag bei dem entsprechenden Betreuer abgeholt werden.
  • Sechs Wochen vor dem Vortrag  führen die Teilnehmer ein Gespräch mit dem Betreuer über die bis zu diesem Zeitpunkt vorliegenden Resultate. Insbesondere soll bei diesem Termin eine Gliederung besprochen werden.
  • Zwei Wochen vor dem Vortrag liegt dem Betreuer die letzte Version der Ausarbeitung vor.
  • Eine Woche vor dem Vortrag wird die Ausarbeitung, in genügender Anzahl kopiert, zum Proseminartreffen mitgebracht (bzw. im Sekretariat des Lehrstuhls ausgelegt). Die Kopien können am Lehrstuhl angefertigt werden.

Ausarbeitung und Vortrag

Die Ausarbeitung kann mit einem beliebigen Textverarbeitungssystem erstellt werden. Wir empfehlen allerdings LaTeX.

Rückfragen

Benedikt Bollig Tel. 0241/80-21210
Valid HTML 4.01 Strict! Valid CSS!