Technische Artikel

Verifikation von Code mit hohen Anforderungen an die Zuverlässigkeit

Von Paul Barnard, MathWorks, Marc Lalo, MathWorks, und Jim Tung, MathWorks


Bei vielen Embedded Software-Projekten besteht das Hauptziel der Verifikation im Aufspüren möglichst vieler Programmfehler in möglichst kurzer Zeit. Die üblicherweise eingesetzten statischen Analyse-Tools eignen sich zwar gut zur Identifikation offensichtlicher Mängel, können aber nicht die Fehlerfreiheit des Quellcodes beweisen. Sie bieten daher keinen Schutz vor endlosen Debugging-Schleifen und einer langatmigen Code-Überprüfung. Deutlich schwerer wiegt aber, dass mit ihnen Fehler mit potenziell katastrophalen Folgen unentdeckt bleiben. Für Anwendungen, die eine hohe Zuverlässigkeit erfordern, ist dies nicht akzeptabel. Polyspace™ Code-Verifikationsprodukte verfolgen einen alternativen Ansatz: Sie beweisen mathematisch die Fehlerfreiheit für bestimmte Typen von Laufzeitfehlern.

Zum Nachweis der Fehlerfreiheit muss ein Verifikationstool jeden Codeabschnitt vollständig untersuchen und seine Zuverlässigkeit unter Berücksichtigung jedes möglichen Datenwertes verifizieren. Die hierbei zu bewältigenden Aufgaben sind mathematisch oft so anspruchsvoll, dass sie die Fähigkeiten eines normalen Fehlerdetektions-Tools übersteigen. Ein solches Tool muss beispielsweise:

  • Numerische Algorithmen lösen
  • Pointer interpretieren
  • Programmkonstrukte wie Schleifen oder If-Then-Else-Anweisungen und unentscheidbare Bedingungen mathematisch modellieren
  • Alle sprach-spezifischen Konstruktionen lesen können

Außerdem muss es über leicht verständliche und einfach zu bedienende Diagnosefähigkeiten verfügen (Abb. 1).

verifying_code_fig1_w.gif
Abb. 1. Einfache Farbkodierungen visualisieren die Ergebnisse der Code-Verifikation. Zum Vergrößern auf das Bild klicken.

Lösung numerischer Algorithmen

Einer der im folgenden Programmabschnitt möglichen Fehler, deren Abwesenheit nachgewiesen werden muss, ist die Division durch Null in der hervorgehobenen Zeile. Das Problem lässt sich auch als Frage formulieren: Können x und y zur gleichen Zeit identische Werte annehmen?

verifying_code_code_sample1_w.gif

Zur Beantwortung dieser Frage muss das Verifikationstool x und y statisch berechnen, und zwar Zeile für Zeile und von Anfang an. Ein rein visuelles Code-Review ließe sich auf diese Weise niemals mit ausreichender Gründlichkeit durchführen.

Um derartige numerische Probleme zu lösen, müssen Code-Verifikationstools die Daten möglichst genau verstehen und modellieren, beispielsweise durch Eingrenzung als komplexe Vielecke oder andere geometrische Formen (Abb. 2).

verifying_code_fig2_w.gif
Abb. 2. Ansammlungen von Datenpunkten lassen sich durch komplexe Vielecke approximieren; dies wird intern von Verifikations-Tool genutzt. Zum Vergrößern auf das Bild klicken.

Lesen von Pointern (Aliasing)

Wenn sich Daten auf andere Daten beziehen, was in C etwa durch Pointer realisiert wird, muss das Verifikationstool ursprüngliche und darauf bezug nehmende Daten erkennen. Anschließend muss es eine Pointer-Analyse durchführen, die ermittelt, auf welche Weise diese Daten sich gegenseitig beeinflussen.

Im folgenden Code muss das Verifikationstool erkennen, dass das Aliasing durch eine bedingte Neuzuweisung in der ersten hervorgehobenen Zeile verändert wird.

verifying_code_code_sample2_w.gif

Am Ende dieser Anweisung zeigt ptr entweder auf x oder auf y, abhängig davon, welcher Pfad ausgeführt wurde. In beiden Fällen ist tmp größer als –19. In der zweiten hervorgehobenen Zeile kann also niemals eine Division durch Null auftreten.

Modellierung von Programmier-Konstrukten

Ein Verifikationstool muss die Syntax ver­stehen, die verschiedenen Programmier-Konstrukten wie For-Schleifen, If-Then-Else oder unbestimmten Bedingungen zu Grunde liegt. Es muss also beispielsweise mathematisch berechnen, was innerhalb einer Endlosschleife geschieht, ohne diese auszuführen (Abb. 3).

verifying_code_fig3_w.gif
Abb. 3. Oben: In diesem Modell werden Variablen in zwei Schritten abgespeichert. Unten: Der aus dem Modell generierte Code zeigt, wie Wertebereiche von Daten auch aus Endlosschleifen heraus weitergegeben werden können. Zum Vergrößern auf das Bild klicken.

Lesen sprachspezifischer Konstruktionen

In bestimmten Sprachen, auch in C++, kann hinter einer einzigen Programmzeile eine große Menge von Rechenoperationen stecken. Durch objekt-orientierte Konstrukte wie Vererbung, Polymorphismen und Templates wird C++-Code außerdem schnell unübersichtlich. Das Verifikations-Tool muss mathematisch ermitteln, welche Anweisungen in jeder Programmzeile ausgeführt werden.

Umfassende Unterstützung anspruchsvollster Aufgaben

Der Beweis der Fehlerfreiheit von Quellcode für Laufzeitfehler wie Überläufe, Divisionen durch Null und Array-Zugriffen außerhalb des gültigen Bereichs ist eine sehr aufwändige Aufgabe, die formale mathematische Methoden und ein vollständiges Verständnis der Semantik einer Sprache voraussetzt. Polyspace-Produkte machen diese Aufgabe durchführbar, weil sie den Quellcode verifizieren, ohne ihn zu kompilieren oder auszuführen. Eben dieses Arbeiten mit dem Quellcode garantiert die Anwendbarkeit der Methode auf handgeschriebenen, automatisch generierten und beliebig aus beiden Sorten gemischten Programmcode.

Neben der Code-Verifikation testen Polyspace-Tools auch auf MISRA-C-Konformität. Für Anwendungen mit automatisch aus Simulink-Modellen oder UML-Diagrammen generiertem Programmcode gibt es außerdem Polyspace Link-Produkte, die die Verifikationsergebnisse wieder mit dem Ursprungsmodell verknüpfen.

Polyspace-Produkte haben sich in allen Bereichen der Entwicklung und Verifikation von Software bewährt (siehe Kasten). So wurden sie etwa als Quality-Gate für von unterschiedlichen Entwicklerteams geschriebenen Code eingesetzt oder in die Submit- und Build-Phasen für separate Software-Komponenten integriert und konnten so den Entwicklern ein schnelleres Feedback geben. Zusammen mit den Link-Produkten für Modellierungs-Tools wie Simulink und Rhapsody wurde Polyspace außerdem in der Designphase eingesetzt, um Systemingenieuren oder Algorithmenentwicklern durch Analysen des automatisch generierten Codes beim Aufspüren von Schwächen eines Entwurfs zu helfen.

Code-Verifikation mit Polyspace

Delphi Diesel Systems entwickelt für OEM-Kunden aus dem Automobilsektor Diesel-Einspritztechnologien, die Motoren leiser, spar­samer, schadstoffärmer und durchzu­gsstärker machen. Delphi setzt Polyspace-Produkte ein, um Software-Module direkt nach deren Erstellung zu analysieren bevor Funktions­tests fertiger Bauteile durchgeführt werden.

Das NATO HAWK Management Office (NHMO) unterhält verschiedene komplexe, missionskritische Anwendungen für das Boden-Luft-Raketensystem HAWK. Zur Einhaltung von Zuverlässigkeits-Standards muss das NHMO-Team Laufzeitfehler identifizieren und beseitigen. Es führt hierzu detaillierte Analysen zur Dynamik der Anwendungen mit Polyspace-Produkten durch, anhand derer Prioritäten für Code-Reviews festgelegt werden.

CSEE Transport, ein führender Entwickler von Signal- und Leitsystemen für Hoch­geschwindigkeitszüge, nutzt Polyspace-Produkte zur Verifikation der Sicherheitssoftware seiner Signalsysteme. Mit klassischen Verifikationsmethoden lassen sich bestimmte Fehler im handgeschriebenen ADA-Code grund­sätzlich nicht entdecken. CSEE Transport setzt Polyspace-Produkte außerdem zur Validierung einzelner Module vor deren Integration ein.

Die GlucoLight Corporation hat ein auf Bildverarbeitung beruhendes, nicht-invasives System zur Dauer­überwachung des Blutzuckerspiegels entwickelt. Zur Verbesserung der Zuverlässigkeit der von Zulieferern bereitgestellten Embedded Software sowie zur Vorbereitung auf die FDA-Zertifizierung wurde neuer oder veränderter C++-Code klassenweise mit Polyspace-Produkten verifiziert. Hierbei konnten mit Polyspace fehleranfällige Strukturen identifiziert und in Folgeversionen des Codes ersetzt werden.

Veröffentlicht 2008 - 91607v00

Weitere Informationen

Artikel für ähnliche Einsatzgebiete anzeigen