Humboldt-Universität zu Berlin, Institut für Informatik, Prof. Dr. Holger Schlingloff, Dr. Jens Gerlach
Vorlesung und Übung "Software-Verifikation 1: Deduktive Verifikation"


Zeiten: Donnerstag 13:15 – 14:45, 4.112, Rudower Chaussee 25 (RUD25)
Übung: Donnerstag 15:15 – 16:45, 4.112, Rudower Chaussee 25 (RUD25)

Aktuelle Hinweise

Vorlesungsunterlagen
Alle Foliensätze und Materialien (C) H. Schlingloff 2011. Verwendung gestattet nur für den prvaten eigenen Gebrauch; Weitergabe nur mit vorheriger schriftlicher Genehmigung!

Übungsblätter
Alle Aufgaben (C) H. Schlingloff, J. Gerlach 2011. Verwendung gestattet nur für den privaten eigenen Gebrauch; Weitergabe nur mit vorheriger schriftlicher Genehmigung!
Abgabe per Mail an jens.gerlach at first.fraunhofer. de

Übungsunterlagen:



Materialien

Empfohlene Literatur


Modulbeschreibung

Inhalt:
Je mehr Software in sicherheitskritischen Systemen eingesetzt wird, umso wichtiger wird es, ihre Korrektheit objektiv nachzuweisen. Beispiele sind Signalisierungsanlagen in der Bahntechnik, Steuercomputer in Flugzeugen oder Regelungen medizinischer Geräte. In den letzten Jahren sind formale Verifikations- und Analysemethoden für solche Software so weit entwickelt worden, dass sie auch für industriell relevante Probleme einsetzbar geworden sind. Zu den Eigenschaften, die formal nachweisbar sind, gehören z.B. die Abwesenheit von arithmetischen Überläufen bzw. Nulldivisionen, Speicherfehlern, oder „toten“ Codes. Der Einsatz dieser Methoden wird von den einschlägigen Normen für hochgradig sicherheitsrelevante Software dringend empfohlen. Aber auch bei der Entwicklung von Treibern und Standardsoftware für weitverbreitete Betriebssysteme werden statische und dynamische Analysewerkzeuge eingesetzt.
Teil 1 dieses Moduls beschäftigt sich mit Methoden der deduktiven Verifikation, bei der die Beweise interaktiv vom Benutzer mit einem Beweissystem geführt werden. Teil 2 (im SS 2012) behandelt die automatische Verifikation mit Modellprüfung. Beide Teile können auch unabhängig voneinander besucht werden.

Qualifikationsziele:
Dieser Modul gibt einen Überblick über die wichtigsten formalen Methoden zur Software-Verifikation. Die Teilnehmer erlernen anhand verschiedener Werkzeuge, wie die entsprechenden Methoden in der Praxis eingesetzt werden können. Themen sind die statische Analyse durch abstrakte Interpretation, deduktive Verifikation, Modellprüfung und Programmtransformation. Alle Methoden werden an Hand frei verfügbarer Werkzeuge eingeführt und durch praktische Übungen untermauert.
Das Modul findet in Zusammenarbeit mit Fraunhofer FIRST statt. Von den Teilnehmern wird neben der regelmäßigen Teilnahme die Bearbeitung der Übungsaufgaben mit den entsprechenden Werkzeugen (unter Linux bzw. Windows) erwartet.

Organisatorisches:

Der Wert des Moduls beträgt 8 Studienpunkte (etwa 240 Arbeitsstunden); die Arbeitsleistungen, auf deren Grundlage die Studienpunkte vergeben werden, sind Abhängig von der Teilnehmerzahl findet nach Semesterabschluß eine mündliche (30 Minuten) oder schriftliche Prüfung (180 Minuten) über die Inhalte des Moduls statt.
Das Modul wird in diesem Semester erstmals angeboten und frühestens im WS 2014 wiederholt.

Veranstalter:

Vorläufige Vorlesungsplanung:


H. Schlingloff / J. Gerlach, Okt.2011