Verification-based Test Generation

Typ:	BA / SA / MA / DA
Datum:
Betreuer:	Christoph Gladisch
Aushang:

Kontext

Formale Verifikationswerkzeuge sind Hightech-Software. Mit einem solchen Verifikationswerkzeug kann man die Korrektheit eines Programms bezüglich einer Anforderungsspezifikation mathematisch beweisen. Ein solcher Beweis ist für alle Ein- und Ausgabesituationen gültig. Bekanntlich sind mathematische Beweise jedoch aufwendig. Der bisher verbreitetere Ansatz, um die Qualität von Software sicherzustellen, ist daher das Testen von Programmen. Programmtests können schnell und einfach durchgeführt werden. Des Weiteren sind Tests ein wichtiges Mittel um den Softwareverifikationsprozess zu unterstützen.

Aufgabenstellung

In dieser Arbeit erweitern Sie das Softwareverifikationswerkzeug KeY mit neuen Komponenten zur Generierung von Java-Unittests. Das KeY-Tool wird seit rund 10 Jahren am KIT und an anderen Universitäten entwickelt. Komponenten zur Testgenerierung existieren bereits in einer früheren Version des KeY-Tools. Da sich das KeY-Tool nun in einer neuen Generation befindet, soll auch die Testgenerierung neu entwickelt werden. Die Schwerpunkte bei dieser Arbeit liegen auf Implementierung. In einer Studien- oder Bachelorarbeit wird eine einfachere Variante der Testgenerierung entwickelt als in einer Diplom- oder Masterarbeit.

Voraussetzungen

• Gute Kenntnisse in Java-Programmierung und in Logik (z. B. Vorlesung „Formale Systeme“)
• Interesse an Forschung