Die Vorlesung wird teilweise im "inverted classroom"-Stil angeboten. Dazu sollen Teilnehmer*innen sich Grundlagenmaterial basierend auf vertonten Vorlesungsfolien im Selbststudium aneignen. Näheres zum Ablauf der Vorlesung wird an einem initialen Präsenztermin in der Nachosterwoche bekanntgegeben.
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 voraussichtlich standardmäßig montags 12-14 Uhr und/oder 16-18 in Präsenz statt (OH 14, R104, Start nach Ankündigung).
Die Vorlesungsmaterialien (Folien, Videos, Konferenzlinks Übungsblätter) stehen in einem Moodle-Arbeitsraum zur Verfügung. Die Registrierung für den Raum soll ausschließlich über das LSF erfolgen.