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

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 

Featured Companies


150 W. 30th Street, 16th floor
New York, NY 10001

Tiera Oliver, editorial intern for Embedded Computing Design, is responsible for web content edits as well as newsletter updates. She also assists in news content as far as constructing and editing stories. Before interning for ECD, Tiera had recently graduated from Northern Arizona University where she received her B.A. in journalism and political science and worked as a news reporter for the university's student led newspaper, The Lumberjack.

More from Tiera