Interview mit Dr. Daniel Kästner, CTO bei AbsInt Angewandte Informatik GmbH
Zuverlässige Aussagen
Die ISO26262-Norm für sicherheitsrelevante elektrische/elektronische Systeme in Kraftfahrzeugen soll die funktionale Sicherheit eines Systems gewährleisten. AbsInt bietet Tools zur Validierung und Verifikation eingebetteter Software.
Die neue Norm ISO26262 soll die funktionale Sicherheit in Kraftfahrzeugen sicherstellen. Wie kann man den hohen Anforderungen genügen?
Dr. Daniel Kästner: Die ISO26262 fordert den Nachweis, dass alle Sicherheitsziele erfüllt sind, die zum korrekten Funktionieren eines Systems erforderlich sind. Der Nachweis kann durch unterschiedliche Techniken erbracht werden. Diese Techniken müssen eine zuverlässige Aussage ermöglichen. Mit der statischen Analyse durch Abstrakte Interpretation, einer formalen Methode, kann eine vollständige Abdeckung erreicht werden. Sehr wichtig bei der ISO26262 ist die statische Verifikation. Sie wird beispielsweise als eines der Hauptziele in der Softwaredesign- und -Implementierungsphase genannt. Mit dynamischen Test- und Messverfahren kann eine vollständige Testabdeckung auf komplexer Software in der Regel nicht mit vertretbarem Aufwand erreicht werden. Besonders schwerwiegend ist dies beim Timing-Verhalten von Echtzeitsoftware, dem Speicherverbrauch oder bei Laufzeitfehlern. Hier ist es ausgesprochen schwierig, relevante Testcases und ein sicheres Testende-Kriterium zu finden.
Sind Ausführungszeit, Speicherverbrauch oder Laufzeitfehler Teil der funktionalen
Sicherheit?
Dr. Daniel Kästner: Alle gängigen Sicherheitsstandards verlangen den Nachweis, dass es in diesen Bereichen nicht zu Fehlern kommen kann. Korrektes Zeitverhalten ist zum korrekten Funktionieren eines Echtzeitsystems funktional erforderlich. Systemabstürze, Fehlfunktionen durch Stacküberlauf oder ungültige Zeigerzugriffe sind schwerwiegende Fehler, die unbedingt ausgeschlossen werden müssen.
Können Sie bitte die Lösungen von AbsInt etwas ausführlicher beschreiben?
Dr. Daniel Kästner: AbsInt bietet Tools zur Validierung und Verifikation eingebetteter Software. Dazu gehört der aiT WCET Analyzer zur Bestimmung garantierter oberer Schranken der längstmöglichen Ausführungszeit von Echtzeittasks, der StackAnalyzer zum Nachweis der Abwesenheit von Stacküberläufen und Astrée zum Nachweis der Abwesenheit von Laufzeitfehlern. Die Tools basieren auf statischer Analyse durch Abstrakte Interpretation, die zu den formalen Verifikationsmethoden gehört. Sie können zur Zertifizierung nach allen gängigen Sicherheitsstandards eingesetzt werden.
Kann man sich darauf verlassen, dass die Tools korrekt arbeiten?
Dr. Daniel Kästner: Um das korrekte Funktionieren der Tools sicherzustellen, betrachten wir zwei Ebenen. Die Technik der Abstrakten Interpretation ermöglicht einen formalen Beweis, dass das Analyse-Design korrekt ist und beispielsweise die längstmögliche Ausführungszeit niemals unterschätzt werden kann. Die entsprechenden Beweise wurden für alle AbsInt-Tools publiziert. Auf einer zweiten Ebene lässt sich nachweisen, ob das Tool im operationalen Kontext der Benutzer korrekt arbeitet. Die meisten Sicherheitsstandards fordern hierzu eine Toolqualifizierung. Wir bieten sogenannte Qualification Support Kits an, mit denen die Qualifizierung der AbsInt-Tools automatisiert durchgeführt werden kann. Zusätzlich wird manchmal ein Nachweis über eine zum Sicherheitsstandard konforme Toolentwicklung gefordert. Hierzu bieten wir den Qualification Support Life Cycle Data Report an.
Welche Branchen sprechen Sie schwerpunktmäßig an?
Dr. Daniel Kästner: Wir sprechen alle Branchen an, in denen sicherheitskritische Softwareprogramme eingesetzt werden. Hierzu gehört die Luft- und Raumfahrtindustrie, die Automobil- und Eisenbahnindustrie, aber auch die Medizintechnik sowie Automation und Anlagenbau. Unsere Tools werden für einen breiten Bereich von Anwendungen eingesetzt, vom Flugsteuerungscomputer im Airbus A-380, bis hin zu Airbag-oder Bremssteuerungen im Automobil.
Wie kann man garantieren, dass die Elektronik bei sicherheitskritischen Aufgaben immer schnell genug reagiert, beziehungsweise wie lässt sich die Echtzeitfähigkeit gewährleisten? Welches sind die beeinflussenden Faktoren für das Zeitverhalten komplexer Systeme?
Dr. Daniel Kästner: Um die Echtzeitfähigkeit zu gewährleisten, muss nachgewiesen werden, dass die relevanten Zeitschranken stets eingehalten werden, das heißt das sogenannte worst-case Timing muss festgelegt werden. Dies erfordert zum einen die Bestimmung der längstmöglichen Ausführungszeit jeder Task auf dem zugrundeliegenden Prozessor unter der präzisen Berücksichtigung der Hardwarearchitektur wie z.B. Caches oder Pipelines. Dies wird durch den aiT WCET Analyzer erfüllt, der sichere und präzise obere Schranken der längstmöglichen Ausführungszeit liefert. Muss das End-to-End Timing auf Systemebene belegt werden, können Tools zur statischen Schedulinganalyse eingesetzt werden.
Wie lässt sich die System-Komplexität beherrschen sowie Engpässe und mögliche Reserven frühzeitig bestimmen?
Dr. Daniel Kästner: Zur Beherrschung der Systemkomplexität und gleichzeitig zur Reduktion der Entwicklungskosten ist eine durchgängige Integration in den Entwicklungsprozess unumgänglich. Dies kann durch Toolkopplungen erreicht werden. So existieren Kopplungen von AbsInt-Werkzeugen mit den modellbasierten Codegeneratoren SCADE, TargetLink und ASCET. Bei der Timing-Analyse können in frühen Entwicklungsphasen virtuelle Prozessormodelle als Grundlage der statischen worst-case Berechnung verwendet werden, in späten Phasen die tatsächlich eingesetzte Hardware. Auch Kopplungen zwischen unterschiedlichen Timingwerkzeugen sind wichtig. So sind AbsInts aiT WCET-Analyzer zur Berechnung der worst-case Tasklaufzeiten, Symtavisions SymTA/S zur Berechnung der worst-case Schedules und Gliwas T1 zur tracebasierten Laufzeitmessung miteinander gekoppelt. Auch eine Kopplung zwischen modellbasiertem Testen und statischer Analyse ist sinnvoll, realisiert z.B. durch eine Kopplung der AbsInt-Werkzeuge mit dem modellbasierten EmbeddedTester von BTC-ES.
