| 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. |
| Inhalt: |
| - Einleitung
- Prozessalgebra: Prozessgraphen und Prozessterme, Bisimulation und Äquivalenz, parallele und kommunizierende Prozesse, Rekursion und Abstraktion, Verifikation des Alternierbitprotokolls als Anwendung
- Harel-Graphen (Statecharts): der graphische Formalismus, Syntax und Semantik, eine Beispielanwendung
- Referenznetze: Verfeinerung und Vergröberung, gefärbte Petrinetze, Netz-Kanäle, Netz-Instanzen, Beispielsysteme
- Prozesse: logische und vektorielle Zeit, Zeitstempelverfahren, Kausalnetze, asynchrone und synchrone Prozesse
- Analyse: elementare Systemeigenschaften, Analyse, Verifikation durch den Erreichbarkeitsgraphen und strukturelle Eigenschaften
- Fehlertolerante Kommunikation in verteilten Systemen: einfacher und byzantinischer Konsens, exponentieller und polynomieller Algorithmus für byzantinischen Konsens, unentscheidbare Probleme
- Symmetriebrechung mit probabilistischen Verfahren: ein probabilistischer Algorithmus für Konsens, Auswahl und wechselseitigen Ausschluss
- Realisierung von Kommunikationsformen: Simulation von Broadcast-Nachrichten, kausale und totale Ordnung eintreffender Nachrichten, gemeinsamer Speicherzugriff in verteilten Systemen, Linearisierbarkeit und sequentielle Konsistenz von Datenzugriffen
- Verifikation und Model Checking: temporale Logik, CTL-Spezifikation, symbolisches und BDD-basiertes Model Checking (Binary Decision Diagrams), temporallogische Verifikationsmethoden
- Systeme von Funktionseinheiten: Handlung, Auftrag, Funktionseinheit, das Gesetz von Little, Systeme mit großer Füllung, Sättigungsfüllung
|
| Materialien:
|
|
Skript (Kapitel 1 - 4)
Skript (Kapitel 8 - 9)
Skript (Kapitel 11)
Korrekturblatt zum Skript
Aufgaben 1 - 2
Aufgaben 3 - 4
Aufgabe 5
Aufgabe 6
Aufgaben 7 - 8
Aufgabe 9
Aufgabe 11
|
| 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 |
Rüdiger Valk