Diplomarbeiten zu vergeben!




Freie Themen und Themengebiete



Evaluierung der Praxistauglichkeit von Werkzeugen zur Software-Verifikation

In den letzten Jahren wurden verschiedene Werkzeuge zur formalen Verifikation von Software-Systemen entwickelt. Tools wie BLAST [1], MAGIC [2], SLAM [3] und viele weitere abstrahieren aus einem C-Programm automatisch ein Modell, über dem mittels Model Checking [4] Eigenschaften wie beispielsweise die Freiheit von Deadlock-Zuständen bewiesen werden können. Leider gibt es zu Software-Model-Checkern momentan weder vergleichende Fallstudien [5], die neben der Leistungsfähigkeit der verwendeten Technologie auch die Praxistauglichkeit der jeweiligen Werkzeuge untersuchen, noch existieren Metriken Für deren Evaluierung.

Eine Abschlußarbeit zu dieser Thematik kann einen großen praktischen Anteil, beispielsweise die Anwendung mehrerer Verifikationswerkzeuge zum Auffinden von Programmierfehlern im Quelltext von Open-Source-Programmen, haben. Der Absolvent sollte sich jedoch vorrangig mit der Frage auseinandersetzen, anhand welcher Kriterien die Praxistauglichkeit der Werkzeuge evaluiert werden kann. Die Arbeit wird ein umfangreiches Studium von Literatur aus dem Bereich des Software-Testing und der Software-Verifikation umfassen. Ihr theoretischer Anteil sollte daher nicht unterschätzt werden.

Literatur
[1]: http://embedded.eecs.berkeley.edu/blast/
[2]: http://www.cs.cmu.edu/~chaki/magic/
[3]: http://research.microsoft.com/slam/
[4]: Eine gute Einführung ist in Berard et al., "Systems and Software Verification", Springer-Verlag, 2001 zu finden.
[5]: Eine Fallstudie zu BLAST ist unter http://www-users.cs.york.ac.uk/~muehlber/blast/ hinterlegt. Der Arbeit ist zu entnehmen, daß das Tool nur begrenzt zum automatischen Auffinden von Fehlern in "realem" Programm- Code geeignet ist.



Objekt-Code-Slicing zur Verifikation von Pointer-Programmen

Während heutige Werkzeuge zur Software-Verifikation [1] zumindest theoretisch Probleme wie Deadlock-Zustände aufdecken können, ignorieren selbst kommerzielle Tools wie SLAM [2] nahezu alle Pointer-Operationen in einem zu analysierenden Programm. Jedoch zeigen beispielsweise Chou et al. in [3], daß ein Großteil der in Programmen vorhandenen Fehler auf die inkorrekte Benutzung von Pointern zurückzuführen ist. Um diesbezügliche Defizite in quelltextbasierten Verifikationsverfahren zu bewältigen, wird im Rahmen eines Forschungsprojektes an der University of York an Verfahren und Tools [4] gearbeitet, die Objekt-Code- Programme statisch analysieren und zur Validierung bzw. Verifikation aufbereiten. Hierbei kommt vor allem das sogenannte Programm-Slicing [5,6] zum Einsatz.

Eine der Herausforderungen unseres Forschungsvorhabens besteht darin, Slicing-Techniken auf Objekt-Code-Programme anzuwenden. Kompilierte Programme vereinfachen nämlich auf der einen Seite die Untersuchung von Pointer-Operationen dadurch, daß sie explizite Adressen und Instruktionen mit einer definierten Semantik benutzen. Auf der anderen Seite erschweren die verschiedenen Adressierungsmodi und die enorme Anzahl der Instruktionen moderner Prozessoren die Extraktion der für die Analyse von Memory-Safety-Eigenschaften relevanten Programmteile.

Momentan gibt es in unserem Forschungsprojekt Themen für Abschlußarbeiten, die sowohl einen praktischen als auch einen theoretischen Schwerpunkt haben können. Denkbar sind beispielsweise die Implementierung von Abstraktionsalgorithmen für die IA64 Architektur oder die Entwicklung von Optimierungs- und Analyseverfahren für die von uns genutzten Zwischenrepräsentationen.

Literatur
[1]: Eine gute Einführung ist in Berard et al., "Systems and Software Verification", Springer-Verlag, 2001 zu finden.
[2]: http://research.microsoft.com/slam/
[3]: Chou et al., "An empirical study of operating system errors", SOSP 2001, ACM Press
[4]: Publikation und Web-Seite hierzu gibt's in ein oder zwei Monaten.
[5]: Weiser, "Program Slicing", ICSE 1981, IEEE Press
[6]: Tip, "A Survey of Program Slicing Techniques", http://www.research.ibm.com/people/t/tip/papers/jpl1995.pdf






Impressum
Jan Tobias Mühlberg, 1.1, Tue, 23 Feb 2010 15:16:43 +0000