Datenflussanalyse zum Nachweis der Fehlerfreiheit von Java Programmen

Programmweite Datenflussanalyse (Pointeranalyse) zum Nachweis der Freiheit von Laufzeitfehlern, wie z.B. Null-Pointer oder Class-Casts, ist immer noch wenig verbreitet. Derzeitige Anwendungen beschränken sich meist auf Informationen für Optimierungen in Compilern, wobei geringe Genauigkeit zwar zu weniger aggressiven Optimierungen führt, aber meist tolerierbar ist.

Bisherigen Analysemethoden fehlte entweder die Genauigkeit, um die vollständige Freiheit von bestimmten Laufzeitfehlern nachzuweisen, oder sie verursachten eine Explosion im Zeit- und Speicherbedarf bei der Analyse nicht trivialer Anwendungen. Zu geringe Genauigkeit führt zu vielen “false positives”, d.h., die Analyse kann für korrekten Code nicht automatisch nachweisen kann, dass kein Fehler auftreten kann, während eine Explosion im Analyseaufwand dazu führt, dass in vertretbarer Zeit gar keine Analyseergebnisse vorliegen.

In diesem Vortrag wird ein im EU Project HIJA (High Integrity Java) entwickeltes Verfahren zur programmweiten Datenflussanalyse präsentiert, das die Abwesenheit bestimmter Klassen von Java Laufzeitfehlern vollständig nachweisen kann. Solch eine Analyse reduziert den nötigen Debugging-Aufwand und verbessert die Code-Qualität im Allgemeinen. Darüber hinaus dient die durch die Analyse gewonnene Information als Grundlage für weitergehende Werkzeuge, etwa zur Bestimmung des nötigen Laufzeitspeichers oder der maximalen Ausführungszeit.