Beschreibung:

Die Vorlesung besteht aus zwei Teilen, die jeweils ein halbes Semester dauern.

Der erste Teil fokussiert sich auf die Modellierung von Nebenläufigkeit, wird vom Lehrstuhl „Modeling of Adaptive Systems“ veranstaltet und endet am 31.05.2017.

Der zweite Teil findet im Anschluss daran statt, wird vom Lehrstuhl „Dependability of Computing Systems“ durchgeführt und beschäftigt sich mit der programmiertechnischen Umsetzung in Java.
Näheres dazu unter: http://dc.icb.uni-due.de/

Zum Modul erfolgt eine modulbezogene Prüfung in der Gestalt einer Klausur über die gemeinsamen Ziele von Vorlesung und Übung (in der Regel: 90-120 Minuten). Vom Dozierenden wird zu Beginn der Veranstaltung festgelegt, ob die erfolgreiche Teilnahme Prüfungsvorleistung oder aber Bestandteil der Prüfung ist. Ist letzteres der Fall, so bilden die Teilleistungen zusammen mit der Abschlussprüfung eine zusammengesetzte Prüfung mit einer Endnote.

Qualifikationsziele:

Die Studierenden

• haben ein Verständnis für die Modellierung nebenläufiger Systeme
• kennen unterschiedliche Spezifikationstechniken für zustandsbasierte Systeme (Prozessalgebren, Petri-Netze, kommunizierende endliche Automaten und Ablaufmodelle)
• können Modelle erstellen und hinsichtlich ihrer Korrektheitseigenschaften formal untersuchen
• beherrschen Grundprinzip und Werkzeuge zum Model Checking für synchrone zeitbehaftete Automatenetze
• können die Modellierung auf Probleme des nebenläufigen Rechnens anwenden
• kennen die Synchronisationskonzepte des nebenläufigen Rechnens
• sind in der Lage, effiziente nebenläufige System zu konstruieren und die Vor- und Nachteile verschiedener Lösungsansätze vergleichend zu bewerten
• sind in der Lage, das nicht deterministische Verhalten von nebenläufigen Systemen durch Ablaufmodelle darzustellen und formal zu spezifizieren
• können Eigenschaften von Modellen formal beschreiben und diese durch modellgestützte Verfahren verifizieren oder falsifizieren
• beherrschen den Umgang mit Werkzeugen zur Erstellung und Behandlung (Animation, Verifikation, Model Checking) von Modellen nebenläufiger Systeme können praktische Aufgabenstellungen hinsichtlich Nebenläufigkeit analysieren und einer Implementierung zugänglich machen
• können nebenläufige Threads für die bekannten „klassischen“ Modelle programmieren und darüber hinaus auch Threads zur Implementierung beliebiger Synchronisationsalgorithmen einsetzen