SAN JOSE, CA & NEW YORK & 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.
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.