High-Reliability Vehicle Component Research Project

TOYOTA ITC

TOYOTA InfoTechnology Center (ITC) Japan selected the SPARK language and SPARK Pro toolset for a research project to develop a vehicle component implementation that can be proven to be free of run-time errors.

Select Language

TOYOTA ITC Japan Selects SPARK Pro Language and Toolset for High-Reliability Research Project

SAN JOSE, Calif., NEW YORK and PARIS, April 23, 2013 – Design West Conference –  AdaCore and Altran today announced TOYOTA InfoTechnology Center (ITC) Japan’s selection of the SPARK language and SPARK Pro toolset for a high-reliability software research project. The goal of the project is to show that software requirements can be transformed into an implementation that can be proven to be free of run-time errors. This will have the key advantage of providing ultra-low-defect software for higher reliability in a vehicle component. An added benefit is the reduction of development and maintenance effort, since the formal approach being used can give mathematical assurance to a variety of correctness properties, reducing the need for certain types of testing and eliminating the need for post-deployment corrections.

The research project is taking a proven design and generating a fully assured code implementation, starting from a single vehicle system component. The aim is to use SPARK Pro technology to prove that the software can be produced free of run-time exceptions under all operating conditions, as a first step to composing larger ultra-low-defect systems. Alternative approaches using conventional software development methods have fundamental limitations. Testing can only provide evidence for a limited set of conditions, and static analysis performed on existing code to check for vulnerabilities, or other errors, does not address the underlying problem of preventing the errors in the first place. Using the SPARK language, toolset and methods solves this basic issue and will provide a clear competitive advantage for this component.

About SPARK
SPARK is a programming language that supports the precise specification of design or requirements in source code using a notation for formal contracts, including pre-conditions and post-conditions for subprograms, and inter-module information flow dependencies. The SPARK Pro toolset can then be used to verify that the software correctly implements the design, or meets its requirements, by verifying that the source code logic complies with the specified contracts. 

SPARK can be used both to precisely express system requirements and to define an executable implementation, which can be formally shown to meet those requirements. Correctness can thus be demonstrated from the start, and maintained incrementally as the system evolves. This is a vastly different approach, and much more reliable, than developing a system and then using tests or static analysis to reduce the number of errors introduced in earlier life-cycle phases.

About SPARK Pro
SPARK Pro, a product jointly developed by Altran and AdaCore, provides a state-of-the-art language and toolset for engineering high-assurance software. It combines Altran’s SPARK language and verification tools with AdaCore’s GNAT Programming Studio (GPS) and GNATbench Integrated Development Environments. There are SPARK versions based on Ada 83, Ada 95, and Ada 2005, so all standard Ada compilers and tools work out-of-the-box with SPARK.

The SPARK Pro language and toolset is specifically designed for developing applications where correct operation is vital for safety or security. It offers static verification that is unrivalled in terms of its soundness (no “false negatives”), low false-alarm rate, depth and efficiency. The toolset generates evidence for correctness, including proofs of the absence of run-time errors that can be used to meet the requirements of safety and security certification schemes, such as ISO 26262, DO-178B, DO-178C and the Common Criteria. SPARK Pro is especially applicable in the context of the Formal Methods supplement to DO-178C.

About TOYOTA InfoTechnology Center Co., Ltd.
TOYOTA InfoTechnology Center Co., Ltd. provides cutting-edge technology and creates value with superior intelligence and greater innovation throughout the IT business related to automobiles. TOYOTA ITC as a whole has as its objective the development of advanced, world-class information technologies to meet market needs. This includes the research, development and evaluation of technologies, hardware and software research, analysis and planning of market and business models, and the management of intellectual property rights.

TOYOTA ITC has North America headquarters in Mountain View, CA and the main office in Tokyo, Japan. www.toyota-itc.com


About Altran
Altran is a leading-edge engineering consultancy that enables UK business to work smarter – from making critical national infrastructure work safely, to bringing products and services to market quickly for the automotive, aerospace and life sciences industries. Altran has in-depth expertise in embedded and critical systems, product lifecycle management and engineering services. We have a global network of over 20,000 employees operating throughout more than 20 countries, and 500 major clients. Altran leads the world in specific areas of advanced systems engineering and innovation such as ultra-low defect software engineering, Human Machine Interface (HMI), safety engineering for complex or novel systems and tools/methods for systems engineering. www.altran.co.uk

About AdaCore
Founded in 1994, AdaCore is the leading provider of commercial software solutions for Ada, a state-of-the-art programming language designed for large, long-lived applications where safety, security, and reliability are critical. AdaCore's flagship product is the GNAT Pro development environment, which comes with expert on-line support and is available on more platforms than any other Ada technology. AdaCore has an extensive world-wide customer base; see http://www.adacore.com/home/company/customers/ for further information.

Ada and GNAT Pro see a growing usage in high-integrity and safety-certified applications, including commercial aircraft avionics, military systems, air traffic management/control, railway systems and medical devices, and in security-sensitive domains such as financial services.

AdaCore has North American headquarters in New York and European headquarters in Paris. www.adacore.com

Press Contacts

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

Jessie Glockner
Rainier Communications (for AdaCore)
Tel: 508-475-0025 x140
adacore@rainierco.com
http://twitter.com/JessieGlockner

Owen Burdekin
Altran
Tel: +44 (0) 203 117 0714
owen.burdekin@altran.com

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