Sicherheitskonzepte aus Luft- und Raumfahrt landen in der Automobilindustrie

Inhaltsverzeichnis

In der Luft- und Raumfahrtindustrie spielt die Software bei der Gewährleistung der Sicherheit der Verkehrsflugzeuge schon lange eine kritische Rolle. Sie ist ein integraler Bestandteil von Systemen wie Motorsteuerung, Flugsteuerung und Navigation. Aufgrund dieser Verbindung wurde im Laufe der Jahre eine verbindliche Reihe von Sicherheitsstandards und Prozessen – zum Beispiel DO-178 B/C – entwickelt, um die Möglichkeit von Softwarefehlern zu minimieren, die zu einer Störung der Flugsicherheit führen können.

Durch neue Herausforderungen in der Automobilindustrie werden die existierenden Sicherheitsstandards und -prozesse, zum Beispiel ISO 26262, immer relevanter. Systeme wie Advanced Driver Assistance Systems (ADAS) werden anspruchsvoller, und die Sicherheit eines Automobils ist zunehmend vom korrekten und sicheren Betrieb seiner softwarebasierten Steuerungssysteme abhängig ist.

In der Vergangenheit waren die auf Luftfahrt und auf Automobile ausgerichteten Märkte für Entwicklungswerkzeuge weitgehend getrennt – mit unterschiedlichen Mikroprozessoren, verschiedenen Betriebssystemen und unterschiedlichen Werkzeugketten. In jüngster Zeit ist jedoch festzustellen, dass einige der modellbasierten Entwicklungsansätze zur Codeerzeugung, die in der Automobilindustrie beliebt sind, auch in der Luft- und Raumfahrtindustrie auftauchen, während sich die strengen Sicherheitsanforderungen und die formalen Prozesse in Luft- und Raumfahrt zunehmend stärker in der Automobilindustrie verbreiten.

Demnach scheint es Bedarf zu geben, die Denkweise der Luft- und Raumfahrtindustrie hinsichtlich Softwaresicherheit in die modellbasierte Entwicklungswelt zu bringen. Man traut modellbasierten Codegeneratoren für Sprachen wie Simulink zu, Code zu erzeugen, der höchsten Ansprüchen bei der Sicherheit gerecht werden kann.

Der vorliegende Artikel untersucht die Verwendung formaler Prozesse als Teil der Überprüfung sicherheitskritischer modellbasierter Systeme sowohl in der Luft- und Raumfahrtindustrie, in der man bestehende formale Prozesse auf modellbasierte Systeme anwendet, als auch in der Autoindustrie, in der formale Verifizierungsprozesse noch in einem früheren Stadium sind. Er beschreibt die Entwicklung und formale Verifikation eines "vertrauenswürdigen" Auto-Code-Generators, der Simulink-/Stateflow-Modelle in MISRA-C oder SPARK, einer auf Ada basierenden Programmiersprache, übersetzt.

Was passiert in Luft- und Raumfahrt?

In der Luft- und Raumfahrtindustrie stellt die Normenreihe DO-178 seit vielen Jahren ein praxisorientiertes Verfahren zur Entwicklung sicherheitskritischer Software zur Verfügung. Die jüngste, 2012 veröffentlichte Version (DO-178C) erweitert sie um Ergänzungen. Zwei sind besonders relevant: diejenige, die sich auf die modellbasierte Entwicklung (DO-331) konzentriert, und die mit dem Fokus auf der Nutzung der formalen Methoden (DO-333). In Verbindung mit DO-178C definieren diese Dokumente einen Prozess, der mit High-Level-Anforderungen beginnt und sie zu Low-Level-Anforderungen verfeinert, die typischerweise in einem Modell der modellbasierten Entwicklung enthalten sind.

Dieser Prozess sieht eine systematische anforderungsorientierte Verifizierung vor, beginnend mit der Überprüfung der Konsistenz der Low-Level- mit den High-Level-Anforderungen. Er überprüft außerdem, ob Tests und/oder formale Beweise, die auf der Modellebene und auf dem endgültigen System durchgeführt werden, alle High- und Low-Level-Anforderungen abdecken.

Die genauen Aktivitäten bei der Überprüfung einer Implementierung auf das Erfüllen sämtlicher High- und Low-Level-Anforderungen können in Abhängigkeit von den hierfür eingesetzten Werkzeugen und Methoden stark variieren. Wenn ein Tool für ein bestimmtes Projekt qualifiziert ist, also die Ausgabe des Werkzeugs für bestimmte Standards – sogenannte Tool Qualification Levels in DO-178C – verifiziert wurde, lassen sich einige normalerweise manuell durchgeführte Aktivitäten stattdessen auf das Werkzeug übertragen oder weglassen. Zum Beispiel kann man eine separate manuelle Überprüfung des erzeugten Quellcodes vereinfachen oder weglassen, wenn das Input-Modell ausreichend verifiziert ist und ein modellbasierter Codegenerator den Quellcode generiert und dieses Werkzeug für die DO-178C Tool Qualification Level 1 (TQL-1) qualifiziert wurde. Es lässt sich dann Quellcode erzeugen, der die Semantik des Originalmodells bewahrt und einem Coding-Standard entspricht.

Die Verwendung formaler Methoden kann beeinflussen, welche Verifizierungsaktivitäten erforderlich sind. Früher wurde ihr Einsatz nicht direkt durch DO-178 adressiert. Aber seit DO-178C wird besonderes Augenmerk auf ihre Verwendung gelegt; das ist in DO-333 dargestellt. Zum Beispiel können formalen Methoden, die beweisen, dass einige oder alle Softwaresysteme ihre Anforderungen unter allen anwendbaren Eingabebedingungen erfüllen, die Menge der erforderlichen konventionellen Tests reduzieren.

Und die Autoindustrie?

Die Automobilindustrie hat begonnen, ihren eigenen Prozessstandard einzuführen, nämlich ISO 26262 ("Road vehicles – Functional safety"), der zum Teil auf der allgemeineren IEC 61508 zur funktionalen Sicherheit basiert. Obwohl er ganz anders als DO-178 strukturiert ist, sind die Ziele dennoch konsistent, und die Erfahrungen der Luft- und Raumfahrtindustrie können hilfreich sein, wenn sich die Automobilindustrie mehr auf den Softwareentwicklungsprozess konzentriert. So entsteht eine der größten Herausforderungen durch die zunehmende Zahl verschiedener Subsysteme, die gleichzeitig im Automobil arbeiten und die potenziell das gleiche Netzwerk, den gleichen Bus und sogar die gleiche Verarbeitungs- und Speicherressourcen teilen. In ISO 26262 müssen Entwickler die "Freedom from Interference" (FFI) zwischen Subsystemen darlegen, die miteinander kommunizieren oder gemeinsame Ressourcen teilen.