Qualitätsverbesserung von Embedded Software

Polyspace-Farbkodierung, die den Status der einzelnen Operationen im Code anzeigt.Mathworks

Embedded Software in Systemen mit hoher Zuverlässigkeit wird immer komplexer. Im Militärbereich besteht die Avionik-Software des F-22 Raptor aus 1,7 Millionen Codezeilen und die Avionik-Software des F-35 Joint Strike Fighter wird voraussichtlich auf 5,7 Millionen Codezeilen kommen. In der zivilen Luftfahrt wird das Flugsteuerungssystem der Boeing 787 ca. 6,5 Millionen Codezeilen umfassen. Da die Software dieser Flugzeugkomponenten immer umfangreicher und komplexer wird, steigt das Risiko eines Versagens und erschwert zugleich den Nachweis der geforderten Software-Zuverlässigkeit.

Risikoanalyse zum Software-Versagen

Die Untersuchung des Versagens von Embedded Systemen in der Vergangenheit hilft beim Verständnis von Softwarefehlern. Der fehlgeschlagene Erstflug einer Trägerrakete war beispielsweise auf einen Programmierfehler zurückzuführen. In diesem Fall kam es weniger als eine Minute nach dem Abheben zur Selbstzerstörung der Rakete. Zurückzuführen war der Vorfall auf die hohe aerodynamische Belastung durch einen Anstellwinkel, der über dem festgelegten Sicherheitsbereich lag.

Die anschließende Untersuchung deckte die Ursache des Versagens auf: ein Überlauf, der zu einem Laufzeitfehler bei der Ausführung der Embedded-Software führte. Der gefundene Überlauf in zwei redundanten Inertial-Referenz-Systemen zur Bestimmung von Fluglage und Position der Rakete, trat beim Konvertieren einer 64-Bit-Gleitkommazahl in eine 16-Bit-Ganzzahl mit Vorzeichen auf. Dieser Fehler veranlasste den On-Board-Computer, den Befehl an die Servomotoren zu geben, die beiden Boosterdüsen und das Triebwerk in eine Extremposition zu stellen. Auch die Redundanz des Systems verhinderte die Selbstzerstörung nicht, da auch das Backup-System das selbe Verhalten implementierte.

Mathworks

Der beschriebene Laufzeitfehler stellt eine bestimmte Art von Softwarefehlern dar, die auch als latente Fehler bekannt sind. Diese Fehler sind im Code vorhanden, können jedoch im Rahmen von Systemtests unentdeckt bleiben, sofern die dafür notwendigen Test-Szenarien nicht abgedeckt sind. Der Code scheint daher normal zu funktionieren. In der Praxis führt er allerdings zu unerwartetem Systemversagen oder zufälligem Verhalten. Einige Beispiele von Laufzeitfehlern:

• Nicht initialisierte Daten,
• Out-of-bound Array-Zugriff,
• Nullzeiger-Dereferenzierung,
• Überlauf und Unterlauf,
• Berechnungsfehler,
• gleichzeitiger Zugriff auf gemeinsam verwendete Daten,
• ungültige Typkonvertierungen.

Verifikation von zuverlässigen Systemen

Die Verifikation von Quellcode umfasst gewöhnlich Code-In-spektionen, statische Analysen und dynamische Tests. Jede dieser Methoden hat gewisse Schwächen. Code-Inspektionen sind gänzlich von der Expertise des Prüfers abhängig und können bei einer umfangreichen Codebasis äußerst mühsam sein. Herkömmliche statische Analysen verlassen sich zum Großteil auf einen Musterabgleich, um unsichere Codemuster zu erkennen. Da Embedded Software immer komplexer wird, ist es im Allgemeinen nicht mehr möglich, zudem alle Betriebszustände dynamisch zu testen. Die Abwesenheit von Laufzeitfehlern kann damit nicht nachgewiesen werden.

Eine neue, als abstrakte Interpretation bekannte Verifikationsmethode baut auf statischen Analysemethoden auf. Durch den Einsatz formeller mathematischer Beweise können bestimmte Laufzeitfehler identifiziert beziehungsweise deren Abwesenheit nachgewiesen werden. Die abstrakte Interpretation wird auf den Quellcode angewendet, ohne dass dieser im Rahmen von dynamischen Tests ausgeführt wird.

Abstrakte Interpretation und nachweisgestützteVerifikationsmethoden

Die abstrakte Interpretation als nachweisgestützte Verifikationsmethode kann durch die Multiplikation von drei großen Ganzzahlen in der folgenden Aufgabe verdeutlicht werden:

–4586 × 34985 × 2389 = ?

Obwohl die manuelle Berechnung der Lösung der Aufgabe zeitaufwändig sein kann, belegen Multiplikationsregeln schnell, dass das Vorzeichen des Ergebnisses negativ sein wird und niemals positiv sein kann. Die Bestimmung des Vorzeichens dieser Berechnung ist eine Anwendung der abstrakten Interpretation. Durch die Methode sind bestimmte Eigenschaften des Endergebnisses, wie das Vorzeichen, bekannt, ohne dass die Multiplikation der Ganzzahlen abgeschlossen werden muss.

Um bestimmte Eigenschaften der Software nachzuweisen, kann die abstrakte Interpretation auf ähnliche Weise auf die Semantik von Software angewendet werden. Durch die Verifikation bestimmter dynamischer Eigenschaften des Quellcodes ohne Ausführung des eigentlichen Programms wird mit der abstrakten Interpretation die Lücke zwischen konventionellen statischen Analysemethoden und dynamischen Tests geschlossen. Bei der abstrakten Interpretation werden in einem Durchgang alle möglichen Ablaufszenarien eines Programms untersucht. Alle möglichen Kombinationen von Werten werden durchgespielt, um zu ermitteln, wie und unter welchen Bedingungen das Programm bestimmte Arten von Laufzeitfehler aufweisen könnte. Die Ergebnisse der abstrakten Interpretation gelten als sicher, da mathematisch nachgewiesen werden kann, dass durch die Methode das richtige Resultat vorausberechnet wird.

Einsatz der abstrakten Interpretation zur Verifikation von Software

Die abstrakte Interpretation kann als statische Analysemethode genutzt werden, um die An- und Abwesenheit bestimmter Laufzeitfehler im Quellcode, wie beispielsweise Überlauf, Division durch Null und unzulässiger Array-Zugriff, zu erkennen und mathematisch nachzuweisen. Die Verifikation wird durchgeführt, ohne dass eine Ausführung des Programms, eine Code-Instrumentierung oder Testsituationen erforderlich sind. Polyspace-Codeverifikationsprodukte von MathWorks basieren auf dieser Art der statischen Analyse. Als Eingabe für ein Polyspace-Werkzeug eignet sich C-, C++- oder Ada-Quellcode. Das Polyspace-Werkzeug untersucht zunächst den Quellcode, um zu ermitteln, wo mögliche Laufzeitfehler auftreten können. Danach wird ein Bericht mit einer Farbkodierung ausgegeben, um den Status der einzelnen Elemente im Code anzuzeigen (siehe Bild und Tabelle).

Gänzlich grün markierte Polyspace-Ergebnisse weisen darauf hin, dass der Code bestimmte Laufzeitfehler nicht aufweist. Wenn mögliche Laufzeitfehler erkannt und in rot, grau oder orange markiert wurden, können Software-Entwickler und Tester die durch die Verifikation gewonnenen Zusatzinformationen zum Beheben der identifizierten Laufzeitfehler verwenden.

Schlussfolgerung

Eine statische Analyse, die durch die abstrakte Interpretation erweitert wird, kann die Qualität und Zuverlässigkeit von Embedded Systemen verbessern. Die Methode unterstützt Entwickler dabei, die Abwesenheit bestimmter Laufzeitfehler in Software nachzuweisen. Eine Lösung zur Codeverifikation, die die abstrakte Interpretation einschließt, kann beim Erreichen eines guten Qualitätsprozesses eine wichtige Rolle spielen. Zudem erhöht das Wissen über nachweislich korrekte Code-Eigenschaften das Vertrauen in die Software und hilft, den Aufwand für Code-Inspektionen und Robustheits-Tests zu senken. Es handelt sich um eine ausgereifte Verifikationsmethode, um eine hohe Zuverlässigkeit bei Embedded-Geräten zu erzielen.

(jj)