Produkt-Programme in Java für effiziente relationale Verifikation

Typ:	BA
Datum:	2017-09-15
Betreuer:	Michael Kirsten Mattias Ulbrich
Aushang:

Ziel

Die Verifikation wichtiger Eigenschaften von Programmen kann sehr aufwändig sein. Insbesondere ist das der Fall, wenn diese Eigenschaften mehr als nur einen Programmlauf behandeln, da hier im Allgemeinen jeder Lauf separat verifiziert werden muss.

Ein wichtiges Beispiel ist das Beweisen der Abwesenheit unerwünschter Informationsflüsse. Hier wird verifiziert, dass sich das Programm gleich verhält, wenn sich die geheimen Informationen geändert haben, also eine Aussage über zwei Programmläufe. Andere Beispiele sind Fairnesseigenschaften für Wahlverfahren, z. B. dass eine Stimme mehr dem entsprechenden Kandidaten keine Wahlniederlage bescheren kann. Häufig möchte man auch einfach beweisen, dass sich in die neue Software-Version keine Fehler eingeschlichen haben.

Hierfür gibt es bereits eine effiziente Technik, das sogenannte Verweben zu einem Produktprogramm, bei der man sich die Ähnlichkeit beider Programmläufe zunutze macht. Mit dieser Technik lassen sich solche Beweise erheblich vereinfachen. Vor Kurzem wurde innerhalb eines Studierendenprojekts ein Prototyp entwickelt, der dies für Javaprogramme automatisiert.

In dieser Bachelorarbeit soll es nun darum gehen, diese Technik zu erweitern und sie auf interessante Fallstudien (bspw. Wahlverfahren, Informationsflüsse oder Softwareregression) anzuwenden. Auch im Bereich der Fallstudien existieren bereits einige Vorarbeiten am Institut, sodass eine breite Auswahlmöglichkeit besteht.

Voraussetzungen

• Erfahrung im Programmieren mit Java
• Kenntnisse, wie sie in der Vorlesung Formale Systeme vermittelt werden, sind hilfreich

Betreuung und Kontakt

• Dr. Mattias Ulbrich (Raum 229, Geb. 50.34)
• Michael Kirsten (Raum 228, Geb. 50.34)