DAAD Austauschprogramm: PPP Spanien - Testfallgenerierung mit kooperierenden Constraint-Solvern

Grunddaten zu diesem Projekt

Beschreibung

Ziel ist die Entwicklung eines Werkzeugs zur automatischen Erzeugung von Testfällen für in der Programmiersprache Java geschriebene Programme, durch das der Kontroll- und/oder Datenfluss in einem System betrachteter Java-Klassen überdeckt wird und ggf. vorhandene Fehler aufgedeckt werden. Methodik:Statt der zur Ausführung von Java-Bytecode üblicherweise verwendeten Java Virtual Machine verwenden wir eine an der Uni Münster selbst entwickelte symbolische Java Virtual Machine (SJVM), bei der die Eingabeparameter einer Java-Methode als logische Variablen aufgefasst werden. Die SJVM ist an einen Constraint-Solver angeschlossen. Während der symbolischen Ausführung von Programmen ergeben sich an Verzweigungen möglicherweise zusätzliche Constraints, die an den Constraint-Solver zur Auswertung weitergeben werden. Widersprechen sich die angesammelten Constraints, wird Backtracking zur letzten alternativen Berechnung eingeleitet. Endet eine symbolische Berechnung erfolgreich, so lässt sich aus einer Lösung der Constraints ein Testfall generieren, der repräsentativ für alle Testfälle mit gleichem Berechnungsweg steht. Bei dem bisher verwendeten System von Constraint-Solvern fehlt ein geeigneter SAT-Solver modulo der hier benötigten Theorien. Bisher sind integriert: 1) ein gemischt-ganzzahliger Solver, der auf dem dualen Simplex-Verfahren und Branch & Bound basiert, 2) ein numerischer Solver für Polynomgleichungen, der von den Madrider Projektpartnern entwickelt wurde, sowie 3) ein Solver für lineare Ungleichungen. Bisher müssen die logischen Variablen in disjunkte Teilmengen zerlegt werden, von denen jede von genau einem Solver bearbeitet wird. Dies ist eine Einschränkung, die durch die geplanten Arbeiten aufgehoben werden soll. Hierbei sollen die in der Madrider Gruppe für die Zusammenarbeit von Solvern entwickelten Theorien für die betrachtete Problemstellung angewendet und konkretisiert werden.