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

Paris, 30. April 2013 – Das Zentrum für Informationstechnologie von Toyota verwendet die auf Ada basierende Programmiersprache SPARK und das SPARK Pro Toolset für die Entwicklung sicher-heitskritischer Lösungen in der Automobilherstellung. SPARK und das von Altran und AdaCore entwickelte SPARK Pro bieten Toyota neue Möglichkeiten bei der Konzeption und Realisierung von Ultra-Low-Defect-Software.

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

Das Forschungsprojekt geht vom bewährten Design einer einzigen Fahr-zeug-System-Komponente aus und erstellt eine vollständig sichere Code-Implementierung. Mit der SPARK-Pro-Tech¬nologie kann Software hergestellt werden, die unter allen Betriebsbedingungen ohne Laufzeit-fehler läuft. Dies stellt einen ersten Schritt für die Erstellung großer Ultra-Low-Defect-Systeme dar. Alternative Ansätze mit herkömm¬lichen Me-thoden der Softwareentwicklung stoßen hier auf fundamentale Grenzen, denn das Testen kann immer nur für eine begrenzte Anzahl von Bedin-gungen den Nachweis der Fehlerfreiheit erbringen, und statische Analy-sen 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 die-se 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 Informationsaus-tausch zwischen Modulen. Mit dem SPARK Pro Toolset können Anwen-der sicherstellen, dass die Software das Design richtig implementiert be-ziehungsweise 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 nachwei-sen kann, dass sie die jeweiligen Anforderungen erfüllt. Formale Rich-tigkeit (Correctness) kann somit von Anfang an gezeigt werden, sie lässt sich dann schrittweise mit der Weiterentwicklung des Systems anpas-sen. 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 Environ-ments 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 Entwick-lung von Anwendungen konzipiert, bei denen ein fehlerloser Betrieb von entscheidender Bedeutung für die Sicherheit ist. SPARK Pro bietet stati-sche Überprüfung, die hinsichtlich ihrer Solidität konkurrenzlos ist – bei-spielsweise keine "false negatives" –, eine niedrige Fehler-Alarm-Rate und Effizienz. Das Toolset garantiert die Korrektheit sowie die Abwe-senheit von Laufzeitfehlern und kann verwendet werden, um die Anfor-derungen von Sicherheitszertifizierungen wie ISO 26262, DO-178B, DO-178C und den 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 überle-genem 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 Pla-nung von Markt- und Geschäftsmodellen sowie das Management von Rechten an geistigem Eigentum. Der Hauptsitz von Toyota ITC ist in To-kio, in Mountain View, Kalifornien, besteht eine Niederlassung; Website: www.toyota-itc.com

Über Altran
Altran ist globaler Marktführer in Innovationen und High-Tech Consul-ting. Altran berät seit über 30 Jahren Marktführer aus den Bereichen Au-tomobilbau, Energie, Finanzen, Healthcare, Luft- und Raumfahrt, Schie-nen- und Transportwesen sowie Telekommunikation.

Altran deckt mit seinen Beratungsangeboten sämtliche Stufen der Pro-jektentwicklung ab und kann dabei auf umfangreiches Technologie-Know-how aus vier Solutions zurückgreifen: Innovative Technologies, Sustainable Products, Sustainable Concepts sowie Sustainability Enter-prise Performance.
Diese Presseinformation kann unter
www.pr-com.de abgerufen werden.

Über AdaCore
AdaCore wurde 1994 gegründet und ist der führende Anbieter von kommerziellen Softwarelösun-gen für Ada, einer modernen Programmiersprache für große, langlebige Anwendungen, bei denen Sicherheit und Verlässlichkeit kritisch sind. Das wichtigste Produkt des Unternehmens ist die Ent-wicklungsumgebung GNAT Pro, die Online-Support bietet und auf mehr Plattformen als jede andere Ada-Technologie verfügbar ist. AdaCore hat eine große, weltweite Kundenbasis; bitte finden Sie weitere Informationen auf der folgenden Seite: http://www.adacore.com/home/company/customers/

Sowohl Ada als auch GNAT Pro werden immer häufiger im High-integrity-Bereich und für sicher-heitszertifizierte Anwendungen eingesetzt, so vor allem in sicherheitssensiblen Bereichen wie der Luftfahrt, militärischen Systemen, der Flugverkehrskontrolle, dem Flugverkehrsmanagement, dem Eisenbahnbereich, der medizinischen Produkte oder dem Finanzsektor.
AdaCore hat seinen nordamerikanischen Hauptsitz in New York, der europäische Hauptsitz ist in Paris. Weitere Informationen unter www.adacore.com

Pressekontakte:
AdaCore 
Jamie Ayre
press@AdaCore.com
www.AdaCore.com
http://twitter.com/AdaCoreCompany

PR-COM GmbH
www.pr-com.de