Wie der ganze Zyklus "Formale Grundlagen der Informatik", beschäftigt sich diese
Vorlesung auf
mathematischer Basis mit Abstraktionen, Modellbildungen und Verfahren zur Beschreibung und
Analyse von Algorithmen und Prozessen. Formale Methoden spielen in der Informatik die
Rolle eines "Denkzeugs", mit dem der (abstrakte) Kern einer Sache knapp und präzise
beschrieben werden kann. Erst auf der Basis eines sauberen theoretischen Fundaments wird
es müglich, solche Beschreibungen zu formulieren und deren Analysen vorzunehmen. Parallele
und nebenläufige Programme und Prozesse sind wegen ihrer Komplexität besonders anfällig
für fehlerhafte Behandlung aufgrund unpräziser Methoden. Es ist daher kein Zufall, dass
"formal methods" in diesem Gebiet fester Bestandteil der Forschung und
Entwicklung sind. Die Vorlesung führt in die wichtigsten Phänomene und
Beschreibungstechniken ein. Sie werden z.T. an realen Programmen illustriert.
Zunächst werden parallele Programme und Nebenläufigkeit durch Prozessausdrücke
eingeführt. Diese Darstellung ist wie die Prozess-Algebra von R. Milner
stark auf Aktionen zentriert. Die Bedeutung der durch Grammatiken definierten
Prozessausdrücke wird durch Transitionssysteme (endliche Automaten) als operationale
Semantik dargestellt. Der Bezug zur Programmierung wird durch Java-Threads hergestellt.
Im 3. Kapitel werden Petrinetze auf drei Abstraktionsebenen eingeführt: als elementare
Netze, als kantenkonstante bzw. Platz/Transitionsnetze und als gefärbte Netze. Im
Gegensatz zur prozessoralen Sprache des vorigen Kapitels weisen Netze eine Ereignis-
und Zustands-Orientierung auf. Sie sind über die operationale Semantik der
Erreichbarkeitsgraphen mit ihr verbunden.
Das 4. Kapitel behandelt elementare Eigenschaften verteilter Systemmodelle wie
Invarianten, Lebendigkeit, Fairness und Beschränktheit. Lebendigkeit und Beschränktheit
werden am Thema der Analyse von Geschäftsprozessen (workflow) exemplarisch eingesetzt. Das
schon im 2. Kapitel am Beispiel behandelte Probleme der Dateninkonsistenz durch
nebenläufige Prozesse wird systematisch aufgegriffen. Mittels schematischer
Auftragsysteme werden die Eigenschaften der Funktionalität und maximalen
Nebenläufigkeit diskutiert.
Das 5. Kapitel beginnt mit Unteilbarkeit (Atomizität) als wichtigem Begriff bei
nebenläufigen Prozessen.
Grundformen der Synchronisation, wie Speicher- Rendezvous- und Nachrichten-Synchronisation
werden behandelt. Das Kapitel enthält auch einige klassische Konzepte und hochsprachliche
Synchronisations-Konstrukte.
Das 6. Kapitel führt in parallele Algorithmen ein, d.h. in zeitgetaktete
Parallelverarbeitung, wie sie auf der PRAM implementiert werden künnte, ohne diese jedoch
formal einzuführen. Im 7. Kapitel werden dagegen verteilte Algorithmen
behandelt, die auf dem Prinzip von kooperierenden
asynchronen Algorithmen beruhen. Zeitstempel sind hier ein verbreitets Konzept, um zentrale Synchronisation zu kompensieren. Durch Kausalnetze wird ein Bezug zur verteilten Semantik der Petrinetze hergestellt.
