Hauptstudiumsgrundlagenveranstaltung zur Theoretischen Informatik im WiSe 2004/2005

18.111 Prozesse und Nebenläufigkeit (PNL)

Rüdiger Valk

4st. Di 10 - 12 Phil C mit integrierten Übungen, Do 8 - 10 Phil C

Zu der Veranstaltung werden zwei Tutorien angeboten, eines in der sechsten und eines in der siebten Kalenderwoche (die erste und zweite Woche der vorlesungsfreien Zeit). Aktuelle Gruppeneinteilung: 6. Woche und 7. Woche.

Die Tutorien finden jeweils am Montag, Mittwoch und Freitag in C-221 statt. Beginn ist 9:30. Jeder Tag ist in drei Blöcke unterteilt: 9:30 bis 11:00, 11:15 bis 12:45 und 13:30 bis 15:00.

Die Termine sind wie folgt organisiert:
Mo: Höhere Petrinetze; Verifikation und Model Checking; Prozesse und ihre Synchronisation
Mi: Prozessalgebra; Harel-Graphen; Systeme von Funktionseinheiten
Fr: Fehlertolerante Kommunikation und Symmetriebrechung

Eine Vorbereitung zu den einzelnen Terminen ist notwendig.

Lernziel:
	Die Vorlesung baut auf dem Grundstudiumszyklus "Formale Grundlagen der Informatik", insbesondere F4: "Parallelität und Nebenläufigkeit" auf. Die dort behandelten Themen hatten eher das Ziel, Grundphänomene verständlich zu machen. Diese Grundlagenveranstaltung soll dagegen verstärkt den Aspekt der formalen Methoden berücksichtigen. Im Vordergrund steht dabei die Behandlung verschiedener Formalismen zur Modellierung verteilter und paralleler Systeme, wobei die Betonung auf "verschiedene" liegt, sowie Methoden der Analyse und Verifikation.
Materialien:
	Skript (Version: Oktober 2004) Folien (Kapitel 2.1) Folien (Kapitel 2.2) Folien (Kapitel 2.3) Petrinetz zum ABP: PDF- und Renew-Dateien (zip-Archiv) Folien (Kapitel 3) Folien (Kapitel 4.1) Folien (Kapitel 4.2) Folien (Kapitel 4.3) Aufgabe 4.29 Feuerlöschen in Renew Folien (Kapitel 4.4) Folien (Kapitel 5.1) Folien (Kapitel 5.2) Folien (Kapitel 5.3) Folien (Kapitel 5.4) Folien (Kapitel 5.5) 4ofen-SMV-Datei Folien (Kapitel 6.1) Folien (Kapitel 6.2) Folien (Kapitel 6.3) Folien (Kapitel 6.4) Folien (Kapitel 7.1) Folien (Kapitel 7.2) Folien (Kapitel 8.1) Folien (Kapitel 9.1) Folien (Kapitel 9.2) Folien (Kapitel 9.3) Aufgabe 4.41 Aufgabe (Prozesse) Literaturhinweise
Stell. im Studienplan:
	Hauptstudium, Vertiefungsgebiete P10, P2, P3, P4, P5, P9, Th1, Th2, Th3, Th4, T1, T2; Schwerpunkte BV, ES, IM, INE, OSE, RNT, SEM, SV, VIS, WV
Voraussetzungen:
	Vordiplom
Vorgehen:
	Vorlesung mit Hörsaalübungen
Literatur:
	C. Girault, R. Valk: Petri Nets for Systems Engineering - A Guide to Modelling, Verification, and Applications, Springer, Berlin, 2001 O. Kummer: Introduction to Petri Nets and Reference Nets. Sozionik Aktuell, 1 (2001): http://www2.informatik.uni-hamburg.de/tgi/forschung/projekte/sozionik/journal/index.html W. Fokkink: Introduction to Process Algebra. Springer, Berlin, 2000 H. Attiya, J. Welch: Distributed Computing, McGraw-Hill, London. 1998 K. Jensen: Coloured Petri Nets, Vol. 1, EATCS Monographs on Theoretical Computer Science, Springer, Berlin, 1992 E. Jessen, R. Valk: Rechensysteme - Grundlagen der Modellbildungen, Springer, Berlin 1987 D. Harel: Statecharts: A Visual Formalism for Complex Systems. Science of Computer Programming, 8 (1987) 231-274
Periodizität:
	jährlich zum WS
Stichworte:
	Strukturelle Analyse, Model Checking, Verteilte Algorithmen, Verifikation, temporale Logik, Prozessalgebra, Statecharts, Petrinetze, Referenznetze