Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
  • DE
Institut für Informationssicherheit und Verlässlichkeit (KASTEL) – Anwendungsorientierte Formale Verifikation
Startseite

Formale Systeme II: Anwendung

Vorlesung im Sommersemester 2017

Prof. Dr. Bernhard Beckert, Dr. Mattias Ulbrich

Zielgruppe: Master Informatik
Umfang: 3 SWS
Vertiefungsfächer: Theoretische Grundlagen und Softwaretechnik und Übersetzerbau
Ort: SR 236 (Geb. 50.34)
Zeit: Dienstag, 11:30 - 13:00 Uhr
Freitag, 11:30 - 13:00 Uhr
Veranstaltungs-Nr.: 2400093

Aktueller Hinweis

Aufgrund von Koordinationsproblemen fand entgegen der Ankündigung am Freitag, 21.07.2017 keine Vorlesung statt. Die Veranstaltung wird aber am Dienstag 24.07.2017 nachgeholt werden. Herr Dr. Sinz wird die zweite Veranstaltung zu "Abstrakte Interpretation" am 28.07. durchführen.

Termine

An 21 von den 28 möglichen Terminen finden Vorlesunge/Übungen statt. An welchen Tagen keine Vorlesung/Übung stattfindet, wird hier rechtzeigt bekanntgegeben. An den nicht genannten Tagen finden Vorlesungen/Übungen statt.

Fr., 05. Mai 2017
Fr., 26. Mai 2017
Fr., 16. Juni 2017
Fr., 30. Juni 2017
Fr., 7. Juli 2017
Di., 11. Juli 2017
Fr., 28. Juli 2017

Überblick

Methoden für die formale Spezifikation und Verifikation - zumeist auf der Basis von Logik und Deduktion - haben einen hohen Entwicklungsstand erreicht. Es ist zu erwarten, dass sie zukünftig traditionelle Softwareentwicklungsmethoden ergänzen und teilweise ersetzen werden. Formale Methoden haben den Bereich akademischer Fallstudien hinter sich gelassen, und die Softwareindustrie zeigt ernsthaftes Interesse.

Nahezu sämtliche formale Spezifikations- und Verifikationsverfahren haben zwar die gleichen theoretisch-logischen Grundlagen, wie man sie etwa in der Vorlesung "Formale Systeme" kennenlernt. Zum erfolgreichen praktischen Einsatz müssen die Verfahren aber auf die jeweiligen Anwendungen und deren charakteristischen Eigenschaften abgestimmt sein. An die Anwendung angepasst sein müssen dabei sowohl die zur Spezifikation verwendeten Sprachen als auch die zur Verifikation verwendeten Kalküle.

Auch stellt sich bei der praktischen Anwendung die Frage nach der Skalierbarkeit, Effizienz und Benutzbarkeit (Usability) der Verfahren und Werkzeuge.

Angedachte Themen sind

  • Deduktive Verifikation mit KeY
  • Bug Finding für imperative Programme mit Software Bounded Model Checking
  • Modellierung und Refinement mit Event-B
  • Informationsfluss-Eigenschaften
  • Temporallogische Eigenschaften mit Model Checking
  • Echtzeiteigenschaften, Timed Automata mit UPPAAL

Materialien und Lektüre zu den einzelnen Themen

Einleitung

  • Folien zu Organisatorisches/Motivation (25.05.17): 00Intro.pdf

Verifikation funktionaler Eigenschaften imperativer und objekt-orientierter Programme

In dieser ersten Einheit geht es darum, die Spezifikation und formale Verifikation von Programmcode in wirklich eingesetzten Programmiersprachen kennenzulernen. Wir betrachten dazu die Programmiersprache Java und die Spezifikationsprache JML (Java Modeling Language). Als Werkzeug verwenden wir den Theorembeweiser KeY.

KeY wird am KIT, der TU Darmstadt, und an der Chalmers University of Technology in Göteborg entwickelt. Es ist ein Softwareverifikationswerkzeug, mit dem die Übereinstimmung von Java-Programmen und ihrer Spezifikation formal bewiesen werden kann. Das KeY-System besitzt eine graphische Benutzeroberfläche und ist komplett in Java geschrieben, so dass es auf jeder Plattform, für die eine virtuelle Maschine für Java zur Verfügung steht, lauffähig ist. Bitte installieren Sie KeY auf Ihrem Rechner. Entpacken Sie dazu die unten stehende ZIP-Datei und starten Sie die Datei KeY.jar. Falls Sie nicht schon zuvor Erfahrung mit KeY gesammelt haben (z. B. in der Übung zur Vorlesung Formale Systeme), arbeiten Sie bitte die Einführung zum Beweisen von prädikatenlogischen Formeln mit KeY durch.

Materialien:
Lektüre:

Abstrakte Modellierung und formale Verfeinerung mit Event-B

Formale Modellierung bereits zu einer sehr frühen Zeit während des Entwurfs hilft Kosten bei der Fehlersuche und -behebung zu verringern. Wir werden mit Hilfe der Technologie Event-B abstrakte formale Modelle formulieren und Verfeinerung im Werkzeug RODIN beweisen.

Materalien
Lektüre:
  • Jean-Raymond Abrial: Modelling in Event-B, System and Software Enginieering, Cambridge University Press, 2010
  • Jean-Raymond Abrial: The B-Book: Assigning programs to meanings, Cambridge University Press, 1996

Bounded Model Checking von C-Programmen mit LLBMC

Bounded Model Checking erlaubt die präzise Prüfung von Laufzeitfehlern systemnaher Programme. LLBMC ist eine Implementierung dieses Verfahrens, basierend auf dem LLVM Compiler-Framework.

Materalien

Model Checker SPIN

Bitte installieren Sie Spin. Um Spin in vollem Umfang nutzen zu können, ist ein C-Compiler notwendig.

Es gibt auch ein Web-Frontend zu Spin.

Materialien
Lektüre:

Verifikation von Informationsflusseigenschaften

Sicherheit und Information sind Schlagworte, die in vielen aktuellen Fragen eine bedeutende Rolle spielen, von cloud computing, big data, smart grid bis zu PRISM und zur NSA. Formale Methoden können dazu beitragen, den Informationsfluss in Programmen zu analysieren und zu verifizieren, dass kein unerlaubter Fluss von Information stattfindet.

Mit Hilfe von KeY wird deduktiv Noninterferenz von kleinen Javaprogrammen bewiesen. Typsysteme und graphbasierte Verifikationsansätze werden ebenso beleuchtet wir Grundlagen der quantitativen Informationsflussanalyse.

Materialien:

Verifikation von Echtzeiteigenschaften: UPPAAL

UPPAAL ist eine Toolumgebung zur Modellierung, Validierung und Verifikation von Echtzeitsystemen, die als Timed-Automata modelliert werden.

Eine Installationsanleitung befindet sich in dem Paket, welches auf der Projektseite zum Download zur Verfügung steht.

Materialien:

Verifikation von C-Programmen mittels Abstrakter Interpretation

Häufig genügt es, eine Abstraktion der eigentlichen Werte im Programm zu verwenden, um Programmeigenschaften zu zeigen. Die Analyse kann dadurch aber leichter werden oder gar erst ermöglicht werden. Hier lernen wir die Technik der Abstrakten Interpretation näher kennen und als Werkzeug das Kommerzielle Tool Polyspace von Mathworks, für das wir eine Campuslizenz haben.

Materialien