Astrée is a static program analyzer that proves the absence of run-time errors (RTE) in safety-critical embedded applications written or automatically generated in C.

Astrée screenshot
Astrée screenshot

Astrée analyzes structured C programs with complex memory usages, but without recursion or dynamic memory allocation. This targets embedded applications as found in earth trans­por­tation, nuclear energy, medical instrumentation, aeronautics and space flight, in particular syn­chro­nous control/command such as electric flight control.

Which run-time properties are analyzed by Astrée?

Astrée analyses whether the C programming language is used correctly and whether there can be any run-time errors during any execution in any environment. This covers any use of C that has undefined behaviour as defined by the C99 standard, or that violates hardware-specific aspects as defined by the C99-standard.

Astrée reports any:

Astrée is sound for floating-point computations and handles them precisely and safely. It takes all possible rounding errors into account.

Tailor it to your own requirements

Astrée offers powerful annotation mechanisms, which enable you to make external knowledge available to it, or to selectively influence the analysis precision for individual loops or data structures. Detailed messages and an intuitive GUI help you understand alarms about potential errors. Actual errors can then be fixed, and in case of a false alarm, the analyzer can be tuned to avoid it. These mechanisms allow to perform analyses with very few or even zero false alarms.

Astrée can also be customized and integrated into established tool-chains.

Success stories

  • Airbus

    Airbus A380© 2007 Xavier Rival

    In November 2003, Astrée proved the ab­sence of any real-time errors in the primary flight-control software of one of Airbus’ models. The analysis was per­formed com­pletely automatically. 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 minutes on an AMD Athlon 64 using 580MB of memory). In January 2004, Astrée was extended to analyze the electric flight-control codes for another Airbus series.

  • Space flight

    Jules Verne ATVCourtesy of NASA

    In April 2008, Astrée was able to prove the absence of any RTE 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. The ana­lysis was performed completely automati­cally.


Your benefits

Astrée is…

  • Sound

    Some static analyzers do not consider all possible run-time errors. Others specifically focus on the most probable ones. As a result, those tools can only be used for static testing (i.e. for finding out the most frequently occuring bugs), but not for verification (i.e. for proving the absence of any run-time errors).

    In contrast, Astrée is sound. It will always exhaustively consider all possible run-time errors. It will never omit pointing out a potential run-time error. This is crucial for verification of safety-critical software. At the same time, Astrée is capable of producing exactly zero false alarms.

  • Automatic

    Some static analyzers (e.g. those relying on theorem provers) require programs to be annotated with lots of inductive invariants.

    Astrée usually requires very few annotations. It can even run completely automatically on certain types of programs, without relying on the user’s help at all.

  • Fast

    Some static analyzers have high computational costs (typically sever­al hours of computation per 10,000 lines of code). Others terminate out of memory, or may not terminate at all.

    In contrast, Astrée is efficient and easily scales up to real-world programs. This has been more than proven in industrial practice. For example, Astrée needed only 80 minutes (on a 2.8GHz PC) to ana­lyze the flight-control software of an Airbus model, which consists of 132,000 lines of C code. Since 2005, Astrée can run on multicore parallel or distributed machines, providing for even faster analysis.

  • Domain-aware

    General-purpose static analyzers aim at analyzing any application written in a given programming language. They can rely on language related properties to find potential run-time errors. Specialized static analyzers put additional restrictions on the applications so as to be able to take specific program structures into account.

    In contrast, Astrée is domain-aware. It thus knows facts about ap­plication domains that are indispensable to make sophisticated proofs. For example, for control/command programs, Astrée takes the logic and functional properties of control/command theory into account.

  • Parametric

    In static program analysis, there is always a trade-off between analysis precision and analysis cost. Analyzers that are precise are usually also very slow, while fast analyzers usually lack precision.

    In contrast, Astrée is parametric, which means that it allows you to freely trade speed for precision and vice versa. The level of abstraction used for analysis can be easily tailored to your very own requirements.

  • Modular

    Astrée consists of several modules (so called abstract domains). These modules can be assembled and parameterized to build application-specific analyzers that are fully adapted to a particular ap­plication domain or specific end-user requirements.

    In case of false alarms, Astrée can be easily extended by intro­duc­ing additional modules that enhance the precision of the analysis.

  • Precise

    General-purpose static analyzers usually suffer from low precision in terms of false alarms, i.e. spurious warnings about errors that can actu­ally never occur at runtime. The ratio of false alarms to number of basic C operations typically ranges between 10% and 20%.

    Specialized analyzers achieve a better precision of 10% or less. How­ever, even a very high selectivity rate of only 1 false alarm for every 100 operations is usually unacceptable for large real-world appli­cations. For example, on a program with 100,000 operations, a selec­tivity rate of only 1% yields 1000 false alarms.

    In contrast, thanks to its modularity and domain-awareness, Astrée can be made exceptionally precise, often to the point of producing exactly zero false alarms. This has been repeatedly proven in indus­tri­al practice, e.g. when analyzing primary flight-control software for Airbus.


Availability

For further information about Astrée, please contact us.

Top