The Toyota Info Technology Center (ITC) in Japan has selected the SPARK programming language and the SPARK Pro toolset within the scope of a research project. The goal of the project is to prove that software requirements can be transferred into an implementation verifiably error-free. This offers decisive benefits in the supply of ultra low defect software for automotive applications. Another advantage is that it enables lower development and maintenance efforts since the formal approach used can yield a mathematically correct prove of desired properties. Thus, certain test activities become redundant, subsequent corrections are required less frequently.
Toyota's research project emanates from the proven of a single vehicle component and generates an entirely safe code implementation. The SPARK Pro technology enables designers to create a software that runs under all operating conditions with zero runtime errors. This is regarded as a first step towards the implementation of large ultra low defect systems. In such a context, conventional methods of software development hit their limits since testing can only prove correctness for a limited number of constraints, and static analysis of existing code as an alternative approach can only react on errors; it cannot rule out the emergence of errors in new code. In contrast, SPARK and SPARK Pro can guarantee correctness and the absence if runtime errors. For these reasons, this tool is frequently used in projects which have to meet the requirements of safety standards such as ISO 26262, DO-178B, DO-178C and the Common Criteria (CC).