Softwareverifikation
Wann und Wo
Vorlesung: Dienstag, 11-13 Uhr, RUD 26, 1'307
Vorlesung: Donnerstag 9-11 Uhr, RUD 26, 1'307
Übung: Dienstag, 13-15 Uhr, RUD 26, 1'307
Wer
Dozent: Prof. Holger Schlingloff / Dr. Esteban Pavese
Beschreibung und Aufbau der Lehrveranstaltung
Je mehr Software in sicherheitskritischen Systemen eingesetzt wird, umso wichtiger wird es, ihre Korrektheit objektiv nachzuweisen. Beispiele sind Steuercomputer für Autos und Flugzeuge, Regelungen für medizinische Geräte usw..
In den letzten Jahren sind formale Verifikations- und Analysemethoden für solche Software entwickelt worden. Diese Methode wurden so stark entwickelt, dass sie auch für industriell relevante Probleme einsetzbar geworden sind. Übliche Softwarefehler wie arithmetisches Überlaufen, Nulldivisionen, Null-Zeiger oder unerreichbar Code, können automatisch von diesen Methoden entdeckt werden.
Vorlesungsplanung bis Semesterende (Änderungen möglich)
- Einführung
- Aussagenlogik
- Modellierung
- Temporale Logik (LTL, CTL, CTL*)
- Algorithmen zur Modellprüfung
- Symbolische Zustandsraumrepräsentation (BDDs)
- Abstraktion und Verfeinerung
- Realzeit-Modellprüfung
- Probabilistische Systeme
- Software Model Checking
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