For two decades now, Airbus France has been using a wide array of our tools, including aiT, StackAnalyzer, Astrée, and CompCert in the development of safety-critical avionics software for several airplane types, including the A380, the world’s largest passenger aircraft. The analyzers are used as part of certification strategy to demonstrate compliance to DO-178B, up to Level A.
MTU Friedrichshafen uses CompCert, aiT, StackAnalyzer, Astrée and RuleChecker to demonstrate the correctness of control software for emergency power generators in power plants. The tools in combination with their qualification packages are part of the certification process according to IEC 60880 and IEC 61508-3:2010.
AREVA employs StackAnalyzer and Astrée for verification of their safety-critical TELEPERM XS platform that is used, among other things, for engineering, testing, commissioning, operating and troubleshooting nuclear reactors.
OHB uses aiT and StackAnalyzer in the development of onboard software essential for mission success of the SmallGEO satellite platform for geostationary communication satellites and the GALILEO FOC platform for satellite navigation.
Astrée was used to prove the absence of any runtime errors in a C version of the automatic docking software of the Jules Verne Automated Transfer Vehicle, enabling ESA to transport payloads to the International Space Station. This was the first fully automatic docking maneuver not performed by a Russian vessel.
As the world’s leading provider of embedded wireless communication and positioning solutions, u‑blox in Switzerland is using StackAnalyzer to avoid stack overflow problems at compile time and to increase the reliability and quality of their controlling software.
The global automotive supplier Helbako in Germany is using Astrée in their development process to demonstrate MISRA compliance of the code and to make sure that no runtime errors can occur in their electronic control software.
A world leader in motors and ventilators for air-conditioning and refrigeration systems, ebm-papst is using Astrée for fully automatic continuous verification of safety-critical interrupt-driven control software for commutating high-efficiency EC motors for ventilator systems.
In 2010, aiT was used by NASA as an industry-standard static analysis tool for demonstrating the absence of timing-related software defects in the Toyota Motor Corporation Unintended Acceleration Investigation.