Verifikation von Software
Wann und Wo
Vorlesung: Dienstag, 9-11 Uhr; RUD 25, 3.113
Vorlesung: Donnerstag, 9-11 Uhr; RUD 25, 4.112
Übung: Dienstag, 11-13 Uhr; RUD 25, 3.113
Wer
Dozent: Prof. Holger Schlingloff / Lennart Siefke, M.Sc.
Beschreibung und Aufbau der Lehrveranstaltung
Um sicherheitskritische Systeme in der Praxis einsetzen zu können, muss die Korrektheit der Software objektiv nachgewiesen werden. Zur Zulassung von Systemen wie etwa Signalisierungsanlagen in der Bahntechnik, Steuercomputer in Flugzeugen oder Regelungen medizinischer Geräte empfehlen die einschlägigen Normen (EN 61508, EN 50128 oder DO-178C) den Einsatz formaler Methoden. In den letzten Jahren sind formale Verifikations- und Analysemethoden so weit entwickelt worden, dass sie auch für Probleme von industriell relevanter Größe einsetzbar geworden sind. Bei der Modellprüfung (Model Checking) wird ein Modell des Systems bezüglich einer temporallogischen Eigenschaft überprüft, und bei der dynamischen Analyse werden Laufzeiteigenschaften bezüglich spezifizierter Anforderungen untersucht. Zu den Eigenschaften, die formal nachweisbar sind, gehören z.B. die Abwesenheit von arithmetischen Überläufen bzw. Nulldivisionen oder die Erreichbarkeit von Fehlerzuständen und Lokalisierung „toten“ Codes. Ein neues Gebiet ist der Sicherheitsnachweis für lernende und adaptive Systeme.
Das Modul behandelt Methoden zur deduktiven Verifikation, bei der die Beweise interaktiv vom Benutzer mit einem Beweissystem geführt werden, sowie automatische Verifikationsverfahren, die in der industriellen Praxis eingesetzt werden.
Die Vorlesung gibt einen Überblick über die wichtigsten formalen Methoden zur Software-Verifikation.
In den Übungen erlernen die Teilnehmer, wie die entsprechenden Methoden in der Praxis eingesetzt werden können. Es wird das praktische Arbeiten und der Umgang mit verbreiteten Werkzeugen der Verifikation von Software geübt.
In Abgrenzung zum Bachelor-Modul W09-01 (Software-Verifikation) geht dieses Master-Modul auch auf neuere Techniken wie Abstraktionsverfeinerung anhand von Gegenbeispielen, erweiterte temporale Logiken, Erfüllbarkeit modulo Theorien und die Verifikation neuronaler Netze ein.
Die Teilnahme am Bachelor-Modul ist explizit nicht Voraussetzung für die Teilnahme an diesem Master-Modul; eine Teilnahme an beiden Modulen ist nicht möglich.
Skript und Übungsaufgaben
Alle Materialien zur Vorlesung werden in Moodle zur Verfügung gestellt. Das Passwort zum Kursbeitritt wird in der ersten Veranstaltung bekanntgegeben.
Änderungen an den Terminen und am genauen Inhalt sind (auch kurzfristig) möglich, werden aber im Normalfall auf dieser Webseite und in der Vorlesung bekanntgegeben.
Die Übungsblätter werden spätestens in der dem Übungstermin vorausgehenden Woche in Moodle zur Verfügung gestellt. Dort befinden sich auch die Folien zu den Übungen.
Voraussetzungen und Prüfung
Grundlagenkenntnisse in Logik und Graphtheorie werden vorausgesetzt.
Für die Zulassung zur Prüfung ist ferner die Teilnahme am Übungsbetrieb verpflichtend.
Die Lehrveranstaltung wird mit entweder eine mündliche Prüfung (etwa 30 Minuten) oder einer 180-Minuten schriftlichen Klausur geprüft. Für schriftliche Prüfungen ist ein beidseitig beschriebener (auch maschinell) DIN A4 Zettel als Zugelassenes Hilfsmittel erlaubt.
Literatur
- Principles of Program Analysis . Flemming Nielson, Hanne Riis Nielson, Chris Hankin.
- Modern compiler implementation in Java, Andrew Appel, 2nd. edition.
- Edmund M. Clarke, Orna Grumberg, Doron Peled. Model Checking. MIT Press, 2000.
- Jeff Magee and Jeff Kramer. Concurrency: State Models & Java Programs. John Wiley & Sons, 2000.
- Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008