Modulbeschreibung Formale Grundlagen der Informatik II
Bachelor-Pflichtmodul: Formale Grundlagen der Informatik II - Modellierung und Analyse paralleler und verteilter Systeme
1. Modulkennung
IP9
2. Studiengang
Bachelorstudiengang Informatik
3. Modulbezeichnung
Formale Grundlagen der Informatik II - Modellierung und Analyse paralleler und verteilter Systeme (PVS), engl.: Modelling and Analysis of Parallel and Distributed Systems
4. Modul-Verantwortlicher
Valk
5. Veranstalter/Dozent
Jantzen, Moldt, Valk, Wolfinger
6. Sprache
Deutsch mit deutsch- und englischsprachigem Lehrmaterial
7. Motivation, Bedeutung für / Stellung im Gesamtprogramm
Parallele und verteilte Systeme sind von zunehmender Bedeutung in Anwendungen aller Art, gleichzeitig aber wegen der Komplexität ihres Verhaltens besonders anfällig für fehlerbehaftete Behandlung aufgrund unpräziser Methoden. Daher sind „formal methods“ seit langem fester Bestandteil der Forschung und Entwicklung auf diesem Gebiet.
Diese Lehrveranstaltung verzahnt daher in besonderer Weise im Studiengang angebotene Inhalte der theoretischen mit solchen der praktischen Informatik, insbesondere solchen die aus der Befassung mit verteilter Software entstehen. So ist diese Veranstaltung, wie alle der theoretischen Informatik einerseits stark auf die Vermittlung von Methoden ausgerichtet, muss aber andererseits alle zentralen Inhalte des Gebietes abdecken.
Sie wird als Wahlpflichtmodul Theorie 1 eingeordnet.
Es werden exemplarisch zwei Formalismen zur Beschreibung und Analyse paralleler und verteilter Systeme behandelt: Petrinetze und Harel-Graphen (statecharts). Das erstere ist das bei weitem entwickelste Gebiet, in dem grundlegende Systemeigenschaften wie Verklemmungsfreiheit, Lebendigkeit und Fairness auch stellvertretend für andere Modelle behandelt werden. Harel-Graphen werden in Variationen in der objektorientierten Analyse eingesetzt. Beide Gebiete wachsen tendenziell zusammen und befruchten einander.
Monographien über verteilte Systeme (z.B. Tanenbaum, Coulouris et al.) behandeln zwar Verfahren zur Lösung von Problemen in verteilten Systemen in großer Vielfalt und rezeptartig, die zugrunde liegenden Algorithmen werden jedoch oft nicht ausformuliert oder gar verifiziert. Das erschwert deren Verständnis ungemein und führt zu unausgereiften Lösungen in der Praxis. Mit den Themen Auswahlalgorithmen, Zeitstempel, totales Broadcast, konsistente Datenreplikation und byzantinischer Konsens werden daher exemplarisch solche Grundlagenverfahren behandelt. Obwohl parallele Algorithmen konzeptionell ein Spezialfall von verteilten Algorithmen sind, unterscheiden sich die hier zu behandelnden Themen deutlich. Sie sind durch algorithmische Methoden für synchrone Mehrprozessorsysteme motiviert. Zu behandeln sind typische Vertreter wie paralleles Mischen und Sortieren und deren spezifische Komplexitätsmaße.
Die Analyse und Verifikation von parallelen und verteilten Systemen wird ebenfalls exemplarisch durch die Themen Model-Checking und Prozessalgebra behandelt. Verfahren des ersten Themas kommen der von der Industrie geforderten Bereitstellung von automatischen Verfahren entgegen. Die Anwendung von entsprechenden Tools setzt jedoch einige theoretische Grundkenntnisse wie temporale Logik und Erreichbarkeitsanalyse voraus. Prozessalgebra liefert kompositionale Modellierungsansätze und führt zu effektiven Verfahren der Verifikation. Dafür werden allerdings vertiefte theoretische Kenntnisse auch beim Werkzeuganwender erforderlich. Zunehmend werden sichere Kommunikationsmechanismen in verteilten Systemen erforderlich. Kryptoprotokolle und verschiedene Verschlüsselungsmethoden wehren Angreifer ab. Ihre Realisierung kann oft nur durch probabilistische Algorithmen erreicht werden. Das Thema Leistungsmodellierung basiert auf dem Einsatz von Wartesystemen und Wartenetzen und rundet die Behandlung von grundlegenden Begriffen für nebenläufigen Auftrags- oder Paketverkehr in Rechnernetzen durch Themen wie das „Gesetz von Little“ oder Verkehrsengpass und Sättigungsfüllung ab. Modellierungstechniken zur Zuverlässigkeitsbewertung paralleler und verteilter Systeme werden in Hinblick auf die Beurteilung der Lebensdauer, der Verfügbarkeit und Konnektivität von Kommunikationsnetzen behandelt.
8. Lernziele/Kompetenzen
8.1 Passung Leitbild
- Übungen mit Vorträgen und Kleinprojekten zur Stärkung der Vortrags- und Kooperationsfähigkeit
- Vermittlung von Fähigkeiten zum Erkennen von System- und Verhaltensstrukturen in Problembereichen und zur Analyse von Zusammenhängen
- Bewertung von Sachverhalten und deren Einordnung in auch fachübergreifende Zusammenhänge
- Einschätzung von Grenzen und Klassifikation der prinzipiellen Möglichkeiten zur Bewältigung von Komplexität mit Hilfe von theoretisch fundierten Aussagen
8.2 Grundlagen-/Faktenwissen
- Erlernen der formalen Konzepte der Modellierung und Analyse nebenläufiger Systeme auf Basis von unterschiedlichen Modellen
- Verständnis der Grundkonzepte der vermittelten Modelle und Verfahren
- Kennenlernen und vertiefen von Definitionsprinzipien und Beweistechniken
- Sequentialität, Parallelität (d.h. synchrone Prozesse) und Nebenläufigkeit (d.h. asynchrone Prozesse) als fundamentale Begriffe verstehen lernen
8.3 Methodenwissen
- Einsatz von Methoden der theoretischen Informatik zur Lösung von Problemen nebenläufiger Systeme
- Anwendung von Definitionsprinzipien und Beweistechniken in unterschiedlichen Bereichen und an typischen Beispielen
- Methoden zu Korrektheitsbeweisen von Modellen und Algorithmen
- Methoden zur Leistungs- und Zuverlässigkeitsbewertung von Rechnernetzen und verteilten Systemen
- Erkennen der Gemeinsamkeiten von Strukturen und Beherrschung des konzeptionellen Kerns der Modelle und Verfahren
- Behandlung von Phänomenen der Nebenläufigkeit und Parallelität
8.4 Transferkompetenz
- Fähigkeit zum Entwickeln neuer Definitionen sowie zur exakten Beschreibung von neuen Spezifikationen in allen Bereichen der Informatik und deren Anwendungen,
- Erkennen von Struktur und Verhalten in informatischen Problemstellungen und Übertragen der mathematischen Methoden zu deren präzisen Modellierung,
- Anwendung der vermittelten Techniken zur Formulierung und Analyse der Algorithmen in verteilten Systemen
8.5 Normativ-bewertende Kompetenz
- Den praktischen Wert von präzisen Beschreibungen erkennen,
- Beurteilung der Qualität von Algorithmen und computergeeigneten Verfahren im Hinblick auf Korrektheit, Zuverlässigkeit, Effizienz und Vollständigkeit,
- Erkennen der grundlegenden Beschränktheit gegebener automatisierter Verfahren oder der Nichtexistenz von gewünschten Algorithmen.
8.6 ABK/BOK/Schlüsselqualifikationen
- Kooperations- und Teamfähigkeit in den Präsenzübungen,
- Strategien des Wissenserwerbs: Kombination aus Vorlesung, Vor- und Nachbereitung am Vorlesungsmaterial, Präsenzübungen mit betreuter Gruppenarbeit und eigenständiges Lösen von Übungsaufgaben
- Kreatives Spezifizieren am Beispiel der Entwicklung von Netzen, Harel-Graphen, Logik und Algorithmen
- Entwicklung von Modellen zur Leistungs- und Zuverlässigkeitsbewertung und zur Charakterisierung von Netzlasten
9. Lehrveranstaltungen
- 4 SWS Vorlesung Modellierung und Analyse paralleler und verteilter Systeme
- 2 SWS Übungen mit Seminaranteilen (Übungen mit Vorträgen und Kleinprojekten zur Stärkung der Vortrags- und Kooperationsfähigkeit, Kleingruppen)
10. Inhalt
10.1 Petrinetze
- Grundprinzipien der Netztheorie: Dualität von Transitionen und Stellen, Lokalität und Nebenläufigkeit, textuelle und graphische Darstellung,
- einfache Netze mit Vergröberung und Verfeinerung, Kausalnetze und Prozesse
- kantenkonstante und S/T-Netze, gefärbte Netze,
- Basiseigenschften: Invarianten, Beschränktheit, Lebendigkeit, Fairness, Zustandsraum und dessen Analyse
- Objekt-Petrinetze unter Wert- und Referenzsemantik
10.2 Harel-Graphen
- Abstraktion und Interaktion als Strukturierungstechnik
- Unterschiedliche Semantiken
- Bezug zu Objektorientierung
10.3 Parallele Algorithmen
- Das Modell der PRAM
- Grenzen der Parallelisierbarkeit
- Maschinenklassen
- Kommunikationsnetzwerke: Hypercube etc.
- paralleles Suchen und optimales Mischen
- parallele Maximumssuche und paralleles Sortieren
10.4 Verteilte Algorithmen
- zentralisierte vs. verteilte Algorithmen
- Auswahlprobleme
- logische und vektorielle Zeitstempel,
- kausales und totalgeordnetes Broadcast, konsistente Datenreplikation
- fehlertolerante Kommunikation: Ausfall- und byzantinischer Konsens
10.5 Sichere Kommunikation
- Kryptoprotokolle
- randomisierte Algorithmen
10.6 Prozesskalküle
- BPA, CSP
- Bisimilarität vs. Äquivalenz
- Prozessterme, Rekursion und Fairness
10.7 Model-Checking
- Kripkestrukturen und LTL/CTL-Model-Checking
- Komplexität und oBDDs
- Fixpunktcharakterisierungen
- Partial-Order-Model-Checking
10.8 Leistungsmodellierung
- Grundlagen der Wahrscheinlichkeitsrechnung
- Wartesysteme und Wartenetze, operationale Modelle
- Gesetz von Little, Durchsatz- und Verweilzeitanalysen für elementare Wartesysteme/-netze
- Exemplarische Modelle für Kommunikationsnetze und ihre Komponenten
10.9 Zuverlässigkeitsmodellierung
- Lebensdauer, Verfügbarkeit, Netzkonnektivität
- k-aus-n-Strukturen
- "gracefully degrading systems"
- redundante Netztopologien
10.10 Lastmodellierung
- Spezifikation von Auftragssequenzen, Benutzerverhaltensautomaten
- Analytische Verkehrsmodelle (u.a. "Packet Train"-, "ON/OFF"-Modelle)
- Transformation von Lastmodellen
11. Bezüge zu anderen Modulen
- Innerhalb des Studienganges: Im Rahmen der Pflichtmodule werden theoretische Grundlagen für die im Modul Grundlagen der Systemsoftware behandelten Themen gelegt. Die Einsicht in Erscheinungen nebenläufiger Systeme und die Kenntnis einschlägiger Methoden werden sowohl in Praktika und Projekten wie auch den Wahlpflichtmoduln Mensch-Computer-Interaktion, Eingebettete Systeme, Datenkommunikation und Rechnernetze, Grundlagen der Wissensverarbeitung, Informatikgestützte Gestaltung und Modellierung von Organisationen zum Teil grundlegend sein, zumindest aber Verwendung finden.
- Im konsekutiven Masterstudiengang: Auch für das Theorie-Pflichtmodul und die Wahlpflichtmodule Verteilte Systeme und Informationssicherheit und Datenbanken und Informationssysteme sowie Projekte und Vertiefungsmodule legt dieses Modul wesentliche Grundlagen.
- In anderen Studiengängen: Vertiefungsmodule des Master-Studiengangs Informatik bauen auf diesem Modul inhaltlich auf. Es eignet sich weiter als Bestandteil von Wirtschafts- und Bioinformatik-Studiengängen. Darüber hinaus ist ein Einbringen als Wahlmodul im Rahmen naturwissenschaftlicher Studiengänge möglich.
12. Modulvoraussetzungen
Verbindlich: keine
Empfohlen: Diskrete Mathematik, Formale Grundlagen der Informatik I, Analysis und lineare Algebra, Softwareentwicklung I, Rechnerstrukturen.
13. Semester, Studienjahr /-phase
Studienabschnitt: 1
Referenzsemester: 5
Empfohlenes Semester: 3
14. Prüfungsleistungen
Die Zulassung zur Modulprüfung setzt die regelmäßige und erfolgreiche Teilnahme
an den Übungen voraus; die Teilnahme gilt grundsätzlich als erfolgreich, wenn alle
Aufgaben bearbeitet und mindestens 50% richtig gelöst wurden; im Falle
abweichender Kriterien müssen diese zu Beginn der Veranstaltung bekannt
gemacht werden.
Gemeinsame Modulprüfung für alle Lehrveranstaltungen des Moduls; in der Regel
schriftlich (Klausur) und in deutscher Sprache; bei Modus-Abweichung Bekanntgabe
zu Beginn der Veranstaltung.
15. Bewertung
Gesamt: 9 Leistungspunkte
(Formale Grundlagen der Informatik II: 5 Leistungspunkte,
Übungen zu Formale Grundlagen der Informatik II: 4 Leistungspunkte)
16. Periodizität
Wintersemester, jährlich, Dauer: 1 Semester
17. Methodische Aufbereitung und Medienformen
- Vorlesung mit Beamer, Overhead und Tafel
- Vorlesungs- und Übungsmaterial wird online zur Verfügung gestellt
- Erwartete Aktivitäten der Studierenden: selbständiges Bearbeiten von Übungsaufgaben, aktive Mitarbeit in den Präsenzübungen
18. Literatur
18.1 Petrinetze, Harelgraphen, Prozessalgebra:
- W. Reisig. Petrinetze. Springer-Verlag, Berlin, 1985.
- C. Girault and R. Valk. Petri Nets for Systems Engineering - A Guide to Modeling, Verification, and Applications. Springer-Verlag, Berlin, 2003.
- Olaf Kummer. Referenznetze. Logos Verlag, Berlin, 2002. Dissertation, Univ. Hamburg. - - D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231–274, 1987.
- W. Fokkink. Introduction to Process Algebra. Springer-Verlag, 1999.
18.2 Parallele und verteilte Algorithmen
- J. Jájá. An Introduction to Parallel Algorithms. Addison Wesley Publ. Co., 1992
- H. Attiya and J. Welch. Distributed Computing. McGraw-Hill, 1998.
18.3 Sichere Kommunikation
- P. Ryan, S. Schneider. Modelling and Analysis of Security Protocols, Addison-Wesley, London, 2001
- J. Gruska. Foundations of Computing, Thomson Computer Press, London, 1997
18.4 Model-Checking
- E.M. Clarke, J.O. Grumberg, D.A. Peled: Model Checking, The MIT Press, Cambridge, 1999
- C. Girault, R. Valk: Petri Nets for Systems Engineering , Part III: Verification, Springer, Berlin, 2003,
18.5 Zuverlässigkeits-, Leistungs- und Lastmodellierung
- E. Jessen, R. Valk: Rechensysteme – Grundlagen der Modellbildung. Springer Verlag, Berlin, 1987.
- K. Heidtmann: Zuverlässigkeit technischer Systeme - Modelle für Zuverlässigkeitsstrukturen und ihre analytische Auswertung. Teubner-Texte zur Informatik 21, Teubner, 1997.
- M. Zaddach: Modellierung, Charakterisierung und Transformation von Videoverkehrslasten, Shaker-Verlag, Aachen, 2001.
