AdaCore and NVIDIA partner on security-critical firmware
NVIDIA is in the process of migrating some product lines to a new architecture using the RISC-V ISA. The company will also upgrade select security-critical firmware software, rewriting it from C to Ada and SPARK. These moves will increase verification efficiencies to achieve compliance with the functional safety standard ISO-26262.
Ada and SPARK are designed to help meet the most stringent software requirements for safety and security. The Ada programming language has built-in features that detect code defects early in the software life cyclet. 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 the absence of run-time errors such as overflow, to more advanced assertions and satisfaction of functional requirements.
More information
Related news
AdaCore joins RISC-V Foundation
Ada competition results show path to improved code quality – AdaCore
DO-178C/ED-12C Guidance from AdaCore, as handbook download
Adacore improves static analysis tool, supports more environments
If you enjoyed this article, you will like the following ones: don't miss them by subscribing to :