Electric Power Steering System Supplier JTEKT Selects SPARK Pro for Safety-Critical Automotive Software

By Tiera Oliver

Associate Editor

Embedded Computing Design

June 23, 2020


Formal methods help JTEKT reduce development and verification costs for safe autonomous driving systems.

AdaCore announced that JTEKT has adopted AdaCore’s SPARK Pro tool suite and the GNAT Pro Common Code Generator (CCG) to aid in the development of safety-critical power steering system software. 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. 

SPARK Pro is a toolset based on the formally analyzable SPARK subset of the Ada language, allowing developers to confirm 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.

For more information, visit: www.adacore.com/industries 

Tiera Oliver, Associate Editor for Embedded Computing Design, is responsible for web content edits, product news, and constructing stories. She also assists with newsletter updates as well as contributing and editing content for ECD podcasts and the ECD YouTube channel. Before working at ECD, Tiera graduated from Northern Arizona University where she received her B.S. in journalism and political science and worked as a news reporter for the university’s student led newspaper, The Lumberjack.

More from Tiera