Durch mathematisch nachgewiesene Korrektheit des Codes sowie durch Hardware Awareness lässt sich in Systemen, in denen es auf Safety und Security ankommt, eine 100-prozentige Codeabdeckung und eine Fehlerquote von null erreichen.
Wenn Embedded-Entwickler ihre Software testen, sind stets mehrere Kräfte am Werk. Die beständig zunehmende Komplexität der Systeme, getrieben von den Forderungen nach mehr Rechenleistung und umfangreicherer Konnektivität sowie nach mehr Safety und Security, macht es für Entwickler immer schwerer, ihren Code anhand der Lastenhefte zu validieren. Wenn zusätzlich die Release-Zeiträume immer kürzer werden, haben es die Testteams außerdem schwer, traditionelle Testmethoden an die höhere Komplexität und den gestiegenen Umfang anzupassen.
Es ist somit notwendig, ganz neu an das Testen heranzugehen und zum Beispiel auf den mathematischen Nachweis der Korrektheit des Codes zu setzen, um das Vertrauen in eine Applikation entscheidend zu steigern. Die Lücke zwischen den Zielvorgaben heutiger Produkte und den Möglichkeiten traditioneller Testmethoden wird besser deutlich, wenn der Einfluss der Komplexität auf das Testen betrachtet wird:
Seit langer Zeit hält sich hartnäckig die Auffassung, eine Codeabdeckung von nahezu 100 % sei unter anderem aus Kostengründen unmöglich zu erreichen. Tatsächlich verursachen traditionelle Testverfahren wie etwa Modultests, Penetrationstests und dynamische Analysen zwar einen übermäßigen Zeit- und Ressourcenaufwand, liefern aber dennoch nur ein unvollständiges Bild der in einem System vorhandenen Fehler und Schwachstellen.
Dass eine 100-prozentige Testabdeckung wirklich unerreichbar ist, wurde aber dank der jüngsten Fortschritte bei den Softwaretechniken und hinsichtlich der Rechenleistung hinreichend widerlegt. Im Zuge von Forschungsarbeiten der Hochschulen und der Industrie wurden mathematisch rigorose Techniken – sogenannte formale Methoden – entwickelt, die es auf eine Codeabdeckung von bis zu 100 % bringen und die Korrektheit von Systemen garantieren können. Diese Techniken sind inzwischen in unternehmenstauglichen Plattformen für die Entwicklung von safety- und securitykritischen Projekten verfügbar.
Auf dem Papier liefern formale Methoden den kategorischen Nachweis, dass der Code frei von Problemen wie etwa Bugs oder Sicherheitslücken ist. Mit rigoros spezifizierten mathematischen Modellen verifizieren diese Methoden die Eigenschaften und das Verhalten der jeweiligen Software anhand präzise definierter Spezifikationen. Anders ausgedrückt, sind formale Methoden in der Lage, jegliche Probleme im Code aufzudecken.
In der Praxis sind unternehmenstaugliche, auf formalen Methoden basierende Testwerkzeuge für alle Entwickler zugänglich und erschwinglich. Sie sind als gründliche statische Analyse-Tools (Exhaustive Static Analysis Tools) bekannt und so konzipiert, dass sie die Fähigkeiten formaler Methoden in die bestehenden Verifikations- und Validierungsprozesse von Entwicklungsteams einbinden, die an safety- und securitykritischen Projekten arbeiten.
Bild 1 zeigt den Unterschied deutlich. Traditionelle Testmethoden gehen bei der Testfallentwicklung und dem Algorithmenentwurf nach dem Best-Effort-Prinzip vor und werden dabei durch die Fähigkeiten des Menschen und die Projektzeitpläne eingeschränkt. Das Resultat sind Tests, die pro Durchgang nur einen einzigen Codezweig ausführen, wodurch in einem bestimmten Testzeitraum nur ein begrenzter Teil des Codes getestet werden kann. Eine vollständige statische Analyse, gestützt durch formale Methoden, kann dagegen in einem Testdurchlauf sämtliche Zweige prüfen, sodass die Testabdeckung auf 100 % steigt und der Zeitaufwand dramatisch sinkt.
Die gründliche statische Analyse kann die Art und Weise, wie Entwickler die Komplexität von Software beurteilen, grundlegend verändern, indem ihnen eine wirkungsvolle Methode zum Umgang mit dieser Komplexität in die Hand gegeben wird.
Ein Mangel traditioneller Testmethoden betrifft die Abdeckung des Zustandsraums. Anders ausgedrückt, können diese Methoden nur eine begrenzte Zahl unterschiedlicher Kombinationen von Datenwerten und Eingaben, Kontroll- und Datenflussvarianten sowie Ausgangspfaden abdecken. Unter anderem prüfen traditionelle Testmethoden die Funktionen nur auf erwartete Ausgaben bei erwarteten Eingaben. Einige statische Analysetools gehen zwar noch einen Schritt weiter und decken einen größeren Bereich von Ein- und Ausgaben ab, jedoch sind die Tools infolge von Restriktionen in Bezug auf den Entwurf, die Implementierung und den Zeitplan der Tests nicht in der Lage, alle möglichen Verhaltensvarianten zu testen.
Der folgende Codeausschnitt zeigt eine C-Funktion, die die Werte von Zellen in einem Array inkrementiert.
Ein typischer Modultest würde die Validierung hier anhand der Anforderungen an die Funktion vornehmen und überprüfen, ob die Funktion die Zellenwerte im ausgegebenen Array tatsächlich inkrementiert hat, um je nach Ergebnis ein »pass« oder »fail« zu melden. Allerdings würde dieser Test nicht unbedingt prüfen, ob der Array-Index *p aufgrund von unerwarteten oder unerwünschten Nebeneffekten im System einen über die Grenzen des Arrays hinausreichenden Speicherzugriff ausgeführt hat, wie es in diesem Codebeispiel wegen einer in der while-Schleife spezifizierten unkorrekten Bedingung der Fall ist.
Ungeachtet des Pufferüberlaufs würde ein traditioneller, an den Anforderungen orientierter Test lediglich verifizieren, dass der Inhalt des Arrays nach Aufrufen der Funktion {2, 4, 6, 8} lautet – und er somit stets ein »pass« als Resultat ausgeben, wie der folgenden Konsolenausgabe zu entnehmen ist:
Solange die Testingenieure die Möglichkeit eines über die Arraygrenzen hinausreichenden Zugriffs nicht einkalkulieren, wird dieser Pufferüberlauf also niemals aufgedeckt werden.
Subtile Fehler dieser Art können zu Verfälschungen von Speicherinhalten führen, die wiederum Bugs, Abstürze oder Sicherheitslücken der Applikation verursachen können. Obwohl sie traditionellen Testmethoden verborgen bleiben, lassen sie sich mit gründlichen statischen Analysetools aufdecken, wie in Bild 2 zu sehen ist.
Das Tool erkennt, dass nach Beginn des Arrays 16 Byte geschrieben werden und somit ein Pufferüberlauf vorliegt.
Diese Verfälschung des Speicherinhalts lässt sich mit einem etwas ausführlicheren Testfall aufdecken, in dem sich die über die Grenzen hinausgehenden Schreibzugriffe auf den Wert des Variablennamens auswirken, obwohl dieser nicht in die getestete Funktion involviert ist. Siehe dazu die folgende Konsolenausgabe:
Entwicklungsteams implementieren jedoch nur selten derart fundierte Tests – insbesondere dann nicht, wenn der Code komplexer ist als in diesem Beispiel.