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

Bemerkung: Der Inhalt der Vorlesung Formale Systeme wird als bekannt vorausgesetzt.

• Vorbereitungstermin am Di, 20.05.2008, 11:30-13:00 in SR 131
  • jeder Teilnehmer stellt in ca. 5 min die Gliederung seines Vortrags vor
  • dazu höchstens 5 Folien
• Abgabe der Ausarbeitung bis Di, 24.06.2008
  • 5-10 Seiten
  • mit LaTeX erstellt
• Vorträge am Di, 08.07.2008 (ganztags) und Mi, 09.07.2008 (vormittags)
  • jeweils ca. 45 min + 15 min Diskussion

• A. Zeller: Der perfekte Seminarvortrag
• F. Mattern: Seminarvortrag - Hinweise zur Präsentation
  

1. Compilerverifikation
   Ziel dieses Vortrags ist es, dem Auditorium eine Anwendung des Programmverifikationssystems KeY auf dem Gebiet der Compilerverifikation zu präsentieren. Als Quelle dient diese Diplomarbeit, wobei auf dieses Papier als Hintergrundinformation zurückgegriffen werden kann. Insbesondere soll klargestellt werden:
   (1) der kleine Ausschnitt der Verifikation eines Compilers, der in diesem DA Projekt angesprochen wird (Codegenerierung ohne Optimierung von der RTL-Zwischensprache in Pentium Maschinensprache)
   (2) die benutzte Verifikationsmethodologie (translation validation)
   (3) die formale Semantikbeschreibung von RTL und Maschinensprache mit ASM
   (4) die Formulierung der Verifikationsaufgabe als Java Programmverifikation, d.h. die Umsetzung von ASM udates in Java Programme und die Formalisierung der Beweisverpflichtungen mit JML
   (5) Grenzen des bisher erreichten (dynamisches Abbildung der RTL Pseudoregister auf Pentium Register)
2. Bogor
   Bogor ist ein Software Model Checking Framework für Java. Außerdem sind in Bogor Techniken zur automatischen Testfallerzeugung und symbolischen Ausführung von Java-Programmen realisiert.
   Dieses Papier vermittelt einen ersten Überblick über Bogor. Weitere Informationen gibt es hier.
3. Daikon
   Daikon ist ein Werkzeug zum automatischen Finden von Invarianten, d.h. Eigenschaften, die bei jeder Programmausführung an einem bestimmten Programmpunkt gelten. Eine Einführung in Daikon gibt dieses Papier. Weitere Veröffentlichungen, Dokumentation und das Werkzeug zum Herunterladen finden sich auf der Daikon-Webseite.
4. Java Applet Correctness Kit (JACK)
   JACK ist ein Werkzeug zur formalen Verifikation von Java-Programmen, das besonderen Wert auf einfache Benutzbarkeit legt. Einen Überblick enthält dieses Papier. Auf der JACK-Homepage gibt es weitergehende Informationen und das Werkzeug zum Herunterladen.
5. Java PathFinder
   Java PathFinder ist ein Software Model Checker für Java. Dieses Papier bietet neben der offiziellen Homepage des Projekts einen guten Überblick über Java PathFinder.
6. Non-null Types in an Object-Oriented Language
   Das Dereferenzieren von "null" ist eine der größten Fehlerquellen in objektorientierten Programmen. Dieses Papier schlägt einen typbasierter Ansatz vor, um dieses Problem in den Griff zu bekommen. Eine konkrete Implementierung des Ansatzes für Java wird hier beschrieben.
7. Perc Pico
   Perc Pico ist ein Java-Compiler für Echtzeitanwendungen. Eine Besonderheit von Perc Pico ist, daß er Java-Code nicht wie sonst üblich in Bytecode sondern, mit dem Umweg über C-Code, in Maschinencode übersetzt. Der so erzeugte Code allokiert keine Objekte auf dem Heap, sondern ausschließlich auf dem Stack. Da dadurch der Garbage Collector, der normalerweise in Java nicht länger benötigte Heapobjekte wiederverwertet, überflüßig wird, wird das Laufzeitverhalten einer mit Perc Pico kompilierten Applikation deterministischer und damit geeigneter für Echtzeitsysteme. Der Preis den man dafür allerdings zahlen muß ist, daß es zu sogenannten "dangling references", Referenzen auf nicht mehr existierende Objekte, kommen kann, die zur Laufzeit unter Umständen zu Exceptions führen. Damit das nicht passiert, müssen Perc Pico-Programme mit Annotationen versehen werden, die mit Hilfe von statischen Analysetechniken überprüft werden können oder dem Compiler als Hinweis dienen, in welchem Speicherbereich bestimmte Objekte allokiert werden müssen.
   Nähere Informationen zu den von Perc Pico verwendeten Annotationen finden sich hier, sowie weiteres Material auf dieser Seite.
8. Pex (Program EXploration)
   Pex ist ein White Box Testgenerierungswerkzeug für .NET. In diesem Papier werden die Pex zugrundeliegenden Konzepte (parametrisierte Unit-Tests, symbolische Ausführung) beschrieben. Weiteres Material: Homepage des Projekts bei Microsoft Research, Pex Tutorial.
9. Towards Verified Model Transformations
   Modellgetriebener Softwareentwurf wird als eine zukunftsträchtige Methode zur Verbesserung des Entwurfsprozesses angesehen. Um auch für sicherheitskritische Anwendungen eingesetzt zu werden, müssen die angewandten Modeltransformationen auch verifiziert werden können. Dieses Papier, zusammen mit einer Diplomarbeit, beschreibt dazu, wie für eine gegebene Modelltransformation sichergestellt werden kann, dass diese die Semantik des Modells erhält.
   Dazu werden FUJABA und Isabelle/HOL verwendet.
10. Interactive Verification of Statecharts
    Dieses Papier stellt einen Ansatz vor, um in einem interaktiven Beweiser (KIV) dynamische Modelle (Statecharts) mit Hilfe von dynamischer Logik, symbolischer Ausführung und Intervalllogik zu verifizieren.
11. Model Checking Dynamic and Hierarchical UML State Machines
    Neben deduktiven Methoden zur Verifizierung von dynamischen Modellen bietet sich auch Model Chcking als eine Alternative an. Dieses Papier beschreibt eine Umsetzung von UML Statemachines auf die Eingabesprache Promela des populären Model Checkers SPIN.