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 2013

Dr. Christoph Gladisch

Diese Vorlesung basiert auf der gleichnamigen Vorlesung von Prof. Dr. Bernhard Beckert und Dr. Vladimir Klebanov

Zielgruppe: Diplom Informatik, Master Informatik
Umfang: 3 SWS
Vertiefungsfächer: Theoretische Grundlagen und Softwaretechnik und Übersetzerbau
Ort: SR 236 (Geb. 50.34)
Zeit: Do 11:30-13:00 und Fr 11:30-13:00
Erstmals: Do 18.04.13
LV-Nr. 24625

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.

Terminplan

Die Veranstaltung hat 3 SWS, also 21 Doppelstunden im Semester. (Der untere Plan enthält vorläufig mehr Stunden, von denen einige entfernt werden.) Entsprechend besteht jede der sieben Einheiten aus zwei Doppelstunden Vorlesung und einer Doppelstunde Übung, in denen die Verfahren anhand konkreter Verifikatiossysteme von den Studierenden praktisch erprobt werden. Vorlesung und Übung gehen dabei fließend ineinander über.

Dieser Plan ist nicht endgültig. Änderungen sind möglich.

Donnerstag, 11:30-13:00, SR 236 Freitag, 11:30-13:00, SR 236
18.04.13: V/Ü 19.04.13: V/Ü
25.04.13: V/Ü 26.04.13: V/Ü
02.05.13: V/Ü 03.05.13: V/Ü
09.05.13: --- (Chr. Himmelfahrt) 10.05.13: V/Ü
--- 17.05.13: V/Ü
23.05.13: V/Ü 25.05.13: V/Ü
30.05.13: --- (Fronleichnam) 31.05.13: ---
06.06.13: V/Ü 07.06.13: V/Ü
13.06.13: V/Ü 14.06.13: V/Ü
20.06.13: V/Ü 21.06.13: V/Ü
27.06.13: V/Ü 28.06.13: V/Ü
04.07.13: V/Ü 05.07.13: V/Ü
11.07.13: V/Ü 12.07.13: V/Ü
18.07.13: V/Ü 19.07.13: V/Ü

Materialien

Virtuelle Maschine mit vorinstallierten Verifikationswerkzeugen

VM Image, Dokumentation (für ein ähnliches System)

Einleitung

Verifikation funktionaler Eigenschaften imperativer und objekt-orientierter Programme: KeY-System

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.

Version 1.6 ist die zuletzt veröffentlichte Version und kann über die Dowloadseite des KeY-Projektes bezogen werden. Wenn Sie die Software Java Web Start installiert haben (auf fast allen modernen Systemen mit Java der Fall), können Sie KeY auch direkt aus dem Internetbrowser heraus starten, ohne etwas installieren zu müssen.

Bitte installieren Sie KeY auf Ihrem Rechner. Falls Sie nicht schon zuvor Erfahrung mit KeY gesammelt haben, 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.

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:

Hinweise:

  • Laden von Beispielen mit: isabelle jedit <dateiname.thy>

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. Alternativ ist UPPAAL in der virtuellen Maschine installiert.

Materialien


Link zur Webseite des vorigen Jahres