Fast and sound static analysis

Astrée is a static analyzer for safety-critical software written or gen­er­ated in C or C++.

Astrée screenshot
Astrée screenshot
NIST logo

Astrée is sound — that is, if no errors are signaled, the absence of errors has been formally proved. In 2020, the US National Institute of Standards and Technology determined that Astrée satisfies their criteria for sound static code analysis.

Features

Who uses Astrée?

Since 2003, Airbus France has been using Astrée in the devel­opment of safety-critical software for vari­ous aircraft series, including the A380.

In 2018, Bosch Automotive Steering replaced their legacy tools with Astrée and RuleChecker in a pilot project for the entire Bosch Group. This led to significant savings thanks to faster analyses, higher accuracy, and optimized licensing and support costs. Bosch then acquired a worldwide license for both tools and the accompanying Qualification Support Kits.

Framatome employs Astrée for verification of their safety-critical TELEPERM XS platform that is used for engineering, testing, commissioning, operating and troubleshooting nuclear reactors.

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.

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, enabling ESA to transport payloads to the Inter­national Space Station.

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.

In the EU research project AQUAS, Astrée was used to analyze SYSGO’s PikeOS operating system.

MTU Friedrichshafen uses Astrée to demonstrate the cor­rectness of con­trol software for emer­gency power gene­rators in power plants. Together with its quali­fication package, Astrée is part of the IEC 60880 certi­fication process.

Static analysis of runtime properties

Astrée logo

Astrée statically analyzes whether the 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 or C++ that, according to the selected language standard, has undefined behavior or violates hardware-specific aspects.

Additionally, Astrée reports invalid concurrent behavior, violations of user-specified programming guidelines, and various program properties relevant for functional safety.

Astrée detects any:

Astrée is sound for floating-point computations and handles them precisely and safely. All possible rounding errors, and their cumu­lative effects, are taken into account. The same is true for −∞, +∞ and NaN values and their effects through arithmetic calculations and comparisons.

Data-flow and control-flow analysis

Flow icon

Astrée tracks accesses to global variables, static variables, and local variables whose accesses are made outside of the frame in which the local variables are defined (e.g. because their address is passed into a called function).

All data and function pointers are resolved automatically. The soundness of the analysis ensures that all potential targets of data and function pointers are taken into account.

Control-flow visualization

A picture is worth a thousand words. The graph-visualization capabilities of Astrée help you discover unexpected behavior of your software, and enable a faster and deeper understanding of third-party or legacy code.

Signal-flow analysis

Astrée is able to analyze the flow from input signals to output signals through complex real-world software. This is accomplished through taint analysis that builds upon a full-fledged semantic analysis, thus taking into account the influence of application configuration parameters on the signal flow.

The analysis can be performed for a specific application configuration, avoiding false signal flows not present in that configuration. Alternatively, the influence of application parameters on the output signal can be determined for a generic configuration.

If the taint analysis does not report an influence of an input signal on an output signal, independence has been proven. If an unexpected influence is reported, Astrée helps you understand the signal flow to either improve your code or tweak the analysis precision.

Analysis of interference between software components

Icon

Astrée enables you to define software components according to your own criteria, and to specify which data or control flow between the components is of interest to you. Astrée then detects every potential data and control interference between the components at the source-code level, and helps you understand the causes to improve your code if needed.

Support for C++ and mixed code bases

C++ icon

Since 2020, Astrée can be applied to C++ and mixed C/C++ code bases, supporting all modern C++ versions up to C++17.

Astrée’s C++ analysis uses the same technology as its C code analysis. It is designed to meet the characteristics of safety-critical embedded software, and is subject to the same restrictions as Astrée for C.

The high-level abstraction features and template library of C++ facilitate the design of very complex and dynamic software. Extensive use of these features may violate the established principles of safety-critical embedded software development and lead to unsatisfactory analysis times and results. The Astrée manual gives recommendations on the use of C++ features to ensure that the code can be well analyzed. For less constrained (less critical) C++ code, we recommend using the standalone RuleChecker.

MISRA and more

RuleChecker logo

The seamlessly integrated RuleChecker lets you check your code for compliance with various coding standards, including MISRA, CWE, ISO/IEC, SEI CERT, and AUTOSAR. You can easily toggle individual rules and even specific aspects of certain rules. The tool can also check for various code metrics such as com­ment den­sity or cyclomatic complexity. Custom extensions for your own in-house coding guidelines are available on request.

RuleChecker can be envoked separately, to allow for even faster checks of your code, or in conjunction with the sound semantic analyses offered by Astrée, to additionally guarantee zero false negatives and minimize false positives on semantical rules. No competing standalone MISRA checker can offer this, and no testing environment can match the full data and path coverage provided by the static analysis.

Qualification support

QSK icon

Your usage of Astrée can be qualified according to DO-178B/C, ISO 26262, IEC 61508, EN-50128, the FDA Principles of Software Validation, and other safety standards. We offer special Qualification Support Kits that simplify and automate the qualification process.

Tailor it to your own requirements

Astrée offers powerful annotation mechanisms for supplying external knowledge and fine-tuning the ana­lysis precision for individual loops or data structures. Detailed messages and an intui­tive GUI guide you to the exact cause of each potential runtime error. Actual errors can then be fixed, and in case of a false alarm the analyzer can be tuned to avoid it. This allows for analyses with very few or even zero false alarms.

dSPACE logo Jenkins logo Eclipse logo

The analyzer can also run in batch mode for easy integration into established tool-chains.

Plugins for TargetLink, Jenkins, and Eclipse are available and actively supported.

Ten years ahead of the competition

Astrée is…

  • Sound

    Most static analyzers do not consider all possible run­time errors. Others specifically focus on the most probable ones.

    As a result, almost all competing tools can only be used for static testing (i.e. finding some frequently occurring bugs), but never for verification (i.e. proving the absence of any run­time errors).

    In contrast, Astrée is sound. It always exhaustively considers all pos­sible 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.

    In 2020, the US National Institute of Standards and Technology determined Astrée to be one out of only two tools in total that satisfy their criteria for sound static code analysis.

  • Automatic

    Certain types of 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 any help from the user.

    Many analyzers cannot be scripted at all. Others can, but won’t let you access their analysis results outside of their proprietary viewer. This actively prevents you from automating the analysis, e.g. as part of your nightly build process.

    In contrast, Astrée offers you complete access to the analysis engine in batch mode, and lets you freely export the analysis results and further process them in any way you choose, no strings attached.

  • Fast

    Many static analyzers have high computational costs (typically, sever­al hours of compu­tation 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 pro­grams in industrial practice.

    As an example, in order to ana­lyze actual flight-control software with 132,000 lines of C code, even on a slow 2.8GHz PC Astrée takes a mere 80 min­utes. Faster machines will get you faster results. Multi­core parallel or distri­buted computation is supported.

  • Domain-aware

    General-purpose static analyzers aim at analyzing any application written in a given pro­gram­ming language. They can rely on language related properties to find potential run­time errors. Specialized static analyzers put additional restrictions on the app­lications 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­pli­ca­tion 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, allowing 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 run­time. The ratio of false alarms to the 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 pro­ducing exactly zero false alarms. This has been repeatedly proven in indus­tri­al practice, e.g. when analyzing primary flight-control software for Airbus.

  • Up-to-date

    Astrée builds upon decades of research in static program analysis, and also makes sure to incorporate the latest ongoing research, always staying well ahead of any competition.

    Major new releases are published twice a year, intermediate releases more often still. If you have a feature request, let us know at support@absint.com.


Free trial

Start your free trial today, complete with online training and technical support.