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.
“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.”
SPARK Pro is a toolset based on the formally analyzable 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.”
About ISO 26262 and ASIL D
ISO 26262 is a functional safety standard for automotive systems and a derivative of the generic IEC 61508 standard for electrical/electronic/programmable electronic ("E/E/PE") systems. It defines an automotive safety lifecycle's phases and their associated activities and uses a risk-based approach to determine Automotive Safety Integrity Levels (ASILs) and the relevant requirements. An analysis of the system's functions focuses on the potential hazards in the event of a failure, and the consequences to life and property. The computed ASIL ranges from A (least critical) to D (most critical) and takes into account the estimated probability of the failure being exposed, whether the driver can ameliorate the hazard in response, and the severity of the hazard's occurrence. ASIL D represents the likely potential for severely life-threatening or fatal injury in the event of a malfunction. It thus requires the highest level of assurance that the dependent safety goals are sufficient and have been achieved.
About JTEKT
JTEKT Corporation was established in 2006 through the merger of Koyo Seiko., Ltd., a world-class bearing manufacturer, and Toyoda Machine Works, Ltd., a machine tool manufacturer excelling in world-leading technologies.
Combining the most advanced technologies and the manufacturing passion of the two companies, JTEKT is now a trusted systems supplier of automotive components, bearings and machine tools, providing customers with world-class products and technologies that result in ongoing contributions to society.