AdaCore has a long and successful history serving customers in the Avionics industry. Our products help developers build and verify software systems that meet the highest levels of safety certification.
On average, more than 8 million people worldwide fly in commercial airplanes every day. That’s over 3 billion passengers a year. Yet air travel continues to be our safest mode of transportation. This is in great part due to the fact that the Avionics industry has set the most stringent requirements for the development of safe and reliable software.
Meeting DO-178 requirements is often a challenging and expensive process. AdaCore has years of experience working with avionics customers and has a deep understanding of the complexities of the certification process and tools needed to ease the workflow and manage costs.
Our Roots in Certification - Levels A and B in DO-178B / DO-178C
The company has extensive knowledge of and experience with avionics software certification standards, with AdaCore personnel playing an active role in standards-related working groups and committees. AdaCore President and co-founder Dr. Cyrille Comar is a recognized expert in software certification and participated in the development effort for DO-178C and its associated supplements.
Qualified Tools, Runtime Libraries and Certification Materials
Several of our tools have been qualified, thus reducing the effort to meet verification objectives including coding standard compliance, code accuracy (prevention of errors such as buffer overrun, integer overflow, and references to uninitialized variables), and structural coverage analysis up to MC/DC. Specialized high-assurance run-time libraries, including one that implements the Ravenscar tasking profile, are simple enough to be included in certified systems but expressive enough to support the needed functionality for hard real-time avionics software. Qualification and certification material for these tools and libraries is available and is adaptable to new project contexts.
Maintaining certified software brings unique challenges, since the customer needs to "freeze" on a specific version of the technology for stability, but still might require updated releases if a problem is encountered as the software evolves. AdaCore's "sustained branch" service, a standard part of the GNAT Pro assurance product, supports this requirement consistent with the guidance in DO-178B / DO-178C.
Customer Projects: Avionics
Major European Aerospace Company Chooses GNAT Pro Ada Targeted to Wind River’s VxWorks 6.x Cert RTOS on PowerPC
Airbus Helicopters (France) has selected the GNAT Pro tool suite and the Ada programming language to develop new software components for the VSR700 prototype project. VSR700 is Airbus Helicopters’ tactical unmanned aerial system (UAS) designed to meet the demanding requirements of global navies and armies in the 21st century.
Thales Aerospace Division Selects GNAT Pro for Airbus A350 XWB (Xtra Wide-Body)
Thales will use the GNAT Pro High-Integrity Edition for DO-178B and the Ada 2005 language to build the Air Data Inertial Reference Unit (ADIRU) for the A350 XWB (Xtra Wide-Body). The ADIRU provides precise in-flight positioning information, and the new system will therefore need to be certified to the highest safety levels. It will meet Level A of the DO-178B standard and use ARINC 653 multi-partition operating system MACS2.
AdaCore Technologies for DO-178C / ED-12C
The guidance in the DO-178C / ED-12C standard and its associated technology-specific supplements helps achieve confidence that airborne software meets its requirements. Certifying that a system complies with this guidance is a challenging task, especially for the verification activities, but appropriate usage of qualified tools and specialized run- time libraries can significantly simplify the effort. This document explains how a number of technologies offered by AdaCore – tools, libraries, and supplemental services – can help.
Read our booklet »
GNAT Pro Assurance
GNAT Pro Assurance includes a specialized service known as sustained branches, which allows a project to continue its use of a specific version of the technology, including upgrades to repair critical issues. It supports all versions of the Ada language standard (from Ada 83 to Ada 2012), and C support is an optional add-on. A full toolsuite is supplied, as well as a configurable run-time library and several specific run-times that are especially suited to high-assurance systems.
SPARK Pro is a language and toolset specifically designed for developing applications where correct operation is vital for safety or security. The SPARK Pro toolset offers static verification that is unrivalled in terms of its soundness, low false-alarm rate, depth and efficiency. The toolset generates evidence for correctness that can be used to meet the requirements of safety and security certification schemes.
CodePeer is an Ada source code analyzer that detects runtime and logic errors. It assesses potential bugs before program execution, serving as an automated peer reviewer, helping to find errors efficiently and early in the development life-cycle. It can also be used to perform impact analysis when introducing changes to the existing code, as well as helping vulnerability analysis. Using control-flow, data-flow, and other advanced static analysis techniques, CodePeer detects errors that would otherwise only be found through labor-intensive debugging.
GNATcoverage allows coverage analysis of both object code (instruction and branch coverage), and Ada or C language source code (Statement, Decision and Modified Condition/Decision Coverage - MC/DC)
QGen is a model-based development toolsuite for Simulink® and Stateflow® reduces the development and verification costs for developers of safety- and security-critical applications, through qualifiable code generation, model verification, and tight integration with AdaCore’s qualifiable target emulation and structural coverage analysis tools. The QGen code generator can generate MISRA C, but can also generate the verifiable SPARK subset of Ada, from Simulink® and Stateflow®. By selecting SPARK for code generation, can formally prove important safety and security properties of their software, not only enhancing quality but also decreasing testing costs.