Home | english  | Impressum | Sitemap | KIT

Formale Software-Entwicklung (SS 08)

Formale Software-Entwicklung (SS 08)
Typ: Seminar
Zeit:

Blockveranstaltung am Semesterende

Beginn: 23.04.2008
Dozent:

Prof. P. H. Schmitt
Christian Engel
Mattias Ulbrich
Benjamin Weiß

SWS: 2

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.

Seminarvorträge am 8./9. Juli 2008

Uhrzeit   Vortrag Ort
Dienstag, 08. Juli 2008
09:45   [Sem:FSE] Philipp Glaser: Daikon   SR 131
10:45   [Sem:FSE] Saoussen Arfaoui: Non-null Types in an Object-Oriented Language   SR 131
11:45-12:45   [Sem:FSE] Sebastian Maisch: Perc Pico   SR 131
14:00   [Sem:FSE] Michael Ziller: Pex (Program EXploration)   SR 131
15:00   [Sem:FSE] Simon Roth: Compilerverifikation   SR 131
16:00   [Sem:FSE] Martin Küster: Towards Verified Model Transformations   SR 131
Mittwoch, 09. Juli 2008
09:45   [Sem:FSE] Daniel Bruns: Interactive Verification of Statecharts   SR -109
10:45   [Sem:FSE] Rolf Haynberg: Model Checking Dynamic and Hierarchical UML State Machines   SR -109
11:45-12:45   [Sem:FMSens] J.P. Tsague: Automated Test Generation using the Simbolic Analysis Laboratory (SAL)   SR -109
14:00   [Sem:SAT] Markus Iser: Visualisierung der Struktur von SAT-Instanzen mittels Graph-Layout   SR -109
14:50   [Sem:SAT] Simon Roth: Software Verifikation: Abstraction Refinement   SR -109
15:40       [Sem:SAT] Jan Rochel: Tree Decomposition für SAT   SR -109

Organisatorisches

  • 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

Hinweise für gute Seminarvorträge

Vortragsthemen

  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.