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.
This press release features multimedia. View the full release here: https://www.businesswire.com/news/home/20200623005008/en/
(Photo: Business Wire)
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 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.
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.
Founded in 1994, AdaCore supplies software development and verification tools for mission-critical, safety-critical and security-critical systems. Four flagship products highlight the company’s offerings:
● The GNAT Pro development environment, a complete toolset for designing, implementing, and managing applications that demand high reliability and maintainability. GNAT Pro is available for Ada and also for C and C++.
● The CWE-Compatible CodePeer advanced static analysis tool, an automatic Ada code reviewer and validator that can detect and eliminate errors both during development and retrospectively on existing software. CodePeer can detect a number of the “Top 25 Most Dangerous Software Errors” in the MITRE Corporation’s Common Weakness Enumeration (CWE).
● The SPARK Pro verification environment, a toolset providing full formal verification oriented toward high-assurance systems with stringent security requirements.
● The QGen model-based development tool suite for safety-critical control systems, providing a qualifiable and customizable code generator and static verifier for a safe subset of Simulink® and Stateflow® models, and a model-level debugger.
Over the years customers have used AdaCore products to field and maintain a wide range of critical applications in domains such as commercial and military avionics, automotive, railway, space, defense systems, air traffic management/control, medical devices, and financial services. AdaCore has an extensive and growing worldwide customer base; see www.adacore.com/industries for further information.
AdaCore products are open source and come with expert online support provided by the developers themselves. The company has North American headquarters in New York and European headquarters in Paris. www.adacore.com.