Formale Methoden des Systementwurfs

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 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.

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, R 104, 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. 

Literatur

• B. Steffen, O.Rüthing, M. Isberner. Grundlagen der höheren Informatik, Band 1: Induktives Vorgehen. Springer-Verlag 2014. (Auch verfügbar via Springer-Link  - Zugriff aus dem Uninetz erforderlich).
• Krzystof R. Apt and Ernst-Rüdiger Olderog, Programmverifikation, Springer-Verlag, 1994
• B. Bérard, M. Bidoit, A. Finkel, F. Larroussinie, A. Petit, L. Petrucci, Ph. Schnoebelen, Systems and Software Verification, Springer-Verlag, 2001
• Eike Best, Semantik – Theorie sequentieller und paralleler Programmierung, Vieweg, 1995
• E.M. Clarke, Jr., O. Grumberg, D. Peled, Model Checking, MIT Press, 1999
• Hans Hüttel, Transitions and Trees - An Introduction to Structural Operational
  Semantics, Cambridge University Press. (Auch kapitelweise als PDF abrufbar  - Zugriff aus dem Uninetz erforderlich)
• Jacques Loeckx, Kurt Sieber, The Foundations of Program Verification, Wiley-Teubner, 1987
• Hanne Riis Nielson and Flemming Nielson, Semantics with Applications – A Formal Introduction, John Wiley and Sons, 1992
• Flemming Nielson, Hanne Riis Nielson, Chris Hankin, Principles of Program Analysis, Springer-Verlag, 1999  (PDF verfügbar über Link)  
• Robin Milner, Communication and Concurrency, Prentice-Hall, 1989
• Ernst-Rüdiger Olderog, Bernhard Steffen, Kapitel "Formale Semantik und Programmverifikation" in Informatik-Handbuch (Hrsg. Peter Rechenberg, Gustav Pomberger), Hanser, 2002
• Christel Baier, Joost-Pieter Katoen, Principles of model checking, Cambridge, 2008. (PDF verfügbar über Link)