Praxis der Softwareentwicklung (PSE)

Hintergrund

Eines der Hauptforschungsthemen an unserem Lehrstuhl ist die Verifikation relationaler Eigenschaften von Programmen. Relationale Eigenschaften sind solche Eigenschaften, die sich auf mindestens zwei Programmausführungen beziehen. Ein Beispiel dafür ist die Programmäquivalenz: Liefern zwei Programme bei gleicher Eingabe immer die gleiche Ausgabe? Ein anderes wichtiges Beispiel für relationale Eigenschaften stellen Informationsflusseigenschaften dar: Haben gewisse Eingaben Einfluss auf gewisse Ausgaben? Eine besondere Rolle spielt hier die Nichtinterferenz-Eigenschaft (engl. noninterference). Diese besagt, dass als geheim eingestufte Eingaben (z. B. ein Passwort) keine öffentlichen Ausgaben beeinflussen können. Für den Nachweis solcher Informationsflusseigenschaften wird eine Technik namens Selbstkomposition verwendet, wobei zwei Ausführungen desselben Programms mit verschiedenen geheimen Eingaben miteinander verglichen werden.

Aufgabenbeschreibung

Unser Lehrstuhl hat bereits verschiedene Ansätze entwickelt und Tools (z. B. llrêve, llrêve for noninterference oder KeY) implementiert, um relationale Eigenschaften formal beweisen zu können. Da es sich hierbei allerdings um ein unentscheidbares Problem handelt und folglich ein Beweis nicht immer gelingen kann, möchten wir im Rahmen dieses PSE-Projekts ein Werkzeug entwickeln, das dem Benutzer die Möglichkeit gibt, mehrere Programausführungen interaktiv zu analysieren und zu vergleichen. Hierzu soll ein sogenannter relationaler Debugger entwickelt werden, der im Unterschied zu einem herkömmlichen Debugger mehrere Programmläufe nebeneinanderlegen und vergleichen kann.

Anforderungen

Das zu entwickelnde Tool soll das gleichzeitige Debuggen von mindestens zwei Programmausführungen erlauben. Übliche Debugger-Konzepte (break-points, stepping, etc.) sollen auf die relationale Ebene übertragen werden. Die Zielsprache soll eine vereinfachte While-Sprache (z. B. eine sinnvolle Teilmenge von Java) sein. Der Debugger soll über eine benutzerfreundliche graphische Oberfläche verfügen, die die Analyse zweier Programmläufe ermöglicht. Die Implementierung soll in der Programmiersprache Java erfolgen.