Mit formaler Verifikation gegen Laufzeitfehler

Anbieter zum Thema

MicroConsult Academy GmbH

MES Electronic Connect GmbH & Co. KG

Cadlog Group

The MathWorks GmbH

Die abstrakte Interpretation lässt sich am besten anhand eines einfachen Beispiels erklären. Angenommen, es sollen drei große Ganzzahlen multipliziert werden: -4586 × 34985 × 2389 = ?

Die Rechnung lässt sich per Hand nur schwer schnell lösen. Abstrahiert man aber das Rechenergebnis auf sein Vorzeichen, erkennt man unmittelbar, dass dieses am Ende negativ sein muss. Eine solche Vorzeichenermittlung ist eine praktische Anwendung der abstrakten Interpretation. Mit dieser Methode kann man einige Eigenschaften des Endergebnisses, wie hier das Vorzeichen, von vornherein wissen, ohne die Ganzzahlen komplett miteinander multiplizieren zu müssen.

Betrachten wir nun eine vereinfachte Anwendung der formalen Mathematik der abstrakten Interpretation auf Software-Programme. Die Semantik einer Programmiersprache ist in der konkreten Domäne S dargestellt. Es sei nun A die Abstraktion dieser Semantik, wobei die Abstraktionsfunktion α die konkrete Domäne S auf die abstrakte Domäne A abbildet. Bestimmte Eigenschaftsbeweise der Software können nun in der abstrakten Domäne A durchgeführt werden, was sich einfacher gestaltet als in der konkreten Domäne S.

Die Abwesenheit von Laufzeitfehlern im Quellcode beweisen

Die Ergebnisse einer abstrakten Interpretation gelten als korrekt, weil sich durch strukturelle Induktion mathematisch beweisen lässt, dass die Abstraktion das richtige Ergebnis vorhersagt. Wendet man die abstrakte Interpretation auf Software-Programme an, dann kann sie dazu eingesetzt werden, bestimmte Eigenschaften der Software zu beweisen, darunter zum Beispiel, dass diese Software frei von bestimmten Typen von Laufzeitfehlern ist. In der Praxis wird für die abstrakte Interpretation mit Hilfe der Abstraktionsfunktion α eine angenäherte Semantik des Software-Codes berechnet, so dass diese in der abstrakten Domäne verifiziert werden kann.

Dabei werden Gleichungen oder Bedingungen erzeugt, deren Lösung eine Computerdarstellung der abstrakten Semantik des Programms darstellt. Werte von Variablen werden mit Hilfe von Graphen (engl. lattices) dargestellt. Für das zuvor beschriebene Vorzeichenbeispiel kann man mit dem in Bild 1 gezeigten Graphen die Fortpflanzung abstrakter Werte in einem Programm verfolgen (von unten nach oben). Das Erreichen jedes einzelnen Knotens bedeutet den Beweis einer bestimmten Eigenschaft.

Erreicht man die Spitze des Graphen, dann bedeutet das, dass eine bestimmte Eigenschaft unbewiesen ist; was darauf deutet, dass diese Eigenschaft unter bestimmten Bedingungen als richtig, unter anderen dagegen als falsch bewiesen wird. Sämtliche möglichen Ausführungspfade in einem Programm werden einer Über-approximation unterzogen. Methoden wie die Erweiterung und Verengung sowie die Iteration mit einem Solver werden zur Lösung von Gleichungen und Nebenbedingungen eingesetzt, um so die Abwesenheit von Laufzeitfehlern im Quellcode zu beweisen.

Die Identifikation sowie der Nachweis der Abwesenheit dynamischer Fehler wie etwa Laufzeitfehler lässt sich durch Definition einer Stärksten Globalen Invariante SGI(k) erzielen. SGI(k) ist hierbei die Menge aller möglichen Zustände, die am Punkt k in einem Programm P erreicht werden können. Ein Laufzeitfehler wird auftreten, wenn SGI(k) eine verbotene Zone schneidet. SGI(k) ist das Ergebnis formaler Beweismethoden und kann als kleinster Fixpunkte eines monotonen Operators am Graphen einer Menge von Zuständen ausgedrückt werden.

Um die Anwendung der abstrakten Interpretation auf die Codeverifikation zu verdeutlichen, sei angenommen, dass der Code die folgende Operation enthält: X = X/(X-Y)

Eine ganze Reihe von Problemen kann hier einen potenziellen Laufzeitfehler erzeugen. Im Einzelnen sind dies:

• nicht initialisierte Variable,
• ein Über- oder Unterlauf bei der Subtraktions-Operation (X-Y),
• ein Über- oder Unterlauf bei der Divisions-Operation,
• eine Division durch Null, falls X = Y wird,
• ein Über- oder Unterlauf durch die Zuweisung zu X.

Die Division durch Null soll näher betrachtet werden. In der Auftragung von X gegen Y (Bild 2) erkennt man, dass die 45°-Linie und damit der Fall X = Y einen Laufzeitfehler erzeugt. Im Streuplot sind sämtliche Werte dargestellt, die X und Y annehmen können, wenn das Programm diese Codezeile ausführt (als + gekennzeichnet). Dynamische Tests würden nun X und Y über viele verschiedene Kombinationen ausführen, um zu ermitteln, ob hierbei ein Fehler auftritt. Angesichts der großen Zahl der dafür notwendigen Tests kann diese Art zu testen den Laufzeitfehler „Division durch Null“ möglicherweise nicht entdecken noch seine Abwesenheit beweisen.

Eine andere mögliche Methode bestünde darin, den Wertebereich von X und Y im Rahmen der Laufzeitfehlerbedingung (also X = Y) mit Hilfe einer Typenanalyse zu untersuchen. In Bild 3 ist der durch die Typenanalyse eingegrenzte Wertebereich als Kasten eingezeichnet. Schneidet die Gerade X = Y diesen Kasten, dann ist hier ein potenzieller Fehler nicht ausgeschlossen. Einige statische Analysetools nutzen diese Technik. Die Typenanalyse ist in diesem Fall jedoch zu pessimistisch, weil sie unrealistische Werte für X und Y berücksichtigt.

Abstrakte Interpretation am Beispiel Polyspace

Die abstrakte Interpretation erzeugt eine exaktere Darstellung der Wertebereiche für X und Y. Da eine ganze Reihe von Programmier-Konstrukten Einfluss auf die Werte von X und Y nehmen können (Zeiger-Berechnungen, Schleifen, If-Then-Else, Multitasking usw.), definiert man einen abstrakten Graphen. Eine vereinfachte Darstellung dieses Konzepts wäre, sich die Gruppierung von Daten durch Polyederzüge vorzustellen, wie dies in Bild 4 gezeigt ist. Weil das Polyeder die Gerade X = Y nicht schneidet, kann eindeutig geschlossen werden, dass keine Division durch Null auftritt.

(ID:341248)