AdaCore announced it is working with NVIDIA to implement Ada and SPARK programming languages for select security-critical firmware used for applications that demand stringent safety and security capabilities, like automated and autonomous driving.
Some NVIDIA system-on-a-chip product lines will migrate to a new architecture using the RISC-V Instruction Set Architecture (ISA). Also, NVIDIA plans to upgrade select security-critical firmware software, rewriting it from C to Ada and SPARK. Both moves are intended to increase verification efficiencies to achieve compliance with the functional safety standard ISO-26262.
The Ada programming language has numerous built-in features that detect code defects early in the software life cycle, expediting the peer review and testing effort. The SPARK language — a restricted set of Ada features designed to perform a formal mathematical proof — increases the certainty of catching defects early that might not have been detected otherwise. SPARK facilitates static analysis that can formally demonstrate certain properties of the code, ranging from correct data flows and absence of run-time errors such as overflow, to more advanced assertions and satisfaction of functional requirements.