Toyota and NVIDIA focus on zero defects software development mathematically

The safety requirements for in-vehicle software as defined within the ISO 26262 standard are increasing rapidly. This is particularly true for autonomous driving and steer-by-wire (SBW) applications, given the potential for severely life-threatening or fatal injury in the event of a malfunction.

This article, written by Hidemasa Kimura of Nikkei Xtech, describes how two prominent automotive manufacturers, JTEKT and NVIDIA, are working to meet these stringent safety requirements by leveraging the Ada and SPARK languages to facilitate unit testing and verification of their systems’ existing C source code, and using "theorem proving" (a type of formal method) to mathematically prove that their software has no defects.

Using formal methods to ensure the correctness of C code generated from SPARK is at the cutting edge of automotive safety/security technology. And 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.

Download in English
Download in French