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


Zeiten: Die Veranstaltung findet als Kompaktvorlesung und Seminar am 9.1., 16.1. und 23.1. statt.

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

Materialien zum Kompaktseminar
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.
Dieser Teil, der unabhängig von der Veranstaltung im vergangenen SS ist, behandelt die automatische Verifikation mit Modellprüfung.

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.
Von den Teilnehmern wird neben der regelmäßigen Teilnahme die Bearbeitung der Übungsaufgaben mit den entsprechenden Werkzeugen (unter Windows und Linux) erwartet.

Organisatorisches:

Der Wert des Moduls beträgt 5 Studienpunkte (etwa 130 Arbeitsstunden); die Arbeitsleistungen, auf deren Grundlage die Studienpunkte vergeben werden, sind Nach Semesterabschluß findet eine mündliche Prüfung (30 Minuten) über die Inhalte des Moduls statt.
Das Modul wird in diesem Semester erstmals angeboten und frühestens im SS 2018 wiederholt.

Veranstalter:


H. Schlingloff, Jan.2016