SPARK Pro software chosen for JTEKT safety-critical Electric Power Steering System
AdaCore today announced that JTEKT, an international automotive electric power steering system manufacturing company headquartered in Japan, has adopted AdaCore’s SPARK Pro toolsuite and the GNAT Pro Common Code Generator (CCG) to aid in the development of safety-critical power steering system software.
Taking advantage of AdaCore’s Mentorship Program to help bring them up to speed quickly with the SPARK technology, JTEKT demonstrated how to leverage the SPARK Ada language subset and formal methods to facilitate unit testing and verification of the system’s C code to ensure that it was correct. The usage of CCG, which compiles SPARK into C source code, enabled JTEKT to reap the full benefits of SPARK to prove critical safety properties while still using their existing C-based infrastructure.
The power steering control software of a steering system needs to control and safely handshake with other autonomous driving systems, such as lane keep assist. Due to the potential for severely life-threatening or fatal injury in the event of a malfunction, these systems are classified as Automotive Safety Integrity Level (ASIL) D – the most stringent classification of initial hazard (injury risk) defined within the ISO 26262 standard.
SPARK Pro is a toolset based on the formally analysable SPARK subset of the Ada language, allowing developers to guarantee properties of source code with mathematics-based rigor. Using SPARK Pro, developers can prove the absence of certain categories of vulnerabilities (such as buffer overflow, division by zero, and references to uninitialized variables) and also prove custom functional assertions. CCG allows projects to cross-compile SPARK applications to any hardware target that provides a C compiler, including targets that do not come with off-the-shelf Ada support. Both SPARK Pro and CCG are qualified under the ISO 26262 and IEC 61508 functional safety standards.
“We have been studying formal methods for a few years now to deal with current demands on software from the automotive industry, i.e., high reliability with a good safety rationale, and we were delighted to find out about SPARK,” said Shinya Yoneki, Manager, Advanced System Development at JTEKT, Japan. “We believe that AdaCore’s tools will enable us to save money on testing of safety-critical software and will eventually help us to mass-produce safe, secure code.”
“Using formal methods to ensure the correctness of C code generated from SPARK is at the cutting edge of automotive safety/security technology,” said Juan Carlos Bernedo, AdaCore Head of Japan Sales. “SPARK is fast becoming a cost-effective solution of choice for software developers needing to meet the automotive industry’s highest level of assurance standards, and JTEKT’s experience shows how a C-centered software provider can successfully introduce and exploit the SPARK language and toolset.”
