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

Hier werden weitere Informationen folgen, wenn der Semesterbeginn ansteht.

Aktuelle Hinweise

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