JTEKT has adopted AdaCore’s SPARK Pro tool suite

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 rigour. Using SPARK Pro, developers can prove the absence of certain categories of vulnerabilities (such as buffer overflow, division by zero, and references to uninitialised 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,” added 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.”