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.

• Anmeldung bei Frau Beckert in Raum 321
• Vorbesprechung am Mi, 29.04.2009, 13:00-14:00 in SR 301
• Vorbereitungstermin am Mi, 27.05.2009, 11:30-12:00
  • jeder Teilnehmer stellt in ca. 5 min die Gliederung seines Vortrags vor
  • dazu höchstens 5 Folien
• Abgabe der Ausarbeitung und der Folien bis Mi, 24.06.2009. Für die Ausarbeitung gilt:
  • 5-10 Seiten
  • mit LaTeX und der verbindlichen IEEE Formatvorlage erstellt
• Vorträge am Mi, 08.07.2009, 9:45-13:45 in SR -109
  • jeweils ca. 45 min + 10 min Diskussion

1. Bogor/Kiasan
   Bogor/Kiasan setzt symbolische Ausführung ein, um die Korrektheit von Java-Programmen zu überprüfen. Dieses Papier vermittelt einen ersten Überblick über Bogor/Kiasan. Weitere Informationen gibt es hier.
2. ScopeJ
   Die "Real-Time Specification for Java" sieht ein Speichermodell mit expliziter Speicherverwaltung vor, bei dem komplette, zuvor definierte, Speicherbereiche vom Programmierer freigegeben werden können. Damit es dabei nicht zu sogenannten hängenden Referenzen (d.h. Referenzen in einen nicht mehr existierenden Speicherbereich hinein) kommt, werden zur Laufzeit Überprüfungen vorgenommen, die das Entstehen solcher Referenzen verhindern (gegebenenfalls durch Werfen einer Exception). ScopeJ definiert ein Typsystem, das solche hängenden Referenzen verhindert und so derartige Überprüfungen zur Laufzeit überflüssig macht.
3. 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.
4. Modellierung eines Dateisystems mit Event-B
   Zur besseren Vergleichbarkeit und als Herausforderungen werden immer wieder Fallstudien vorgeschlagen, mit denen sich formale Werkzeuge beschäftigen sollen. Die formale Spezifizierung eines Dateisystems - vorgeschlagen von Seiten der NASA - ist eine solche Fallstudie. In diesem Papier wird berichtet, wie man mit Hilfe der Formalen Methode Event-B Aspekte eines Dateisystems modellieren kann und dieses Modell über mehrere Schritte verfeinert.
5. ProB: An Automated Analysis Toolset for the B Method
   Normalerweise werden deductive Verfahren eingesetzt, um Korrektheit von Spezifikationen in abstrakteren Formalismen zu beweisen. Daneben gibt es aber auch Tools wie den Model Checker ProB, der nicht deduktiv arbeitet. Die Autoren dieses Papiers begründen, dass ProB eingesetzt werden kann, um frühzeitig Fehler in Spezifikationen zu entdecken, und im Falle eines Fehlers auch, um Gegenbeispiele zu konstruieren.
6. Atelier B
   Die B-Methode ist eine etablierte Methode zur formalen Spezifikation von Systemen, die in einigen namhafte Firmen regelmäßig in realen, großen Projekten zur Anwendung kommt. Die professionelle Werkzeugsammlung Atelier B für die B Methode steht seit Oktober 2008 jetzt erstmals in einer frei erhältlichen Version zur Verfügung. Aufgabe dieses Vortrages ist es, den typischen B-Entwurfsprozess in Atelier-B anhand eines Beispieles von der abstrakten Spezifikation, über die konkrete Spezifikation bis hin zum generierten Code zu erläutern. Die meiste Dokumentation über das System liegt auf Englisch vor. Da die Software von einer französischen Firma entwickelt wird, sind für die Recherche aber elementare Französischkenntnisse hilfreich, wenngleich nicht notwenig.
7. Datengruppen
   Beim Spezifizieren objektorientierter Programme werden Methoden typischerweise mit Vor- und Nachbedingungen versehen. Zusätzlich wird eine sogenannte "Modifies-Klausel" angegeben, die festlegt, welchen Teil des Programmzustands die Methode höchstens verändern darf. Problematisch in Bezug auf diese Modifies-Klauseln sind Methoden in Oberklassen, die später in Unterklassen überschrieben werden sollen: Beim Schreiben der Spezifikation in der Oberklasse sind die konkreten Speicherstellen, die sich in der Unterklasse ändern dürfen, noch unbekannt. Datengruppen sind ein Ansatz zur Lösung dieses Problems. Eine Umsetzung von Datengruppen für Java ist Teil der Java Modeling Language (JML).
8. Dafny
   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. Dieses Vorlesungsskript beschreibt Dafny und die Verifikation von Dafny-Programmen.
9. Universe Types
   Es ist typisch für objektorientierte Programmen, dass es in einem Programmzustand gleichzeitig mehrere Referenzen auf ein Objekt geben kann ("Aliasing"). Unkontrolliertes Aliasing kann aber zu verschiedenen Problemen führen. Beispielsweise verwendet häufig die Implementierung eines Objektes intern andere ("Hilfs"-)Objekte. Es ist dann oft nicht wünschenswert, dass Referenzen auf diese Hilfsobjekte in der "Außenwelt" bekannt sind, da sie benutzt werden könnten, um die Schnittstelle des "umschließenden" Objektes zu umgehen und die Hilfsobjekte direkt zu manipulieren. Ein Ansatz zur Lösung dieses Problem ist es, eine "Ownership"-Beziehung auf Objekten einzuführen, und es Objekten zu verbieten, Referenzen auf Objekte im "Besitz" eines anderen Objekts zu halten. Zur Spezifikation und Verifikation solcher Kapselungseigenschaften werden meistens Typsysteme verwendet. Universe Types sind das zur Zeit wohl bekannteste solche Typsystem. Eine Umsetzung von Universe Types für Java wird hier beschrieben.
10. FindBugs
    FindBugs ist ein Werkzeug, das Java-Programme nach möglichen Fehlern durchsucht. Zu diesem Zweck verwendet FindBugs eine Bibliothek sogenannter "bug patterns", also Code-Muster, die mit einiger Wahrscheinlichkeit auf einen Bug hindeuten. Ein besonders häufiges Fehlersymptom sind Dereferenzierungen von "null". Die von FindBugs benutzte Analyse zum Erkennen solcher Fehler wird hier ausführlicher beschrieben.
11. Vergleich von objekt-orientierem und funktionalem Programmieren
    Wenn auch die Vormachtstellung objekt-orientierter Programmiersprachen zur Zeit ungebrochen erscheint, gibt es doch ernsthafte Überlegungen, ob nicht auch andere Paradigmen mehr Beachtung finden sollten. In diesem Seminarvortrag soll das Papier "Mapping and Visiting in Functional and Object-Oriented Programming", vorgestellt werden. Es vergleicht anhand des "visitor patterns" objekt-orientierte und funktionale Programmierung. Als Schlußfolgerung wird eine Verallgemeinerung dieses Musters vorgeschlagen, das in einer Programmiersprache realisiert werden kann, die sowohl Objektorientierung als auch funktionale Programmierung unterstützt.
12. Einführung in die Typentheorie
    Chapter 9 Simply Typed Lambda-Calculus und Chapter 12 Normalization aus dem Buch:
    Types and Programming Languages
    Benjamin C. Pierce
    The MIT Press
    InfoBib Signatur: E.Pie(38492)

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