![[Mail]](../../../Images/umschlag.gif)
| Benedikt Bollig | Disclaimer | Last modified: 2002-11-28 08:41 UTC |
![[I2 logo]](../../../Images/i2.gif)
![[RWTH logo]](../../../Images/rwth-rot90.gif)
(Informatik 2)
HomeNewsJobsContactStaffTeachingResearchMOVES SeminarDFG-GK AlgoSynCS ChairsLuFG I2
|
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.
| Termin | Seminarist | Betreuer | Thema | Literatur | |
|---|---|---|---|---|---|
| 1. | fällt aus | N.N. | Michael Weber | UML | [SP99] |
| 2. | 24.10.2002 | Gereon Frey, Arndt Fröhlich | Michael Weber | SDL | [Hog89] Kapitel 5 |
| 3. | 31.10.2002 | Sebastian Dahlen, Piotr Kornatowski | Benedikt Bollig | Estelle | [Hog89] Kapitel 3 |
| 4. | 07.11.2002 | Katja Gruber, Jennifer Herrmann | Benedikt Bollig | LOTOS | [Hog89] Kapitel 4 |
| 5. | 14.11.2002 | Brice Gaetan Ntchoumou, Matthias Poser | Benedikt Bollig | Z | [Wor92] |
| 6. | fällt aus | N.N. | Darius Dlugosz | VHDL | [Maz95] |
| 7. | 28.11.2002 | Georg Richlofsky, Sven Theissen | Benedikt Bollig | Message Sequence Charts (MSCs) | [Ren98] Kapitel 2 |
| 8. | 05.12.2002 | Jonathan Heinen, Nina Gholizadeh | Benedikt Bollig | Promela | [Hol91] |
| 9. | 12.12.2002 | Ergang Song, Zhang Yan | Benedikt Bollig | Von MSCs zu Promela | [Gre97] S.65-S.89 |
| 10. | 19.12.2002 | Anna Lea Dyckhoff, Azadeh Nikookhesal | Darius Dlugosz | Jakarta | [Bar01] |
| 11. | 09.01.2003 | Ahmad Al-Nassre, Omar Malass | Benedikt Bollig | CCS I | [Mil99] Kapitel 2-4 |
| 12. | 16.01.2003 | Ye Jun, Xi Zhao | Benedikt Bollig | CCS II | [Mil99] Kapitel 5-7 |
| 13. | 23.01.2003 | Christian Charles, Evamarie Storch | Benedikt Bollig | Petri-Netze | [Rei86] Kapitel 1-4 |
| 14. | 30.01.2003 | Haobo Song, N.N. | Benedikt Bollig | Spezifikation und Verifikation I | [Ber01] Teile Kapitel 1-5 |
| 15. | 06.02.2003 | Mahir Kilic, Martin Oczko | Benedikt Bollig | Spezifikation 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.
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.
- Einführungsmaterial zu LaTeX aus dem LaTeX-Kurs
