Toyota verwendet SPARK Pro in einem Forschungsprojekt für Ultra-Low-Defect-Software

Das Toyota InfoTechnology Center (ITC) in Japan hat die Programmiersprache SPARK und das SPARK Pro Toolset für den Einsatz in einem Forschungsprojekt für die Entwicklung von Software höchster Zuverlässigkeit ausgewählt. Das Ziel des Projektes ist es, zu zeigen, dass Software-Requirements nachweislich frei von Laufzeitfehlern in eine Implementierung überführt werden können. Dies bietet entscheidende Vorteile der Bereitstellung von Ultra-Low-Defect-Software für erhöhte Zuverlässigkeit von Fahrzeug-Komponenten. Ein weiterer Vorteil ist die Reduzierung des Entwicklungs- und Wartungsaufwands, da der verwendete formale Ansatz eine Reihe von erwünschten Eigenschaften mathematisch beweisen kann. Bestimmte Testaktivitäten werden dadurch überflüssig, nachträgliche Korrekturen seltener.

Das Forschungsprojekt geht vom bewährten Design einer einzigen Fahrzeug-System-Komponente aus und erstellt eine vollständig sichere Code-Implementierung. Mit der SPARK-Pro-Technologie kann eine Software hergestellt werden, die unter allen Betriebsbedingungen ohne Laufzeitfehler läuft. Dies stellt einen ersten Schritt für die Erstellung großer Ultra-Low-Defect-Systeme dar. Alternative Ansätze mit herkömmlichen Methoden der Softwareentwicklung stoßen hier auf fundamentale Grenzen, denn das Testen kann immer nur für eine begrenzte Anzahl von Bedingungen den Nachweis der Fehlerfreiheit erbringen, und statische Analysen von vorhandenem Code hinsichtlich Schwachstellen oder Fehler können immer nur auf bereits vorhandene Fehler reagieren, sie aber nicht von vornherein ausschließen. Mit der Programmiersprache SPARK, dem Toolset und den dazugehörigen Methoden wird dieses grundlegende Problem gelöst und ein klarer Wettbewerbsvorteil für diese Komponente erreicht.

Ãœber SPARK

SPARK ist ein Subset der Programmiersprache Ada, das die genaue Spezifikation des Designs oder Anforderungen im Quellcode mit einer formalen Notation für Contracts unterstützt, einschließlich Pre- und Post-Bedingungen für Funktionen und Abhängigkeiten im Informationsaustausch zwischen Modulen. Mit dem SPARK Pro Toolset können Anwender sicherstellen, dass die Software das Design richtig implementiert beziehungsweise seinen Anforderungen entspricht, indem überprüft wird, ob die Logik des Quellcodes den spezifizierten Contracts entspricht.

SPARK kann sowohl Systemanforderungen präzise ausdrücken als auch eine ausführbare Implementierung definieren, die formal nachweisen kann, dass sie die jeweiligen Anforderungen erfüllt. Formale Richtigkeit (Correctness) kann somit von Anfang an gezeigt werden, sie lässt sich dann schrittweise mit der Weiterentwicklung des Systems anpassen. Dies ist ein völlig neuer Ansatz, der sehr viel zuverlässiger ist als die herkömmliche Entwicklung eines Systems mit anschließenden Tests oder statischen Analysen zur Reduzierung von Fehlern, die in früheren Phasen entstanden sind.

Ãœber SPARK Pro

SPARK Pro wurde gemeinsam von Altran und AdaCore entwickelt. Es bietet eine State-of-the-Art-Sprache und ein Engineering-Toolset für hochsicherheitskritische Software. SPARK Pro verbindet die Sprache und Verifikations-Tools von Altrans SPARK mit dem GNAT Programming Studio (GPS) und GNATbench Integrated Development Environments von AdaCore. Verfügbar sind SPARK-Versionen auf Basis von Ada 83, Ada 95 und Ada 2005, so dass alle gängigen Ada-Compiler und -Tools Out-of-the-Box mit SPARK arbeiten können.

Die Sprache SPARK Pro und das Toolset sind speziell für die Entwicklung von Anwendungen konzipiert, bei denen ein fehlerloser Betrieb von entscheidender Bedeutung für die Sicherheit ist. SPARK Pro bietet statische Ãœberprüfung, die hinsichtlich ihrer Solidität konkurrenzlos ist – beispielsweise keine „false negatives“ –, eine niedrige Fehler-Alarm-Rate und Effizienz. Das Toolset garantiert die Korrektheit sowie die Abwesenheit von Laufzeitfehlern und kann verwendet werden, um die Anforderungen von Sicherheitszertifizierungen wie ISO 26262, DO-178B, DO-178C und der Common Criteria (CC) zu erfüllen. SPARK Pro lässt sich insbesondere im Zusammenhang mit dem Anhang „Formal Methods“ zu DO-178C verwenden.

Ãœber Toyota InfoTechnology Center

Toyota InfoTechnology Center Co. bietet Spitzentechnologie mit überlegenem Know-how und Innovationskraft für Kraftfahrzeug-IT. Toyota ITC befasst sich mit der Entwicklung von fortgeschrittenen, anspruchsvollen Informationstechnologien, um den Anforderungen des Marktes gerecht zu werden. Dazu zählen Forschung, Entwicklung und Evaluierung von Technologien, Hardware- und Software-Studien, die Analyse und Planung von Markt- und Geschäftsmodellen sowie das Management von Rechten an geistigem Eigentum. Der Hauptsitz von Toyota ITC ist in Tokio, in Mountain View, Kalifornien, besteht eine Niederlassung; Website: www.toyota-itc.com

Ãœber Altran

Altran ist globaler Marktführer in Innovationen und High-Tech Consulting. Altran berät seit über 30 Jahren Marktführer aus den Bereichen Automobilbau, Energie, Finanzen, Healthcare, Luft- und Raumfahrt, Schienen- und Transportwesen sowie Telekommunikation.

Altran deckt mit seinen Beratungsangeboten sämtliche Stufen der Projektentwicklung ab und kann dabei auf umfangreiches Technologie-Know-how aus vier Solutions zurückgreifen: Innovative Technologies, Sustainable Products, Sustainable Concepts sowie Sustainability Enterprise Performance.

Diese Presseinformation kann auch unter www.pr-com.de abgerufen werden.

Weitere Informationen unter:
http://www.adacore.com