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 2011

Prof. Dr. Bernhard Beckert (BB)
Dr. Vladimir Klebanov (VK)

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 14.04.2011
LVNr.: 24625

Aktuelles

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.

Inhalt und Struktur der Vorlesung

Die Vorlesung ist anhand verschiedener Anwendungsszenarien mit unterschiedligen Eigenschaften und Anforderungen an formale Verifikationsmethoden organisiert. In sieben Einheiten werden diese Szenarien, typische Spezifikations- und Verifikationsmethoden und Werkzeuge vorgestellt:

Anwendungsszenario Methoden
1. Verifikation funktionaler Eigenschaften imperativer und objekt-orientierter Programme Java Modeling Language
Dynamische Logik		 (BB)
2. Nachweis temporallogische Eigenschaften endlicher Strukturen Model Checking (VK)
3. Verifikation nebenläufiger Programme (Concurrency) Rely/Guarantee (VK)
4. Hybride Systeme Model Checking, Dynamische Logik für hybride Systeme (BB)
5. Verifikation von Echtzeiteigenschaften Timed Automata, UPPAAL (BB)
6. Verifikation der Eigenschaften von Datenstrukturen Abstract Interpretation, TVLA (BB)
7. Programm-/Protokollverifikation Termersetzungsverfahren (Rewriting) (VK)
8. Information Flow

Die Veranstaltung hat 3 SWS, also 21 Doppelstunden im Semester. 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.

Terminplan

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

Donnerstag, 11:30-13:00, SR 236 Freitag, 11:30-13:00, SR 236
14.04.2011: V/Ü (1) 15.04.2011: ---
21.04.2011: V/Ü (1) 22.04.2011: --- (Karfreitag)
28.04.2011: V/Ü (1) 29.04.2011: V/Ü (1)
05.05.2011: V/Ü (2) 06.05.2011: V/Ü (2)
12.05.2011: V/Ü (2) 13.05.2011: V/Ü (2)
19.05.2011: V/Ü (5) 20.05.2011: V/Ü (5)
26.05.2011: V/Ü (5) 27.05.2011: ---
02.06.2011: --- (Chr. Himmelfahrt) 03.06.2011: ---
09.06.2011: V/Ü (4) 10.06.2011: V/Ü (7)
16.06.2011: V/Ü (7) 17.06.2011: V/Ü (7)
23.06.2011: --- (Fronleichnam) 24.06.2011: ---
30.06.2011: V/Ü (3) 01.07.2011: ---
07.07.2011: V/Ü (6) 08.07.2011: V/Ü (6)
14.07.2011: V/Ü (8) 15.07.2011: V/Ü (8)

Materialien

Vorlesungsfolien

Die Vorlesungsfolien werden hier jeweils nach der Vorlesung zur Verfügung gestellt.

0. Organisatorisches und Einführung

1. Funktionale Verifikation von Java-Programmen

Java Modeling Language

2. Model Checking mit SPIN

Einführung in Promela

SPIN-Grundlagen

Modellieren nebenläufiger Prozesse

Model Checking mit LTL

3. Verifikation nebenläufiger Programme mit Rely-Guarantee

Vortrag von Leonor Prensa Nieto (Autorin der Formalisierung von Rely-Guarantee in Isabelle)

4. Hybride Systeme

Folien aus dem Tutorial von Martin Fränzle, Universität Oldenburg

5. Verifikation von Echtzeiteigenschaften, UPPAAL

Folien aus dem Tutorial von Kim Larsen, Aalborg University

6. Abstrakte Interpretation, TVLA

Folien aus dem Tutorial von Patrick Cousot, ENS Paris

  • Foliensatz - Relevant: Folien 1-41, 59-66, 71-95

7. Modellierung/Verifikation in Rewriting Logic/Maude

8. Verifikation von Informationsflusseigenschaften

Verifikationswerkzeuge

Hier werden Informationen und Links zu den in der Vorlesung verwendeten Werkzeugen bereitgestellt.

1. KeY-System

Für die Vorlesungseinheit "Verifikation funktionaler Eigenschaften imperativer und objekt-orientierter Programme" verwenden wir das KeY-System. KeY wird am KIT und 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.4 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:
KeYIntro.pdf.

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

3. 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. Die Rely-Guarantee- (und die Owicki-Gries-) Theorie ist Teil der Isabelle-Distribution unter src/HOL/Hoare_Parallel. Einen Artikel zum Thema gibt es hier.

Um Isabelle/HOL mit der "Proof General"-Benutzeroberfläche zu nutzen, benötigt man noch zusätzlich GNU Emacs. Man ruft den Beweiser dann mit "ISABELLE_DIR/bin/isabelle emacs file.thy" auf.

4. HieroMate

Das Tool HieroMate ermöglicht die grafische Spezifikation von Hybriden Automaten, sowie eine Erreichbarkeitsanalyse mittels Model-Checking mit Hilfe eines Constraint Solvers und dem Tool Hytech.
HieroMate wird an der Universität Koblenz-Landau entwickelt von Christian Schwarz und Ammar Mohammed Ammar. Eine Beschreibung zu dem Tool befindet sich in HieroMate: A Graphical Tool for Specification and Verification of Hierarchical Hybrid Automata.

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

6. TVLA

TVLA ist ein Tool zur Erstellung von abstrakten Interpretern aus operationalen Semantiken. Mit Hilfe von TVLA können unter anderem Eigenschaften von Heap-allokierten Daten überprüft werden.

TVLA steht auf der Tool-Webseite zum Download zur Verfügung. Dieses Paket beinhaltet neben dem TVLA-Tool noch ein Manual sowie Beispiele. Außerdem befindet sich auf der Webseite ein Technischer Bericht zum dem Tool.

7. Maude

Maude ist ein Termersetzungssystem, ein Hochleistungsinterpreter für Spezifikationen in Rewriting Logic. Als Anwendung werden wir u.a. Verifikation mittels ausführbarer Java-Semantik JavaFAN behandeln. Die Maude-Webseite enthält das Manual (entspricht weitgehend dem Maude-Buch) und einen Primer (Einführung).


Link zur Webseite des vorigen Jahres

Bernhard Beckert