Aufgrund der durch die Corona-Pandemie bedingten Verschiebung des Semesteranfangs auf den 20.04.2020 beginnt die Vorlesung frühestens am 20.04.2020 (näheres folgt). Nach Beschlusslage der TU Dortmund werden alle Veranstaltungen zunächst ausschließlich in digitaler Form (Screen-/Podcasts, Videokonferenzen) angeboten Die Vorlesungsinhalte werden im Moodle zum Download angeboten. Falls sich im Laufe des Semesters eine Verbesserung der Situation ergeben sollte und der Vorlesungsbetrieb ohne gesundheitliche Risiken aufgenommen werden kann, findet die Vorlesung wie geplant als Präsenzveranstaltung statt.
Komplexe Hard- und Softwaresysteme durchdringen immer mehr Lebensbereiche und werden zunehmend auch in Anwendungen eingesetzt, die hohe Anforderungen an Sicherheit und Verfügbarkeit stellen. Prominente Beispiele sind Flugzeug- und Bremssteuerungen, aber auch Anwendungen im Finanzbereich. Hier stößt klassisches Testen an seine Grenzen. Daher werden formale Methoden in diesen Gebieten jetzt auch in der industriellen Praxis rigoros eingesetzt: Während z.B. Airbus schon lange auf formale Methoden setzt, hat Boeing erst kürzlich den Einsatz formaler Methoden für obligatorisch erklärt. Formale Methoden zielen darauf ab, mit semantisch fundierten Techniken Aussagen über das Verhalten von Systemen zu überprüfen oder automatisch zu berechnen. Außer zu Validierungs- und Verifikationszwecken werden formale Methoden zunehmend auch zur automatischen 'Systemveredelung' eingesetzt, beispielsweiswe zur (Programm/Prozess) Optimierung, zur Erhöhung der Fehlertoleranz, oder zur Beherrschung der Systemevolution. Besonders konsequent werden diese Ansätze im Rahmen des "Model Driven Design" vorangetrieben, wo modell-basierte Verifikations-, Simulations-, Test- und Synthesemethoden zunehmend verschmelzen.
Die Vorlesung behandelt einen panoramischen Rundblick auf die relevanten Methoden, wobei sie insbesondere auf den Verschmelzungsaspekt eingeht. Der wird besonders im Kontext des praxis-orientierten Automatenlernes deutlich, einem Grenzgebiet zwischen dem dynamischen modell-basierten Testen und klassischen statischen formalen Methoden wie Programmanalyse und Modelchecking. Die konzeptuelle Einführung in die Thematik wird durch theoretische und praktische Übungen unter Einsatz entsprechender Softwarewerkezuge vertieft.
Die entsprechende Modulbeschreibung finden Sie unter Inf-Ba-223.
In den Übungen wird durch konkrete Aufgabenstellungen die Möglichkeit gegeben, das in der Vorlesung "Formale Methoden des Systementwurfs" theoretisch erworbene Wissen anzuwenden und zu festigen. Durch eine strukturierte Rekapitulation des Stoffes stellen die Übungen eine gute Voraussetzung für eine erfolgreiche Teilnahme an einer Prüfung über die Vorlesung "Formale Methoden des Systementwurfs" dar.
Die Übungen finden standardmäßig am Montag 16.15-17.45 Uhr (Haupttermin) in OH 14, R 104 statt. Ein weiterer kleinerer Übungstermin findet bei ausreichender Nachfrage nach Absprache mit den Teilnehmern statt.
Die Vorlesungsmaterialien (Folien, Skript, Übungsblätter) stehen in einem Moodle-Arbeitsraum zur Verfügung, der auch über die Vorlesungsseite im LSF verlinkt ist.