Nvidia drives Ada and SPARK into driverless cars
Cette publication existe aussi en Français
AdaCore and Nvidia have developed an open source reference flow for the Ada and SPARK programming languages in safety critical automotive software, particularly for driverless cars.
The flow enables faster development of ISO26262 software on top of the Nvidia DriveOS operating system. Nvidia developed DriveOS with 7m lines of codes using SPARK alongside the certification flow for applications on its DRIVE AGX-based hardware.
The AGX-Orin chip, based on the Ampere GPU architecture and ARM Cortex A78AE cores, is being used by car makers including Volvo, Mercedes-Benz, Jaguar Landrover, GM, Zeekr and Geely and now Toyota, the world’s largest car maker.
The AGX-Thor chip based on the Blackwell architecture with NeoverseV3AE cores, is expected to sample later this year for autonomous driving. This is being used by Chinese EV maker BYD, autonomous shuttle maker WeRide, Volvo, truck maker Aurora, Continental and Li Auto.
DriveOS was certified to ASIL-D by TUD SUD in January on the Orin chip, with an AI safety framework called Halos.
“The time for autonomous vehicles has arrived and we will work with AI in manufacturing, enterprise and the way they simulate and design cars and in the car,” said Jensen Huang, CEO of Nvidia. “We’ve been working on self driving cars for over a decade.”
The reference flow is a key step forward and includes software components that comply with the highest levels of integrity of the automotive certification standard ISO-26262. Using SPARK required establishing a development process that takes advantage of formal methods and other safety characteristics of the Ada formal language and its SPARK subset.
AdaCore and Nvidia have decided to publish the reference process as an open-source and evolving document, allowing the industry at large to adopt Ada and SPARK.
“This marks an important turning point for developers working on software-defined vehicles,” Quentin Ochem, Chief Product and Revenue Officer at AdaCore tells eeNews Europe..
“What’s unique here is Nvidia’s approach. By adopting Ada and SPARK and openly publishing their ISO 26262 qualification documentation, they are reshaping how these responsibilities are handled. Rather than burden developers with siloed, abstract compliance activities, Nvidia is bringing these concerns as close as possible to the developer’s primary artifact: the code itself. This aligns with a growing trend to integrate verification, traceability, and requirements directly into the development flow, making correctness a property of the codebase, not just a separate process.”
“Traditionally, developers have had to wear many hats—beyond writing code, they often find themselves taking on the responsibilities of QA engineers, verification engineers, and even requirements engineers,” he added.
“Safety-critical domains like automotive, governed by standards such as ISO 26262, demand rigorous traceability, evidence of correctness, and formal assurance—responsibilities that go far beyond conventional software engineering.”
He also points to Nvidia’s decision to open source the certification artefacts as a key move.
“It’s also rare to see a major technology provider open up their internal safety certification process to this degree. The fact that Nvidia’s ISO 26262 documentation is usable off-the-shelf is a big deal—it provides a concrete, practical starting point for other automotive software teams. It lowers the barrier to entry for developers and companies aiming to build safe, certified vehicle software, without reinventing the wheel.”
The ISO-26262 reference process is available on nvidia.github.io/spark-process/ and can be used or customized freely by anyone interested in adopting these languages.
ISO26262 process
The document defines a SPARK-based ISO-26262-compliant process for developing a subset of the safety-critical vehicle software units to ASIL D and to lower ASILs.
The process applies exclusively to software units that are developed entirely in the Ada programming language, but is oriented towards software units for which some or all of the Ada code complies with the SPARK subset. While some elements of this process, such as required Ada compiler warning settings, may be applicable to safety-critical Ada software development in general, a software unit that mixes Ada with other languages (such as C, C++, or assembly language) cannot be developed using this process.
This process covers the ISO 26262 requirements and objectives relevant to language subsets, software unit design, software unit implementation, and software unit verification. Additionally, the process covers the ISO 26262 requirements and objectives related to safety requirements when they are expressed in software interface specifications.
This process supports formal verification and non-formal verification side-by-side. A single software unit developed according to this process can be formally verified in its entirety, non-formally verified in its entirety, or partially formally verified and partially non-formally verified.
“In short, this move helps demystify safety certification for developers and paves the way for more robust and efficient software-defined vehicle architectures,” said Ochem.
Adopting a new programming language involves deploying a new environment, training teams to a new formalism, adapting programming patterns and many other issues. However, from a process standpoint, programming languages are vastly interchangeable, but Ada and SPARK is a different story.
Considering it as a language shift is a possibility, and this would certainly yield value across a traditional development process. This would however miss the key opportunity brought by the technology, the ability to spin the development process to a verification driven process, allowing to demonstrate software properties in a much more rigorous and cost effective way than traditional methods.
Ada semantics are designed to minimize the risk of vulnerability and maximize the semantic information defined directly in the source code. SPARK uses these attributes to avoid common vulnerabilities and allows defining additional properties to be formally verified in place of dynamic testing.
In SPARK, it is possible to guarantee basic properties such as variable initialization, absence of buffer overflow, range of data, or more generally what would otherwise end up being defensive code, But it also provides means to define more advanced requirements that can be expressed in the form of boolean assertions, and against which an implementation can be formally demonstrated to be correct without any need of running tests.
Developing code with formal verification in mind has an impact at various levels in the development process. Establishing a way to develop software in this way can be a long iterative path, with risks of missing some key aspects of the technology.
The reference flow aims to allow new adopters to skip this, and start off an already established process which has been reviewed by authorities and experimented with by the industry. It is not meant to be used ‘as-is’, but as a starting point for a customized process fit to the specific situation of each individual organization.
However Nvidia points out that the flow does not cover software architectural design specification, how to port an existing C/C++ software unit to this SPARK-based process or concurrency or software safety analysis.
www.adacore.com; nvidia.github.io/spark-process/
If you enjoyed this article, you will like the following ones: don't miss them by subscribing to :
