Polyspace spürt Laufzeitfehler auf

02.06.2005
Polyspace Verifier prüft Programmcode mittels semantischer Analyse.

Klassische Methoden für das Software-Testing verursachen in Unternehmen immer noch 60 bis 70 Prozent der Gesamtkosten einer Softwareentwicklung. Immer öfter werden deswegen notwendige Tests auf Unit- oder Modulebene gestrichen - im Vertrauen darauf, dass Laufzeitfehler spätestens beim Systemtest auffallen. Einen solchen Bug zu finden, dauert eine Stunde. Taucht der Fehler erst im Integrationstest auf, benötigen Experten zehn, bei der abschließenden Validierung bis zu 100 Stunden.

Statische Verifikation

Dem soll das in Deutschland noch weitgehend unbekannte Tool "Polyspace Verifier" von der Polyspace Technologies GmbH aus Weßling-Oberpfaffenhofen entgegenwirken. Es beruht auf der bereits vor 20 Jahren entwickelten Methode zur "statischen Verifikation von Software", arbeitet nach dem Prinzip der abstrakten Interpretation und prüft laut Anbieter Programme in einem Bruchteil der Zeit, die andere Verfahren benötigen.

Der Verifier steht für die Programmiersprachen C, C++ und die beiden Ada-Versionen 83 und 95 zur Verfügung. Anwender sind unter anderem Eads, die Nasa, Volkswagen, Siemens und General Electric. Im Gegensatz zu herkömmlichen Tests führt das Prüfverfahren die Software nicht aus, sondern analysiert sie anhand eines mathematischen Verfahrens.

Das Problem, Laufzeitfehler eines Programms nicht automatisch vorab bestimmen zu können, da die exakte Menge der möglichen Systemzustände nicht zu berechnen ist, umgeht der Hersteller in seinem Produkt: Der Datentyp gibt Variablen eine bestimmte Spannweite möglicher Ausprägungen vor. Ausgehend vom Datenfluss berechnet Polyspace Verifier dann, welchen Wertebereich jede Variable zu einem Zeitpunkt beinhalten kann. Durch Approximation lässt sich die Anzahl der tatsächlich möglichen Zustände darstellen. Über die semantische Analyse können dann Verhaltensweisen eines Programms überprüft werden, indem für jede Operation berechnet wird, ob nicht erlaubte Zustände (Division durch Null, Overflow etc.) auftreten können.

Den Vorteil statischer gegenüber dynamischer Testverfahren begründet der Hersteller damit, dass sich mit dynamischen Softwaretests nur feststellen lässt, ob ein Fehler vorliegt, aber nicht, worin er besteht. Dann müsse mit Debugging erhebliche Zeit investiert werden, um zur Ursache zu gelangen. Fehler bleiben unentdeckt, weil Testszenarien nicht ausgeführt wurden oder weil die Bugs auf das erwartete Testergebnis keinen Einfluss hatten (Lesezugriff auf nicht initialisierte oder unabsichtlich überschriebene Daten).

Ein weiterer Nachteil dynamischen Testens sei, dass jeder Tester den Programmcode wiederum verändert und so neue Fehler auftreten können. Dagegen könnten mittels der statischen Verifikation alle Fehler ohne Eingriff in den Quellcode gefunden werden. Gegenüber dem weit verbreiteten Faganschen Inspektionsprozess habe die automatisierte Prüfung den Vorteil, dass sie wesentlich schneller abläuft: 400 Zeilen Quellcode soll der Verifier in etwa zehn Minuten überprüfen - dazu benötigten vier Inspektoren nach Fagan jeweils sechs Stunden. (ue)