High Integrity Systeme Mit formaler Verifikation gegen Laufzeitfehler

Bei großem Umfang und hoher Komplexität von Embedded-Software sind konventionelle Verifikations- und Testmethoden oft keine optimale Lösung mehr. Dieser Artikel beschreibt den Einsatz zuverlässiger Verifikationsverfahren, wie sie sich z.B. für die Entwicklung von High Integrity Software anbietet.

Anbieter zum Thema

MicroConsult Academy GmbH

MES Electronic Connect GmbH & Co. KG

Cadlog Group

The MathWorks GmbH

Der Umfang und die Komplexität der in High Integrity Systemen eingesetzten Software nimmt stetig zu. Konventionelle Verifikations- und Testmethoden sind für diese Software keine optimale Lösung mehr. Dieser Artikel beschreibt den Einsatz zuverlässiger Verifikationsverfahren für die Entwicklung von High-Integrity-Software. Er konzentriert sich dabei vor allem auf die Anwendung formaler Methoden basierend auf Abstrakten Interpretationsverfahren, mit deren Hilfe die Abwesenheit einer definierten Menge von Laufzeitfehlern mathematisch bewiesen werden kann.

Verbreitete Verifikationsmethoden für Embedded-Software sind Codereviews, statischen Analysen und dynamische Tests. Codereviews stehen und fallen mit der Fachkompetenz des Prüfers und können für große Code-Basen ineffizient sein. Konventionelle statische Analysemethoden fußen hauptsächlich auf einem Mustersuchverfahren, mit dem nach unsicheren Codemustern gesucht wird, können aber nicht die Abwesenheit von Laufzeitfehlern beweisen. Letztlich ist es angesichts der wachsenden Komplexität der Gerätesoftware praktisch unmöglich, diese unter allen denkbaren Arten von Betriebsbedingungen zu testen.

Ein häufiges Problem in High-Integrity-Software: Laufzeitfehler

Eine häufige Ursache für Versagensfälle eingebetteter Systeme sind Laufzeitfehler. Laufzeitfehler sind eine spezifische Klasse von Softwarefehlern, die als latente Fehler bezeichnet werden. Diese können im Code vorhanden sein, lassen sich im System aber nur feststellen, wenn sehr spezifische Tests unter ganz besonderen Bedingungen durchgeführt werden. Oberflächlich kann der Programmcode den Anschein erwecken, als funktioniere er völlig normal, es können aber trotzdem unerwartete Fehlfunktionen mit zuweilen fatalen Konsequenzen auftreten.

Einige Ursachen für Laufzeitfehler sind:

• nicht initialisierte Daten,
• Array-Zugriffe außerhalb der definierten Grenzen,
• dereferenzierte Nullzeiger,
• Berechnungsfehler,
• gleichzeitiger Zugriff auf gemeinsam genutzte Daten,
• illegale Datentypkonvertierungen,
• Endlosschleifen.

Das erklärte Ziel von Code-Reviews besteht darin, Fehler im Code zu finden. Ein weiterer Aspekt können Prüfungen der Konformität mit bestimmten Programmierstandards sein wie etwa MISRA-C oder JSF++ (für C und C++). Das Aufspüren subtiler Laufzeitfehler kann sich schwierig gestalten. So können beispielsweise Überläufe oder Unterläufe leicht übersehen werden, die durch komplexe mathematische Berechnungen erzeugt werden.

Dynamische Tests verifizieren den Ablauf bei der Ausführung von Software, also z.B. Entscheidungspfade, Eingaben und Ausgaben. Es werden zunächst Testfälle und Testvektoren erzeugt und dann die Software gegen diese Tests ausgeführt. Danach werden die Testergebnisse mit dem erwarteten oder bekannten korrekten Verhalten verglichen. Analysen haben gezeigt, dass die durchschnittliche Effektivität dynamischer Tests bei nur etwa 47% liegt. Mit anderen Worten bleiben bei dynamischen Tests mehr als die Hälfte aller Fehler unentdeckt.

Die statische Analyse stellt ein noch relativ neues Verfahren dar, das die Software-Verifikation weitgehend automatisiert. Sie zielt darauf ab, Fehler im Programmcode zu identifizieren, beweist aber nicht notwendigerweise deren Abwesenheit. Der Prozess einer statischen Analyse basiert auf Heuristiken und Statistiken und es müssen weder Testfälle entwickelt noch Code ausgeführt werden. Die damit gefundenen Fehlertypen kann man sich als starke Compiler-Typisierung (etwa die Überprüfung, ob Variablen stets initialisiert oder verwendet werden) im Rahmen einer ausführlichen Datenfluss-Analyse vorstellen.

Das Problem der False Positives und False Negatives

Solche Tools können zweifellos Fehler im Code finden, dies aber mit einer hohen Rate von False Positives. Der Begriff False Positive bezieht sich auf die Identifikation eines Fehlers, der nicht real ist. Die mittlere Zahl von False Positives beträgt laut Analysen bei einigen statischen Analysetools 66%. Neben den False Positives ist es außerdem wichtig, False Negatives zu verstehen. Man spricht von einem False Negative, wenn ein statisches Analysetool einen Fehler nicht entdeckt.

Der Begriff formale Methoden wurde typischerweise für die auf Beweise gestützte Verifikation eines Systems gegen seine Spezifikation verwendet. Der gleiche Terminus kann aber auch einen mathematisch stringenten Ansatz zum Beweis der Korrektheit von Programmcode meinen. Dieser Ansatz kann helfen, die Zahl von False Negatives zu verringern, das heißt, er kann helfen, eindeutig die Abwesenheit bestimmter Laufzeitfehler festzustellen. Der folgende Abschnitt beschreibt den Einsatz der abstrakten Interpretation als eine auf formalen Methoden basierende Verifikationslösung, die auf Softwareprogramme angewandt werden kann.

(ID:341248)