Modellbasierte Enwicklung Schwere Fehler sicher ausschließen

Bei der modellbasierten Entwicklung wird die Software auf einer hohen Abstraktionsebene, dem Modell, entwickelt, während die Implementierung in Form von C-Code automatisch aus dem Modell generiert wird. Die Tool-Hersteller dSpace und AbsInt haben den Serien-Code-Generator TargetLink mit den statischen Analysewerkzeugen aiT, StackAnalyzer und Astrée gekoppelt, wodurch viele Vorteile entstehen.

In einem modellbasierten Entwicklungsprozess wird die Software grafisch auf einer hohen Abstraktionsebene entwickelt, in der Regel durch Zustandsautomaten und Datenflussdiagramme. Das ausführbare Modell ist damit zugleich Software-Spezifikation des Systems. Die Implementierung wird von Code-Generatoren automatisch aus dem abstrakten Modell generiert, in der Regel in Form von C-Code. Zu den Vorteilen gehört, dass sich Entwickler auf die eigentlichen Funktionen konzentrieren können, ohne sich um Implementierungsdetails kümmern zu müssen, und dass Modelländerungen automatisch zu entsprechenden Code-Änderungen führen. Damit reduziert sich zum einen der Entwicklungsaufwand, zum anderen erhöht sich die Systemsicherheit.

Der hohe Abstraktionsgrad hat jedoch auch Nachteile: Einige wichtige Systemeigenschaften sind für Benutzer nicht mehr unmittelbar sichtbar. Hierzu zählen Laufzeitfehler im generierten C-Code durch fehlerhafte Modellspezifikationen, der Stack-Bedarf des generierten Maschinencodes und das Zeitverhalten des Maschinencodes auf dem eingebetteten Zielprozessor. Das kann dazu führen, dass schwerwiegende Fehler erst in späten Entwicklungsphasen entdeckt werden. Verletzungen von Echtzeitanforderungen, Stack-Überläufe und Laufzeitfehler können zu fehlerhaften Systemreaktionen bis hin zum kompletten Systemabsturz führen. Der Nachweis, dass diese sogenannten nichtfunktionalen Fehler nicht auftreten können, gehört zu den Verifikationszielen aller aktuellen Sicherheitsnormen, beispielsweise der ISO 26262, DO-178B/DO-178C oder IEC 61508.

Nichtfunktionale Software-Eigenschaften, wie Ausführungszeit, Stack-Bedarf und das Auftreten von Laufzeitfehlern, sind durch Test- und Messverfahren nur schwer zu erfassen: Spezifische Testfälle, beispielsweise zur Stimulation der maximalen Ausführungszeit, sind in der Regel nicht vorhanden, ein sicheres Testendekriterium unbekannt. Basieren Messungen auf Code-Instrumentierung, muss im sicherheitskritischen Bereich ausgeschlossen werden, dass die Instrumentierung das Ergebnis verfälscht, was insbesondere bei Laufzeitmessungen ein ungelöstes Problem darstellt. In aller Regel ist der erforderliche Testaufwand hoch und die Testergebnisse sind unvollständig.

Formale Verifikationsverfahren schaffen Abhilfe, weil sie die Abwesenheit von Fehlern mathematisch beweisen können. Ein solches Verfahren ist die abstrakte Interpretation, die eine formale Methode zur Durchführung von statischen Analysen darstellt. Sie liefert sichere Ergebnisse, die für jede mögliche Programmausführung und für jedes mögliche Eingabeszenario gelten. Aufgrund ihrer guten Skalierbarkeit ist sie für große Software-Projekte einsetzbar. Statische Analysatoren auf Basis der abstrakten Interpretation, die obere Schranken der maximalen Ausführungszeit berechnen und die Abwesenheit von Stack-Überläufen sowie Laufzeitfehlern garantieren können, sind heutzutage im Industrieeinsatz verbreitet. Sie können als Stand der Technik zur Verifikation nichtfunktionaler Software-Eigenschaften angesehen werden [1].

Die Kopplung der statischen Analysatoren aiT [2], StackAnalyzer [3] und Astrée [4] mit dem Serien-Code-Generator TargetLink ermöglicht die automatische Berechnung sicherer oberer Schranken der maximalen Ausführungszeit und des maximalen Stack-Bedarfs sowie den Nachweis, dass keine Laufzeitfehler vorhanden sind. Darüber hinaus werden Fehler frühzeitig im Entwicklungsprozess entdeckt, wodurch teure Integrationsprobleme in späten Projektphasen vermieden werden können. Entdeckte Fehler lassen sich auf Modellebene zurückverfolgen, die enge Kopplung der Werkzeuge ermöglicht eine deutliche Verbesserung der Entwicklungseffizienz.