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