|
Lehrende: Dr. Daniel Moldt
Veranstaltungsart:
Vorlesung
Anzeige im Stundenplan:
FGI 2 - VL
Semesterwochenstunden:
4
Credits:
5,0
Unterrichtssprache:
Deutsch
Min. | Max. Teilnehmerzahl:
- | 120
Kommentare/ Inhalte:
Prozesse und Nebenläufigkeit paralleler und verteilter Systeme sind von zunehmender Bedeutung in Anwendungen aller Art. Gleichzeitig sind solch komplexen Systeme aber wegen der Komplexität ihres Verhaltens besonders anfällig für fehlerbehaftete Behandlung aufgrund unpräziser Methoden. Daher sind formale Ansätze seit langem fester Bestandteil dieses Gebiets. Aus diesen Gründen betrachtet das Modul Analyse-, Verifikations- und Entwicklungsverfahren von parallelen und verteilten Systemen. Zur präzisen Bearbeitung ist die Modellierung der jeweiligen Systeme zwingend notwendig. Dafür sind ausreichend ausdrucksstarke Modellierungstechniken notwendig. Exemplarisch werden daher Büchi-Automaten, Temporallogik, Prozessalgebra und (höhere) Petrinetze vorgestellt. Dazugehörige Methoden der Analyse und Verifikation (Model-Checking, Komposition, Algorithmenentwurf, Berechenbarkeits- und Komplexitätsbetrachtungen, strukturelle und dynamische Analyse etc.) werden zielgerichtet behandelt.
Somit werden allgegenwärtige Konzepte der Informatik, wie Nebenläufigkeit, Synchronisation, Konflikt, Nicht-Determinismus, Verteilung, Verklemmungsfreiheit, Lebendigkeit, Fairness etc. wesentlich vertieft, da diese für die Entwicklung komplexer, verteilter Systeme zwingend notwendig sind. Ohne die Kenntnis dieser Konzepte könnten heutige Systeme nur laienhaft entwickelt werden. In diesem Modul werden die üblicherweise implizit vorausgesetzten Grundlagen systematisch explizit aufbereitet, so dass für Programme, Systeme und deren Modelle konkrete Aussagen bezüglicher ihrer Eigenschaften getroffen werden können. Fragen nach der Termination, Korrektheit oder Vollständigkeit werden explizit thematisiert. Wesentliche Phänomene von Web-Anwendungen, Programmiersprachen, Datenbanken, Betriebssystemen etc. werden somit grundlegend aufbereitet, um für die Analyse, Modellierung, Gestaltung und Bewertung von sogenannten Systemen-in-Systemen / Ultra-Large Scale Systems im Laufe des Studiums vorbereitet zu sein.
Lernziel:
Lernziel ist die Kenntnis, Beurteilung und Verwendung von formalen Methoden als Grundlage zur Programm- und Systementwicklung. Daher eignet sich die Veranstaltung nicht nur als Wahlmodul im Bachelorstudiengang „Informatik“, sonder auch in den Bachelorstudiengängen „Software-System-Entwicklung“, „Computing in Science“, „Mensch-Computer-Interaktion“ und "Wirtschaftsinformatik".
Vertieft werden vergleichbare Inhalte in dem nachfolgenden Bachelor/Master-Wahlpflichtmodul „Modellierung verteilter Systeme (MVS)“ regelmäßig im Sommersemester.
Mit diesem Modul werden zentrale Konzepte der Informatik erlernt. Mittels der erlernten Prinzipien, Methoden, Techniken und Werkzeuge können formale Eigenschaften von Systemen festgestellt, beschrieben, präzise modelliert, analysiert und implementiert werden.
Vorgehen:
Diese Lehrveranstaltung verzahnt in besonderer Weise bestimmte in den Studiengängen der Informatik 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 grundlegenden Veranstaltungen einerseits stark auf die Vermittlung von Methoden ausgerichtet, soll aber andererseits zentrale Inhalte des Gebietes abdecken.
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 im Gegensatz zu dieser Veranstaltung oft nicht ausformuliert oder gar verifiziert. Das erschwert deren Verständnis und führt zu unausgereiften Lösungen in der Praxis.
Verfahren des Model Checking kommen der von der Industrie geforderten Bereitstellung von automatischen Verfahren entgegen. Die Anwendung von entsprechenden Werkzeugen setzt jedoch einige theoretische Grundkenntnisse wie temporale Logik und Erreichbarkeitsanalyse voraus. Ebenso ist die Nutzung von Werkzeugen zur Leistungsanalyse auf höherem Niveau nur mit Kenntnis der formalen Grundlagen möglich.
Im Rahmen des gesamten Moduls werden daher diese Verfahren in der Vorlesung vorgestellt und detailliert diskutiert. In den zugehörigen, genau auf den Stoff abgestimmten Übungen werden neben den theoretischen Kenntnissen sowohl konzeptionelle als auch praktische Fähigkeiten im Bereich der Modellierung und Entwicklung komplexer Systeme erworben und vertieft.
Das Modul wurde letztes Jahr durch das Lehrlabor gefördert. Dadurch stehen uns nun besonders anspruchsvoll überarbeitete Lernhilfen zur Förderung des Lernerfolgs zur Verfügung. Dabei werden zum einen ein kooperatives Übungsgruppenkonzept und zum anderen ein begleitendes Lernen durch Online-Werkzeuge (Olat-Tests) unterstützt. Alle Materialien (Folien, Skript, Übungsaufgaben mit Musterlösungen etc.) werden zur Verfügung gestellt und um schon vorhandere Lecture2Go Aufzeichnungen und einen gemeinsamen Lernraum sowie zwei Repetitorien unterstützt.
Literatur:
Ausgewählte Inhalte aus
- C. Baier, J.-P. Katoen. Principles of Model Checking, The MIT Press, Cambridge, 2008.
- W. Fokkink. Introduction to Process Algebra. Springer-Verlag, 1999.
- C. Girault and R. Valk. Petri Nets for Systems Engineering - A Guide to Modeling, Verification, and Applications. Springer-Verlag, Berlin, 2003.
- J. Gruska. Foundations of Computing, Thomson Computer Press, London, 1997.
- M. Huth, D. Ryan, Logic in Computer Science - Modelling and Reasoning about Systems, Cambridge University Press, 1999
- E.M. Clarke, J.O. Grumberg, D.A. Peled: Model Checking, The MIT Press, Cambridge, 1999.
- E. Jessen, R. Valk: Rechensysteme Grundlagen der Modellbildung. Springer Verlag, Berlin, 1987.
Zur Unterstützung der Veranstaltung und des Übungsbetriebes werden verschiedene Programme eingesetzt, die im Rahmen der Veranstaltung bekannt gegeben werden.
Zusätzliche Hinweise zu Prüfungen:
Diese Veranstaltung eignet sich auch als Grundlage für die F4 Veranstaltung (Prüfungsordnung Diplom Wirtschaftsinformatik) und PNL (Prüfungsordnung Diplom Informatik).
Für diejenigen, die ihr Studium im Master fortsetzen wollen, wird FGI-2 empfohlen, da insbesondere das heutzutage allgegenwärtige Konzept der Nebenläufigkeit grundlegend vermittelt wird.
Das Modul eignet sich für alle Studiengänge!
|
