Formale Programmentwicklung (SoSe 2010)
Typ: | Seminar | ||
---|---|---|---|
Semester: | Sommersemester 2010 | ||
Ort: | n.V. |
||
Zeit: | Vorbesprechung am Mi, 21.04.2010, 13:00-14:00 in SR 301 Blockveranstaltung am Semesterende |
||
Dozierende: |
Professor Bernhard Beckert Professor Peter H. Schmitt Thorsten Bormer Daniel Bruns Christian Engel David Faragó Dr. Vladimir Klebanov Mattias Ulbrich Benjamin Weiß |
||
SWS: | 2 | ||
LVNr.: | 24821 |
Thema
Software-basierte Systeme sind aus unserem Alltag nicht mehr wegzudenken.
Sie halten Einzug in nahezu alle Bereiche unseres Lebens.
Allerdings bleibt die Qualität der Software trotz ihrer wachsenden Bedeutung
nur allzuoft auf der Strecke. In manchen Bereichen mag dies tolerierbar sein,
sobald aber durch fehlerhafte Software Menschenleben gefährdet sind
(z.. B. Eisenbahnwesen oder Anwendungen in der Medizin) oder hohe finanzielle
Schäden zu befürchten sind (z.. B. Internet-Banking), muss auf die
Qualität - insbesondere auf die Korrektheit - der Software besonderer Wert
gelegt werden.
In diesem Seminar werden (formale) Methoden behandelt, deren Anwendung es
tatsächlich ermöglicht, fehlerfreie Software zu entwickeln
oder zumindest die Qualität der Software deutlich zu erhöhen.
Organisatorisches
- Anmeldung bei Frau Beckert in Raum 321
- Vorbesprechung am Mi, 21.04.2010, 13:00-14:00 in SR 301
- Vorbereitungstermin am Mo, 17.05.2010, 14:00-15:30 in SR -109
- jeder Teilnehmer stellt in ca. 5 min die Gliederung seines Vortrags vor
- dazu höchstens 5 Folien
- Für die Ausarbeitung gilt:
- 5-10 Seiten
- mit LaTeX und der verbindlichen IEEE Formatvorlage erstellt
- Vorträge am Mo, 05.07.2010, 09:45-12:30 in SR -107
- jeweils ca. 45 min + 10 min Diskussion
Vortragsthemen
-
Dafny
[Dokument 1,
Dokument 2]
Dafny ist eine experimentelle objektorientierte Programmiersprache von Microsoft Research. Dafny-Programme können in Dafny selbst spezifiziert und mit einem mitgelieferten Werkzeug verifiziert werden. Die Sprache bietet dafür u.a. die Möglichkeit, Vor- und Nachbedingungen von Methoden anzugeben, und mit Hilfe von "Modifies"- und "Reads"-Klauseln festzulegen, welche Speicherstellen eine Methode höchstens schreiben bzw. lesen darf. Die Neuigkeit gegenüber anderen Sprachen liegt dabei in der Art und Weise, wie solche Modifies- und Reads-Klauseln formuliert werden. Der Ansatz von Dafny basiert auf den sogenannten "Dynamic Frames", die eine größere Flexibilität bieten als frühere Ansätze wie z.. B. "Datengruppen". - Informationsflussanalyse mit Theorembeweisern Die meisten Ansätze zur statischen Analyse von sicherem Informationsfluss basieren auf einem speziellen Typsystem oder einer speziellen Datenflussanalyse. Diese Ansätze sind vollautomatisch, aber es gibt dabei immer Programme, die als "falsch" eingeordnet werden, obwohl sie in Wahrheit keinen unsicheren Informationfluss enthalten. In diesem Seminarthema soll ein von Darvas, Hähnle und Sands vorgeschlagener Ansatz vorgestellt werden, der diesen Nachteil nicht hat: Hier können alle korrekten Programme auch als korrekt klassifiert werden, wenn auch nicht immer automatisch. Die Grundidee des Ansatzes ist es, Informationflusseigenschaften in einer allgemeinen Programmlogik zu formalisieren und mit einem entsprechenden Theorembeweiser (KeY) zu beweisen.
- Termersetzung und sicherer Informationsfluss Kontrollierter Fluss sensibler Informationen ist eine wichtige Sicherheitsanforderung für Software. Neuerdings kann man Informationsfluss in Java-Programmen mittels moderner Termersetzungsmaschinen wie z.. B. Maude modellieren und analysieren. Das Thema beinhaltet eine allgemeine Einarbeitung in Maude und Rewriting-Logik, sowie konkret in die Informationsflussanalyse anhand dieses Papiers.
- Temporallogische Spezifikation Beim Spezifizieren von Programmen werden Methoden typischerweise mit Vor- und Nachbedingungen versehen. Dies erlaubt jedoch nicht temporale Aussagen wie "Methode x wird irgendwann in der Zukunft aufgerufen", die eventuell für die Verifikation von Sicherheitseigenschaften benötigt werden. Die AutorInnen dieses Papiers* stellen eine temporallogische Erweiterung der Java Modeling Language (JML) vor.
- Separation Logic in der Praxis Dieses Papier beschreibt die Verwendung eines SMT-Beweisers in der Verifikation von Programmen einer C-aehnlichen Sprache, deren Methodenkontrakte mit Hilfe von separation logic spezifiziert sind.
- Beweisverwaltung Im Laufe einer formalen Programmentwicklung verändert sich neben der Software auch die Spezifikation und eventuelle Beweise. Heutige, zeilenbasierte Versionskontrolle wie CVS hat sich als ungeeignet erwiesen, komplexe Datenstrukturen wie Beweise und deren Semantik zu verwalten. Ein Ansatz ist das auf sog. Entwicklungsgraphen basierende MAYA-System.
- Einführung in Spec Explorer Spec Explorer ist eines der bekanntesten und mächtigsten Werkzeuge für modellbasiertes Testen und eine Erweiterung von Microsoft (MS) Visual Studio. Es wurde ursprünglich von MS Research entwickelt, ist mittlerweile aber bei MS DevLabs und im industriellen Einsatz. Die Spezifikationen sind auf abstrakter Ebene in Spec# oder AsmL geschrieben. Testfälle werden mit einem explicit-state Model Checker erzeugt. "Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer" ist eine allgemeine Einführung und das Papier, über das referiert werden soll. Das Buch "Model-Based Software Testing and Analysis with C#" ist ein ausführliches Nachschlagewerk.
- Fallstudie mit CADP CADP (Construction and Analysis of Distributed Processes) ist eine Werkzeugsammlung für den Entwurf und die Analyse von Kommunikations-protokollen und verteilten Systemen. Sie wird sowohl akademischen als auch industriell eingesetzt. In der Fallstudie wird ein SIP registrar auf abstrakter Ebene in LOTOS (Language of Temporal Ordering Specification) spezifiziert. Danach werden mit TGV (Test Generation from transitions systems using Verification techniques) und Überdeckungskriterien bzw. Mutationen Testfälle generiert.
- Verifikation eines Microkernels: L4.verified Im Projekt "L4.verified" wird die Korrektheit der Implementation eines L4-basierten Microkernels formal bewiesen. Einen Überblick gibt die Website des Projekts, sowie diese Publikation. Einen Vergleich mit aehnlichen Projekten findet sich in diesem Papier.
- Übersetzung von Java in die Verifikationssprache BoogiePL Die Verifikation von Software findet nicht immer auf der Ebene des Quelltextes statt. Häufig wird dieser zunächst auf eine für die Verifikation besser geeignete Zwischensprache abgebildet, auf der diese dann erfolgt. Dieses Papier beschreibt, wie ausgehend von Java Byte Code eine Übersetzung in die Zwischensprache BoogiePL erfolgen kann.
-
Moderne Entwicklungen in der Verifikation nebenläufiger Programme
[Dokument 1,
Dokument 2]
Entwicklung korrekter nebenläufiger Programme ist eine besonders schwere Herausforderung. Eine klassische Methode zu diesem Zweck ist deduktive Verifikation mittels Rely-Guarantee-Technik. Obwohl Rely-Guarantee seit den 80er Jahren bekannt ist, gab es in letzter Zeit eine Reihe interessanter Weiterentwicklungen. Einige wenige sollen hier erörtert werden. - Verifikation von nebenläufigen Programmen mit Chalice Die Verifikation von mehrfädigen Programmen stellt eine besondere Herausforderung dar, wenn Speicher auf beliebige Weise gemeinsam genutzt werden soll. Die zu Forschungszwecken entworfene Sprache Chalice, die in diesem Artikel vorgestellt wird, verfolgt den Ansatz, mittels spezieller Kommunikation zwischen den Prozessen (Erlaubnis-Transfer, Kanäle, Locks, ...), dieser Aufgabe habhaft zu werden.
* Dokumente von springerlink.com sind von innerhalb des KIT-Netzwerkes erreichbar.