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

Anwendung Formaler Verifikation

Vorlesung im Sommersemester 2015

Dr. Vladimir Klebanov und Dr. Mattias Ulbrich

Zielgruppe: Diplom Informatik, 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 und Freitag, 11:30-13:00
Erstmals: 14.04.13
LV-Nr. 2400093

Aktuelles

  • Keine Vorlesung am 1. Mai

Anwendung formaler Verifikation

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.

Einleitung

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:

Model Checker SPIN

Bitte installieren Sie Spin und das Frontend jspin auf Ihrem Rechner. Um Spin in vollem Umfang nutzen zu können, ist ein C-Compiler notwendig. Bei der Installation von jspin ist es nötig, die Pfade zu spin usw. in der Datei config.cfg korrekt anzugeben.

Es gibt auch ein Web-Frontend zu Spin.

Materialien

Lektüre:

Deduktive Verifikation nebenläfiger Programme in Isabelle/HOL

Rely-Guarantee ist eine Technik für die deduktive Verifikation nebenläufiger Programme. Sie wird in modernen Verifikationssystemen eingesetzt, wie z. B. dem Verifying C Compiler von Microsoft Research. Wir werden Rely-Guarantee anhand einer Formalisierung im generischen Beweiser Isabelle/HOL kennenlernen.

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

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

Material:


Diese Vorlesung basiert auf gleichnamigen Vorlesung von Prof. Dr. Bernhard Beckert, Dr. Vladimir Klebanov und Dr. Christoph Gladisch aus frühreren Semestern.
Link zu den Webseiten zu Vorlesungen der vergangenen Jahre: 2012, 2013

Vladimir Klebanov, Mattias Ulbrich