Directed model checking with AI exploration algorithms
Final Report Abstract
Gerade in der Zeit von Multi-Core Rechnern wird die automatische Analyse von nebenläufiger Software zu einer Kernfragestellung der Informatik. Innerhalb des DFG-Projektes Gerichtete Modellprüfung wurden KI-Suchverfahren zur beschleunigten Fehlersuche innerhalb von parallelen Programmen eingesetzt. Die Idee dabei ist der schnellen Falsikation durch Studie der Fehlerbeschreibung selbst einen höhereren Stellenwert beigemessen als der vollständige Verikation. Durch das Projekt ist die gerichtete Modellprüfung als eine der wichtigsten Methoden zur Bewältigung des State Explosions Problems etabliert, das dadurch entsteht, dass der Raum der zu prüfenden Systemzustände üblicherweise exponentiell in der Anzahl der Variablen wächst. Fragestellungen, wie die effektive Nutzung der Festplatte bei begrenztem Speicher, sowie den Einsatz mehrerer Rechner zur Verikation wurden behandelt und fließen in die Entwicklung von universitärer Prototypen ein. Kann ein formales Modell des Programms extrahiert werden, bieten sich die entwickelten (sogenannter XXL-) Erweiterungen der Modellprüfer SPIN und UPAALL/CORA an. Das eigentliche Ziel, die Prüfung direkt auf den unabstrahierten Quelltext zu verwirklichen (damit werden Fehler bei der Modellierung vermieden), wurde durch die Simulation des Objektcodes in dem c/c++-Programmprüfer realisiert. Dabei werden dem Benutzer aufgespürte Fehler interaktiv in einer Benutzerschnittstelle (hier Eclipse) zur Verfügung gestellt.
Publications
- Large-scale directed model checking LTL. In SPIN, pages 1-18, 2006
S. Edelkamp and S. Jabbar
- Distributed verication of multi-threaded c++ programs. In Parallel and Distributed Methods in Verication (PDMC), pages 33-48, 2007
S. Edelkamp, S. Jabbar, and D. Sulewski
