GNAT Pro Assurance guarantees
your certification needs
GNAT Pro Assurance offers a number of options that can simplify the development and verification effort, and provide real cost savings for projects with stringent certification requirements. These include certification material for the run-time libraries, as well as qualification material for several AdaCore tools.
A software system needs to be maintained and updated over time in response to changing requirements. The customer thus needs to have confidence that if an issue such as a code generation problem is encountered, then it can be addressed in the context of the version of the compiler that is being used. That is the purpose of AdaCore’s “sustained branch” service; guaranteeing product stability, with controlled evolution to correct problems.
The GNAT Pro compiler is also validated by SuperTest™ for safety-critical mixed language development.
Certification Evidence for the Ada Run-Time Libraries and Compiler
The GNAT Pro toolchain includes a number of run-time libraries (“profiles”) that can be used in certified applications, ranging from a “no-run time” profile (zero footprint) to minimal feature sets (Ravenscar tasking or Cert/Minimal profiles). We have deep expertise across a range of major software safety certification standards. These include:
Commercial airborne software
|CAP670 / SW01|
Air Traffic Services
Railway - signalling equipment
Railway - software embedded on trains
|ECSS-E-ST-40C / ECSS-Q-ST-80C|
Air Traffic Management
Beyond what is needed for the run-time libraries, some standards require specific certification evidence for the compiler itself. AdaCore can provide such artifacts, in particular:
For DO-178B/C — a source-to-object traceability study for Ada or C, applicable to level A certified software (Objective A-7 (9))
For EN-50128/EN-50657 and IEC-61508 — qualification material for GNAT Pro at level T3
For ISO-26262 — a TCL3 level qualification, required for ASIL4 certified software
This document explains how a number of technologies offered by AdaCore – tools, libraries, and supplemental services – can help. It covers not only the “core” DO-178C / ED-12C standard but also the technology supplements: Model-Based Development and Verification (DO-331 / ED-218), Object-Oriented Technology and Related Techniques (DO-332 / ED-217), and Formal Methods (DO-333 / ED-216).
This document presents the usage of AdaCore’s technology in conjunction with the CENELEC EN 50128:2011 standard. It describes where the technology fits best and how it can best be used to meet various requirements of the standard.
Qualifiable Code Generator for Simulink® and Stateflow® models
AdaCore’s QGen is a qualifiable and tunable code generation and model verification toolsuite for a safe subset of Simulink® and Stateflow® models. The selected feature set ensures code generation that is appropriate for critical control loop algorithms, leaving out features that might result in unpredictable behavior or potentially unsafe source code. The QGen code generator translates the models into source code in either the portable MISRA subset of C, or the formally analyzable SPARK subset of Ada.
AdaCore can provide DO-178C TQL1 or EN-50128 T3 qualification material for QGen. Official qualification of the code generator is planned for late 2021 or early 2022.
Our tools and technologies are also useful for developers who need to certify their software with respect to standards that are not safety-related, such as the FACE™ (Future Airborne Capability Environment) Technical Standard. With AdaCore’s products, developers can meet the relevant conformance requirements while gaining additional benefit in terms of assurance (reliability, safety, and/or security).
NVIDIA plans to upgrade select security-critical firmware software, rewriting it from C to Ada and SPARK to increase verification efficiencies to achieve compliance with the functional safety standard ISO-26262.