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 1

Code-Generierung und Simulation

TargetLink [5] erzeugt aus Matlab/Simulink/Stateflow-Modellen effizienten C-Code für Serienproduktanwendungen. Eine wichtige Eigenschaft von TargetLink ist die Trennung zwischen Implementierungsdaten – zum Beispiel Informationen über die generierten Funktionen, Variablen und Wertebereiche – und dem Modell. Durch die wachsende Komplexität modellbasiert entwickelter Software und die Notwendigkeit, die zugehörigen Implementierungsspezifikationen zwischen unterschiedlichen Entwicklern austauschen zu müssen, werden viele Daten nicht im Modell selbst verwaltet, sondern in einem separaten zentralen Container, dem sogenannten TargetLink Data Dictionary [6]. Jedes TargetLink-Modell wird mit einem Data Dictionary assoziiert, und im Modell werden die im Data Dictionary enthaltenen Datenelemente referenziert. Diese Zentralisierung ermöglicht es, dass verschiedene Entwickler mit konsistenten Definitionen gemeinsamer Daten wie Schnittstelleninformationen oder Kalibrierungsdaten arbeiten. Gleichzeitig stellt das Data Dictionary eine ideale Grundlage zur Anbindung von Analysewerkzeugen dar.

Neben der eigentlichen Code-Erzeugung bietet TargetLink die Möglichkeit, frühzeitig umfangreiche Simulationen in unterschiedlichen Simulationsmodi durchzuführen. Bei der Model-in-the-Loop- (MiL-) Simulation wird das Modell interpretiert, bei der Software-in-the-Loop- (SiL-) Simulation wird der generierte C-Code auf dem Host-PC ausgeführt, bei der Processor-in-the-Loop- (PiL-) Simulation wird der erzeugte Code mit einem Cross-Compiler kompiliert und auf einem Evaluierungsmodul ausgeführt. Mit den verschiedenen Simulationen lässt sich schon in frühen Entwurfsphasen prüfen, ob das Modell die funktionalen Anforderungen erfüllt. Fehler im Modell oder beispielsweise in der Skalierung können frühzeitig erkannt werden. Die PiL-Simulation ermöglicht es darüber hinaus, Messungen bezüglich Ausführungszeit und Stack-Bedarf durchzuführen.

Wie eingangs geschildert, hängt die Qualität dieser simulations- und testbasierten Verifikations- und Validierungsaktivitäten stark von der Qualität und Vollständigkeit der ausgeführten Simulation und der ausgeführten Testfälle ab. Daher sollten für sicherheitskritische Software auch sichere statische Analysatoren zum Einsatz kommen, um die Abwesenheit von Laufzeitfehlern zu beweisen und sichere obere Schranken der verwendeten Ressourcen des Zielprozessors zu bestimmen.

Statische Analyse nichtfunktionaler Software-Eigenschaften

Bei einer statischen Analyse werden Informationen über ein Software-Programm berechnet, ohne dieses tatsächlich auszuführen. Zu den statischen Analysen gehören reine Syntaxverfahren wie Code-Checker zum Prüfen von Kodierrichtlinien, unsichere semantikbasierte Verfahren und sichere semantikbasierte Verfahren. Die unsicheren semantikbasierten Verfahren betrachten die Semantik des Programms, um potenzielle Fehler zu finden, können aber nicht garantieren, dass alle Fehler gefunden werden. Bei den sicheren semantikbasierten Verfahren lässt sich mathematisch beweisen, dass keine Fehler übersehen werden. Sie beruhen auf der formalen Methode der abstrakten Interpretation [7] und haben sich innerhalb der letzten Jahre zum Stand der Technik zur Verifikation nichtfunktionaler Software-Eigenschaften entwickelt [1]. Die im Folgenden betrachteten Analysatoren gehören zur Klasse der sicheren semantikbasierten Verfahren.

Stack-Bedarf

In eingebetteten Systemen ist der Laufzeit-Stack in der Regel der einzige dynamisch verwaltete Speicherbereich. Der maximale Stack-Bedarf jeder Task muss in aller Regel zur Konfigurationszeit des Systems festgelegt werden. Wird er unterschätzt, kann es zu einem Stack-Überlauf kommen. Stack-Überläufe können schwerwiegende Fehler verursachen. Ein Beispiel ist die unbeabsichtigte Beschleunigung im 2005er Modell des Toyota Camry: Das vom zuständigen US-Gericht beauftragte Expertengutachten gibt als wahrscheinlichste Ursache einen Stacküberlauf an [8].

StackAnalyzer ist ein statischer Analysator auf Basis der abstrakten Interpretation, der sichere und präzise obere Schranken des maximalen Stack-Bedarfs von Tasks berechnet. Die Haupteingabe von StackAnalyzer ist eine ausführbare Binärdatei, also der Maschinen-Code des Zielprozessors. Die Analyse erfordert keine Code-Instrumentierung und keine Debug-Informationen und berücksichtigt präzise die Auswirkungen von Inline-Assembly und Bibliotheksfunktionen. Der Analysator berechnet, wie sich die Höhe des Laufzeit-Stack entlang der möglichen Kontrollpfade des Programms ändert, und ermittelt daraus eine sichere obere Schranke des maximalen Stack-Bedarfs. Die Analyseergebnisse werden graphisch im Aufruf- und Steuerflussgraph visualisiert und geben wichtige Hinweise zur Optimierung des Stack-Bedarfs.

Maximale Ausführungszeit

Viele Tasks in sicherheitskritischen eingebetteten Systemen haben harte Echtzeitanforderungen. Sie müssen innerhalb fest vorgegebener Zeitschranken terminieren, um ein korrektes Funktionieren des Systems zu gewährleisten. Aufgrund der Komplexität moderner Hardware- und Software-Architekturen stellt die Bestimmung der maximalen Ausführungszeit (Worst-Case Execution Time, WCET) ein schwieriges Problem dar [9]. Für einen Überblick über Methoden und Werkzeuge zur WCET-Analyse sei auf [10] verwiesen.

Der statische Analysator aiT WCET Analyzer berechnet eine sichere Approximation aller möglichen Cache- und Pipeline-Zustände des Zielprozessors an jedem Programmpunkt. Dabei wird jede mögliche Programmausführung und jedes mögliche Eingabeszenario berücksichtigt. Die genaue Kenntnis des Maschinenzustandes ist erforderlich, um die zur Ausführung der Maschineninstruktionen erforderlichen Taktzyklen präzise vorherzusagen. Sind diese bekannt, lässt sich der längste Ausführungspfad durch das Programm berechnen, aus dem sich eine sichere obere Schranke der maximalen Task-Ausführungszeit ergibt. Ebenso wie StackAnalyzer arbeitet aiT auf ausführbaren Binärdateien des jeweiligen Zielprozessors. Weder Code-Instrumentierung noch Debug-Informationen sind notwendig, die Effekte von Inline-Assembly und Bibliotheksfunktionen werden präzise analysiert. Die Analyseergebnisse werden grafisch im Aufruf- und Steuerflussgraf visualisiert und geben wichtige Hinweise zur Optimierung des Zeitverhaltens.