Home
High Integrity Systeme
Mit formaler Verifikation gegen Laufzeitfehler
11.05.2010 | Autor: Jay Abraham*
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.
 | |
|
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.
Ergänzendes zum Thema
+ Typische Laufzeitfehler in Embedded-Software
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.
Social Networks:
Themenverwandte Beiträge
Code-Verifikation: Simulink Design Verifier 2.0 spürt Logikfehler auf
18.07.2011 - The MathWorks meldet Vollzug: Die Version 2 des Verifikationswerkzeugs Simulink Design Verifier ist verfügbar. Sie enthält Polyspace-Techniken zur Logikprüfung.
weiter
AUTOSAR: ISO-26262-konforme Komponenten ohne Laufzeitfehler
AUTOSAR: ISO-26262-konforme Komponenten ohne Laufzeitfehler
12.12.2011 - Die Einhaltung der Norm ISO 26262 zur funktionalen Sicherheit ist eine große Herausforderung für Steuergeräte-Entwickler. Wir verraten Ihnen, wie sich diese Aufgabe mit Polyspace einfacher bewältigen lässt.
weiter
Software-Testmethoden: Was den Code stark macht
Software-Testmethoden: Was den Code stark macht
05.05.2008 - Wenn die Software ernsthafte Probleme bereitet, liegt dies meist an einer verspäteten Fehlersuche. Moderne Prüfmethoden wie die statische Verifikation leisten in allen Phasen Unterstützung – vom Design bis zur Validierung. Sie garantieren robusten Code, auch wenn der Zeitrahmen für das Projekt eng gesteckt ist.
weiter
Kommentare zu diesem Artikel
Lizenzierung urheberrechtlich geschützter Artikel
Nutzen Sie diesen Artikel ID 341248 oder andere Fachinformationen für Ihr Marketing. Wir bieten Ihnen die Nutzungsrechte für Ihre Website, Ihren Newsletter oder Ihre Kundenzeitschrift. Für alle Fragen wenden sie sich bitte an Frau Maurer unter Tel. 0931 / 418-2888 oder unseren Content-Dienstleister www.mycontentfactory.de .
Artikel versenden
Druckversion
Artikel als PDF
Artikel Bewertung
Wind River
Software Security
Alexander Damisch, Director Industrial Solutions, bei Wind River, zu Sicherheitskonzepten für industrielle Software und dem Umgang der Industrie mit potenziellen Sicherheitsrisiken. weiter
MF Instruments GmbH
Albstadt, Deutschland
Optimierung Ihres Prozessdatenarchivs durch OPC-Technologie
Wie Ihnen OPC hilft Investitionen die Sie zur Speicherung Ihrer Prozessverlausdaten getätigt haben optimal zu nutzen.
Wie Ihnen OPC hilft Investitionen die Sie zur Speicherung Ihrer Prozessverlausdaten getätigt haben optimal zu nutzen.
OPC Unified Architecture: 5 Punkte die jeder wissen sollte
OPC UA - Was ist es, inwiefern hilft es mir, und wo kann ich es bekommen? Dieses Whitepaper fasst die Punkte zusammen, die man über OPC UA wissen sollte.
OPC UA - Was ist es, inwiefern hilft es mir, und wo kann ich es bekommen? Dieses Whitepaper fasst die Punkte zusammen, die man über OPC UA wissen sollte.
Das OPC-Handbuch für Jedermann
In diesem Whitepaper werden die OPC Grundlagen anschaulich erklärt und die Mehrwert von OPC verdeutlicht.
In diesem Whitepaper werden die OPC Grundlagen anschaulich erklärt und die Mehrwert von OPC verdeutlicht.
Effektive OPC-Sicherheit für Steuerungssysteme
Aktuelle Cyber-Attacken, wie z. B. die des Stuxnet-Wurms, sind ein Alarmzeichen für die Automatisierungsbranche. Der Schutz der Steuerungssysteme ist unbedingt notwendig.
Aktuelle Cyber-Attacken, wie z. B. die des Stuxnet-Wurms, sind ein Alarmzeichen für die Automatisierungsbranche. Der Schutz der Steuerungssysteme ist unbedingt notwendig.
Copyright © 2012 Vogel Business Media
(nicht registrierter User)