AdaCore and NVIDIA team on Ada and SPARK programming languages for safety-critical software
Feb. 14, 2019
NEW YORK –Software specialist AdaCore in New York is working with NVIDIA Corp. in Santa Clara, Calif., to implement the Ada and SPARK programming languages for security- and safety-critical firmware in applications like avionics and self-driving cars.
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 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 and SPARK programming languages are designed to help meet stringent software requirements for safety and security. The Ada programming language has built-in features that detect code defects early in the software life cycle.
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 formally can demonstrate properties of the safety-critical code, ranging from correct data flows and absence of run-time errors such as overflow, to more advanced assertions and satisfaction of functional requirements.
For more information contact AdaCore online at www.adacore.com or NVIDIA at www.nvidia.com/en-us.
Ready to make a purchase? Search the Military & Aerospace Electronics Buyer's Guide for companies, new products, press releases, and videos
