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 analyzes structured C programs with complex memory usages, but without recursion or dynamic memory allocation. This targets embedded applications as found in earth transportation, nuclear energy, medical instrumentation, aeronautics and space flight, in particular synchronous 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:
- division by zero,
- out-of-bounds array indexing,
- erroneous pointer manipulation and dereferencing (NULL, uninitialized and dangling pointers),
- integer and floating-point arithmetic overflow,
- violation of optional user-defined assertions to prove additional run-time properties (similar to assert diagnostics),
- code it can prove to be unreachable under any circumstances (note that this is not necessarily all unreachable code),
- read access to unintialized variables.
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
© 2007 Xavier RivalIn November 2003, Astrée proved the absence of any real-time errors in the primary flight-control software of one of Airbus’ models. The analysis was performed completely automatically. 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). In January 2004, Astrée was extended to analyze the electric flight-control codes for another Airbus series.
Space flight
Courtesy of NASAIn 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 analysis was performed completely automatically.
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 several 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 analyze 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 application 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 application domain or specific end-user requirements.
In case of false alarms, Astrée can be easily extended by introducing 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 actually 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. However, even a very high selectivity rate of only 1 false alarm for every 100 operations is usually unacceptable for large real-world applications. For example, on a program with 100,000 operations, a selectivity 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 industrial practice, e.g. when analyzing primary flight-control software for Airbus.
Availability
For further information about Astrée, please contact us.