In 2003, Astrée proved the absence of any runtime errors in the primary flight-control software of an Airbus model. The system’s 132,000 lines of C code were analyzed in only 80 minutes on a 2.8GHz 32-bit PC using 300MB of memory (and in only 50 minutes on an AMD Athlon 64 using 580MB of memory). Since then, Airbus France has been using Astrée in the development of safety-critical software for various plane series, including the A380.
In 2008, Astrée proved the absence of any runtime errors in a C version of the automatic docking software of the Jules Verne Automated Transfer Vehicle (ATV), enabling ESA to transport payloads to the International Space Station. This was the first fully automatic docking maneuver not performed by a Russian vessel.
The global automotive supplier Helbako in Germany is using Astrée to guarantee that no runtime errors can occur in their electronic control software and to demonstrate MISRA compliance of the code.
MTU uses Astrée to demonstrate the correctness of control software for emergency power generators in power plants. The tool in combination with its qualification package is part of the certification process according to IEC 60880.
AREVA employs 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.
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.
