Startseite > Automotive > Software + Tools > Schwere Fehler sicher ausschließen

Modellbasierte Enwicklung

Schwere Fehler sicher ausschließen

15. April 2014, 13:03 Uhr | Von Dr. Daniel Kästner und Carsten Rustemeier

▶ Diesen Artikel anhören

Fortsetzung des Artikels von Teil 2

Laufzeitfehler

Eine weitere Klasse kritischer Programmierfehler sind die sogenannten Laufzeitfehler, wie arithmetische Überläufe, Feldgrenzenverletzungen oder ungültige Zeigerzugriffe. Sie können die Datenintegrität eines Programms zerstören und fehlerhafte Systemreaktionen bis hin zum Systemabsturz verursachen. Die Explosion der Ariane-Rakete im Jahr 1996 ist ein bekanntes Beispiel für mögliche Auswirkungen eines Laufzeitfehlers.

Ein Beispiel eines statischen Laufzeitfehler-Analysators auf Basis der abstrakten Interpretation ist Astrée, das alle möglichen Laufzeitfehler in C-Programmen findet und damit die Abwesenheit von Laufzeitfehlern beweisen kann. Der Kern von Astrée besteht in einer optimierten Werteanalyse, die Zusammenhänge zwischen Variablen erkennt und die möglichen Variablenwerte präzise approximieren kann. Die Präzision des Analysators lässt sich zudem genau an die zu analysierende Software anpassen, so dass die vorhandene Rechenleistung effizient genutzt werden kann. Das ermöglicht niedrige Fehlalarmraten bei kurzer Analysedauer: Sicherheitskritische Avionik-Software von mehr als 500.000 Zeilen Code konnte auf einem handelsüblichen PC in 6 Stunden ohne Fehlalarm analysiert werden [11].

Tool-Kopplung

In einer modellbasierten Entwicklungsumgebung ist es leicht möglich, Modelle zu ändern, zu verfeinern und die Codeerzeugungsoptionen zu variieren. Nach jeder Änderung sollten die Auswirkungen auf Verhalten und Sicherheit des Steuerungssystems untersucht werden. Simulationsbasierte Prüfungen sind in moderne modellbasierte Entwicklungsumgebungen gut integriert, aber ein sicherer Nachweis nichtfunktionaler Anforderungen ist in der Regel nicht möglich. Das Ziel der Kopplung von aiT, StackAnalyzer und Astrée mit TargetLink besteht darin, diese Lücke zu schließen und die Arbeitsabläufe innerhalb des iterativen Entwicklungsprozesses effizient zu gestalten. Zudem ist es wichtig, dass die Analysatoren Informationen auswerten können, die im TargetLink-Modell enthalten, aber nicht Teil des generierten Codes sind. Durch eine automatische Berücksichtigung dieser Informationen können eine fehleranfällige Mehrfachspezifikation dieser Angaben vermieden und die Analyseergebnisse verbessert werden.

Jobangebote+ passend zum Thema

Regional Key Account (m/w/d) für Elektronische Bauteile

KOA Europe GmbH, Dägeling

Alle Jobangebote im Elektroniknet Karrierebereich anzeigen

Bild 1 zeigt den Arbeitsablauf der Kopplung von TargetLink mit aiT zur Berechnung der maximalen Ausführungszeit. Zunächst wird der generierte Code kompiliert und gelinkt, um eine ausführbare Binärdatei zu erhalten. Dieser Schritt ist für die Laufzeitfehleranalyse nicht erforderlich, weil Astrée auf dem generierten C-Code arbeitet. Anschließend werden die Informationen über die durchzuführende Analyse in eine XML-Datei im XTC-Format geschrieben.

XML Timing Cookie (XTC) ist ein standardisiertes Austauschformat, das eine generische Schnittstelle für den Datenaustausch beliebiger Analyse- und Verifikationswerkzeuge darstellt [12]. XTC wurde im Rahmen verschiedener internationaler Forschungsprojekte entwickelt, darunter „Interested“, „All-Times“, „Timmo-2-Use“ und „MBAT“. In XTC wird unter anderem festgelegt, welcher Analysetyp durchzuführen ist, welche Dateien analysiert werden sollen, der Eintrittspunkt der Analyse wird spezifiziert und die Analyseoptionen werden bestimmt. Eine solche Projektkonfiguration wird automatisch für jede Root-Funktion des TargetLink-Modells erzeugt.

Das TargetLink Data Dictionary enthält detaillierte Informationen über den erzeugten Code, beispielsweise aufzurufende Root-Funktionen, Wertebereiche von Eingangs- und Ausgangsvariablen, Schleifengrenzen, Informationen über Interpolationsfunktionen usw. Durch Berücksichtigung dieser Informationen lässt sich eine hohe Analysepräzision erreichen, was sich zum Beispiel in einer sehr niedrigen Zahl von Fehlalarmen niederschlägt. Alle relevanten Informationen werden automatisch in formale Analysedirektiven umgesetzt. Die verwendeten Annotationssprachen sind offene Formate [13], die keinerlei Modifikation der analysierten Dateien erfordern und robust gegenüber Code-Änderungen sind.

Für die Laufzeitfehleranalyse wird eine Eintrittsfunktion generiert, die das Ausführungsmodell beschreibt. Zunächst werden Initialisierungsfunktionen ausgeführt, anschließend werden die Root-Funktionen des Modells aus einer reaktiven Schleife heraus aufgerufen. Für Eingabevariablen werden die im Modell angegebenen Wertebereiche angenommen oder aber der volle Wertebereich, sofern keine Bereichsangaben vorliegen. Für Wertebereiche von Ausgangsvariablen werden statische Assertions generiert, die einen formalen Beweis über die Einhaltung des Wertebereichs ermöglichen.

Die entsprechenden dynamischen Funktionstests lassen sich eliminieren. Im Falle der WCET- oder der Stack-Analyse ist kein spezieller Eintrittspunkt nötig, weil die Ausführungszeit und der Stack-Bedarf separat für jede Root-Funktion (runnable) berechnet werden.

Alle Arbeitsschritte sind vollständig automatisiert und lassen sich aus dem AbsInt-Menü des Simulink/TargetLink-Modellfensters starten (Bild 2).

Die Analysen lassen sich automatisch ausführen, zum Beispiel, wenn mit TargetLink neuer Code erzeugt wird oder Regressionstests ausgeführt werden. Nach beendeter Analyse wird die maximale Ausführungszeit jeder TargetLink-Root-Funktion (aiT), ihr maximaler Stack-Bedarf (StackAnalyzer) sowie Benachrichtigungen über potenzielle Laufzeitfehler (Astrée) in XML-basierte Ergebnisdateien geschrieben, die sich über den Menüeintrag Results in TargetLink öffnen lassen.

Zusätzlich werden die Informationen über maximale Ausführungszeit und maximalen Stack-Bedarf im Data Dictionary gespeichert. Auf diese Weise können sie automatisch in die TargetLink-Modelldokumentation übernommen oder für AUTOSAR-Authoring-Werkzeuge wie SystemDesk im standardisierten AUTOSAR-Format exportiert werden.

Wird TargetLink mit der Option „generate model-linked code view“ aufgerufen, werden die generierten HTML-Dateien automatisch in Astrée geöffnet. Das vereinfacht nicht nur die Analyse möglicher Laufzeitfehler, sondern ermöglicht auch eine direkte Rückverfolgung von Implementierungsfehlern auf Modellebene (Bild 3).