Home  |  Impressum  |  Datenschutz  |  Sitemap  |  KIT

Formale Systeme II: Anwendung

Vorlesung im Sommersemester 2019

Prof. Dr. Bernhard Beckert, Dr. Mattias Ulbrich


Zielgruppe: Master Informatik
Umfang: 3 SWS, 5 ETCS
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

Aktuelle Hinweise

10.7.19: Am Dienstag, den 16.7. findet zur gewohnten Vorlesungszeit das Meet and Prove statt, bei dem aktuelle Themen des Lehrstuhl vorgestellt werden und kleinere Beweisaufgaben gelöst werden können. Wenn Sie an der Veranstaltung teilnehmen wollen, melden Sie sich bitte kurz formlos unter jonas.schiffl@kit.edu an.

3.5.19: Bitte bringen Sie (falls verfügbar) einen Rechner mit installiertem Java (>= 8) für die Veranstaltung am Dienstag, 7.5.19 mit.
Die Vorlesung am 7.5. findet im Raum 131 statt.

28.4.19: Am Dienstag, 30.4.19 findet die Vorlesung statt. Am Freitag, 3.5.19 findet keine Vorlesung statt.

Ü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.

Software:
  • RODIN installieren
  • Relevante Plugins: Diese müssen für Grundfunktionalität installiert werden über den Menüpunkt "Help → Install New Software ...".
    • Atelier B Provers - http://methode-b.com/update_site/atelierb_provers > Atelier B Provers
    • Rodin - http://rodin-b-sharp.sourceforge.net/updates > Prover Extensions > SMT Solvers Integration (Erklärung)
    Beide Einträge sind im Dropdown-Menu vorhanden.
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

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

Model Checker SPIN

Spin ist ein Modelchecker der ersten Stunde. Mit ihm untersuchen wir, wie nebenläufige oder verteilte Systeme modelliert und verifiziert werden können.

Wenn Sie Spin installieren, ist ein C-Compiler (z.B. gcc) notwendig, um es in vollem Umfang nutzen zu können.

Es gibt auch ein Web-Frontend zu Spin (Alternatives Web-Frontend).

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

Dies kann sich noch ändern.

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:
to top