Humboldt-Universität zu Berlin, Institut für Informatik, Prof. Dr. Holger Schlingloff, Dr. Jochen Burghardt
Vorlesung und Übung "Software-Verifikation 2: Automatische Verifikation"


Zeiten: Donnerstag 11:15 – 12:45, FIRST, Kekuléstr. 7, D318
Übung: Montag 13:15 – 14:45, FIRST, Kekuléstr. 7, D318

Aktuelle Hinweise

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

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

Übungsunterlagen:



Materialien

Empfohlene Literatur

Originalartikel


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 II behandelt hauptsächlich automatisierte Methoden der Verifikation von eingebetteter Software und Hardware: Modellprüfung, Erfüllbarkeit und automatische Testverfahren, wie sie heute für sicherheitskritische Anwendungen gefordert 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, Apr.2012