Real-world applications of Astrée

In 2003, Astrée proved the ab­sence of any run­time errors in the primary flight-control software of an Airbus model. The sys­tem’s 132,000 lines of C code were ana­lyzed in only 80 minutes on a 2.8GHz 32-bit PC using 300MB of memory (and in only 50 min­utes on an AMD Athlon 64 using 580MB of memory). Since then, Airbus France has been using Astrée in the devel­opment of safety-critical software for vari­ous plane series, including the A380.

ESA logo

In 2008, Astrée proved the absence of any run­time errors in a C ver­sion of the auto­matic docking software of the Jules Verne Automated Transfer Vehicle (ATV), enabling ESA to transport payloads to the Inter­national Space Station. This was the first fully automatic docking maneuver not per­formed by a Rus­sian vessel.

The global automotive supplier Helbako in Germany is using Astrée to guar­antee that no run­time errors can occur in their elec­tronic control software and to de­monstrate MISRA compliance of the code.

MTU uses Astrée to demonstrate the cor­rectness of con­trol software for emer­gency power gene­rators in power plants. The tool in combination with its quali­fication 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 conti­nuous verification of safety-critical interrupt-driven control software for commu­tating high-efficiency EC motors for venti­lator systems.