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

June 23, 2020 Tiera Oliver

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 

About the Author

Tiera Oliver, edtorial 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.

Follow on Twitter Follow on Linkedin Visit Website More Content by Tiera Oliver
Previous Article
Embedded Toolbox: Use Ada and Let the Compiler Do the Static Analysis
Embedded Toolbox: Use Ada and Let the Compiler Do the Static Analysis

The Ada language abstracts most direct interaction with memory onto compilers, transitioning things like me...

Next Article
Inova Semiconductors Provides Standalone ISELED LED Driver & Controller in Volume Production
Inova Semiconductors Provides Standalone ISELED LED Driver & Controller in Volume Production

The INLC10AQ will be used to construct custom LED chains that can be controlled via a bidirectional two-wir...