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


Zeiten: Dienstag 11:15-12:45, Donnerstag 9:15 – 10:45, 1.307, Rudower Chaussee 26 (RUD26)
Übung: Dienstag 13:15 – 14:45, 1.307, Rudower Chaussee 26 (RUD26)

Aktuelle Hinweise

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

Übungsblätter
Alle Aufgaben (C) H. Schlingloff, E. Pavese 2017. Verwendung gestattet nur für den privaten eigenen Gebrauch; Weitergabe nur mit vorheriger schriftlicher Genehmigung!
Abgabe per Moodle; als pdf mit dem Namen Abgabe-Blatti_Name.pdf

Ü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. Dieser Kurs behandelt die automatische Verifikation mit Modellprüfung, bei der eine Eigenschaft

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 9 Studienpunkte (etwa 270 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 dieser Form erstmals angeboten und frühestens im SS 2019 wiederholt.

Veranstalter:

Vorläufige Vorlesungsplanung:


H. Schlingloff, Apr.2017