(openPR) Paris, 23. Juni 2020 – Formale Methoden und die Toolsuite SPARK Pro von AdaCore unterstützen den Automobilzulieferer JTEKT bei der Reduzierung der Entwicklungs- und Verifikationskosten für sichere autonome Fahrsysteme.
JTEKT, ein internationaler Hersteller von elektrischen Servolenkungssystemen für Kraftfahrzeuge mit Hauptsitz in Japan, setzt die AdaCore SPARK Pro-Toolsuite und den GNAT Pro Common Code Generator (CCG) ein, um die Entwicklung von Software für sicherheitskritische Servolenkungssysteme zu unterstützen. Mit Hilfe des Mentorenprogramms von AdaCore machte sich JTEKT schnell mit der SPARK-Technologie vertraut. Der Zulieferer hat gezeigt, wie das SPARK-Ada-Sprach-Subset und formale Methoden Unit-Tests und die Verifizierung des C-Codes des Systems vereinfachen. Gleichzeitig wurde die Fehlerfreiheit des Codes sichergestellt. Mit dem CCG, der SPARK in C-Quellcode kompiliert, kann JTEKT alle Möglichkeiten von SPARK nutzen, um kritische sicherheitsrelevante Eigenschaften zu überprüfen, während die bestehende C-basierte Infrastruktur weiterhin verwendet wird.
Die Software zur Steuerung der Servolenkung in einem Lenksystem wird benötigt, um andere autonome Fahrsysteme wie den Spurhalteassistenten zu steuern und sicher mit ihnen zu kommunizieren. Diese Systeme werden wegen des Risikos schwerwiegender lebensbedrohlicher oder tödlicher Unfälle durch eine Fehlfunktion als Automotive Safety Integrity Level (ASIL) D klassifiziert – die am höchsten eingestufte Gefahr (Verletzungsrisiko), die in der Norm ISO 26262 definiert ist.
SPARK Pro ist ein Toolset, das auf dem formal analysierbaren SPARK-Subset der Ada-Sprache basiert und Entwicklern ermöglicht, Eigenschaften des Quellcodes mit mathematischer Strenge zu bestimmen. Mit SPARK Pro können Entwickler die Abwesenheit bestimmter Schwachstellen-Kategorien wie Buffer Overflow, Teilung durch Null und Referenzen auf nicht initialisierte Variablen nachweisen und auch benutzerdefinierte, funktionale Assertionen überprüfen. CCG ermöglicht bei Projekten das Cross-Kompilieren von SPARK-Anwendungen für jede Zielhardware, die einen C-Compiler bereitstellt, einschließlich Zielhardware, die keine serienmäßige Ada-Unterstützung bietet. Sowohl SPARK Pro als auch CCG sind nach den Standards für funktionale Sicherheit ISO 26262 und IEC 61508 zertifiziert.
„Wir erforschen seit einigen Jahren formale Methoden, um den aktuellen Anforderungen an Software aus der Automobilindustrie gerecht zu werden, das heißt hohe Zuverlässigkeit mit einem angemessenem Sicherheitsverständnis. Wir haben uns deswegen sehr für SPARK interessiert“, erklärt Shinya Yoneki, Manager Advanced System Development bei JTEKT. „Wir gehen davon aus, dass die Tools von AdaCore uns ermöglichen, beim Überprüfen sicherheitskritischer Software Kosten zu sparen – und dass sie uns schließlich dabei unterstützen, sicheren Code serienmäßig zu erstellen.“
„Der Einsatz formaler Methoden, um die Korrektheit des aus SPARK generierten C-Codes sicher zustellen, ist auf dem neuesten Stand der Automobilsicherheitstechnik“, erläutert Juan Carlos Bernedo, Head of Japan Sales bei AdaCore. „SPARK erweist sich schnell als eine kostengünstigen Lösung für Softwareentwickler, die die höchsten Sicherheitsstandards der Automobilindustrie erfüllen müssen. Die Erfahrung von JTEKT zeigt, dass auch ein C-orientierter Softwareanbieter die SPARK-Sprache und das SPARK-Toolset erfolgreich einführen kann“.
Über ISO 26262 und ASIL
ISO 26262 ist eine Norm für funktionale Sicherheit in Kraftfahrzeugen und eine Ableitung der allgemeinen Norm IEC 61508 für elektrische/elektronische/programmierbare elektronische Systeme („E/E/PE“). Sie definiert die Phasen des Safety Life Cycle von Fahrzeugen und die damit verbundenen Maßnahmen und legt auf Grundlage eines risikobasierten Ansatzes die Automotive Safety Integrity Levels (ASILs) und die entsprechenden Vorgaben fest. Eine Analyse der System-Funktionen konzentriert sich auf die potenziellen Gefahren im Falle eines Ausfalls und die Folgen für Leben und Eigentum. Der berechnete ASIL reicht von A (am wenigsten kritisch) bis D (am kritischsten) und berücksichtigt die geschätzte Wahrscheinlichkeit, mit der der Ausfall auftritt, die Frage, ob der Fahrer die Gefahr mit einer Gegenmaßnahme verringern kann, sowie das Ausmaß des Auftretens. ASIL D stellt das wahrscheinliche Risiko einer schwerwiegenden, lebensbedrohlichen oder tödlichen Verletzung im Falle einer Störung dar. Es erfordert daher ein Höchstmaß an Sicherheit, dass die erforderlichen Sicherheitsvorgaben ausreichend sind und erreicht weden.
Über JTEKT
JTEKT entstand 2006 durch die Fusion von Koyo Seiko, einem Hersteller von Lagern, und Toyoda Machine Works. Einem weltweit führenden Werkzeugmaschinenhersteller. Durch die Kombination fortschrittlicher Technologien und der Leidenschaft beider Unternehmen ist JTEKT heute ein zuverlässiger Systemlieferant von Automobilkomponenten, Lagern und Werkzeugmaschinen.
Diese Presseinformation und das Bildmaterial in höherer Auflösung können unter www.pr-com.de/adacore abgerufen werden.
