Certification Materials

Since the company's inception in the mid 1990s, AdaCore has been serving customers in the most demanding safety-critical industries. With this experience has come deep expertise across a range of major software safety certification standards, including DO-178B/C (avionics), EN 50128 (railway), ECSS-E-ST-40C / ECSS-Q-ST-80C (space), IEC 61508 (industrial automation), and ISO 26262 (automotive). Our tools and technology meet the most demanding certification requirements, from the perspectives of both feature functionality and safety assurance.

Certification Evidence for the Ada Run-Time Libraries and Compiler

The GNAT Pro toolchain includes various run-time profiles that can be embedded in certified applications, from a no-run time profile (zero footprint) to minimal feature sets (Ravenscar tasking or Cert/Minimal profiles). The code implementing these profiles can be provided with certification artifacts for various standards, including DO-178B/C or EN-50128, targeting the highest level of assurance.

In addition to 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, needed for level A certified software

  • For EN 50128, a T3 qualification kit

GNAT Pro Assurance - A toolchain with Guarantees for Certification Needs

Certification standards require specific control / configuration management on tools used to produce software. These tools - in particular the compiler - need to be fixed in time, and subject to additional analysis during development and maintenance of certified software. GNAT Pro Assurance is AdaCore's answer to meet these needs. The product's Sustained Branch service provides long-term support on a specific version of the technology, including safety-critical fixes years after the initial release and providing extra analysis, in particular impact analysis, on known problems.

Qualified Verification Tools

AdaCore provides a number of verification tools that can be used to address certification requirements. The certification process typically requires specific documentation in order to allow the these tools to be used without manual checks of their results; for example TQL-5 or TQL-4 qualification for DO-178C, or T2 for EN 50128. AdaCore can provide qualification documentation for a variety of tools, in particular:

Qualified Code Generator for Simulink®

The Simulink® modeling language is used to design control loop algorithms. Automatic code generators from Simulink® to Ada and to C can generate source code that is then compiled for deployment on an embedded target. Confidence in the generated source code can be obtained either by manual verification of this code, or by qualification of the code generator itself. AdaCore can provide DO-178C TQL1 or EN-50128 T3 qualification material for QGen, its code generator from Simulink® to Ada (in fact SPARK) and to MISRA C.

Read the books: AdaCore Technologies for EN 50128, AdaCore Technologies for DO-178C / ED-12C.