logo slogan

Astrée: Fast and sound runtime error analysis

Finding all Runtime Errors and Data Races in C Programs: Astrée is a parametric static analyzer designed to prove the absence of runtime errors and data races in software programs written in C. Astrée is parameterizable and can be specialized to the program under analysis –key-features to enable high analysis precision.

 

Astrée is a static code analyzer that proves the absence of runtime errors and invalid concurrent behaviour in safety-critical software written or generated in C.

 

Astree Astree

 

Astrée primarily targets embedded applications as found in aeronautics, earth transportation, medical instrumentation, nuclear energy, and space flight. Nevertheless, it can just as well be used to analyze any structured C programs, handwritten or generated, with complex memory usages, dynamic memory allocation, and recursion.

 

Astrée is sound — that is, if no errors are signalled, the absence of errors has been proved.

 

Which runtime properties are analysed by Astrée?

 

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

 

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

Astrée detects 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,

       

    • • read access to uninitialized variables,

       

    • • data races (read/write or write/write concurrent accesses by two threads to the same memory location without proper mutex locking),

       

    • • inconsistent locking (lock/unlock problems),

       

    • • invalid calls to operating system services (e.g. OSEK calls to Terminate-task on a task with unreleased resources),

       

    • • violation of optional user-defined assertions to prove additional runtime properties (similar to assert diagnostics),

       

    • • code it can prove to be unreachable under any circumstances.

     

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

 

MISRA and more

 

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

 

Using RuleChecker in conjunction with the sound semantic analyses offered by Astrée guarantees zero false negatives and minimizes false positives on semantic-al rules. No standalone MISRA checker can offer this, and no testing environment can match the full data and path coverage provided by the static analysis.

 

NOTE: The CTO's of both AbsInt and Phaedsys are on the MISRA-C working Group. Phaedsys since it's inception

 

 


Tailor it to your own requirements

 

Astrée offers powerful annotation mechanisms for supplying external knowledge and fine-tuning the analysis precision for individual loops or data structures. Detailed messages and an intuitive 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.

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

Seamless integration with TargetLink, Jenkins, and Eclipse is actively supported

  

dSPACE logo Jenkins logo Eclipse logo

 

 

 

Qualification support

 

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.

 

 


Ten years ahead of competition

 

Astrée is…

Sound

 

 

 

 

 

 

 

 

  • Most static analysers do not consider all possible runtime 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 runtime errors).

    In contrast, Astrée is sound. It always exhaustively considers all possible runtime errors. It will never omit pointing out a potential runtime 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

 

 

 

 

 

 

 

 

 

 

  • Certain static analysers (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 analysers 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 analysers 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 in industrial practice.

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

 

Domain Aware

 

 

 

 

 

 

  • General-purpose static analysers aim at analysing any application written in a given programming language. They can rely on language related properties to find potential runtime errors. Specialized static analysers 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. Analysers that are precise are usually also very slow, while fast analyzer 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 parametrized to build application-specific analysers 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 analysers 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 the number of basic C operations typically ranges between 10% and 20%.

    Specialized analysers 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 analysing primary flight-control software for Airbus.

     

Up to date

 

 

 

  • Astrée not only builds upon decades of research in static program analysis, but also incorporates 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 info@phaedsys.com.

 

 

 

Who uses Astrée?

 

  • Automotive

 

 

 

 

 

 

 

     

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.

 

 

 

Bosch Automotive Steering replaced their legacy tools with Astrée and RuleChecker, resulting in significant savings thanks to faster analyses, higher accuracy, and optimized licensing and support costs.

 

 

 

Aviation

 

 

 

 

 

 

In 2003, Astrée proved the absence of any runtime errors in the primary flight-control software of an Airbus model. Automatically in only 80he system’s 132,000 lines of C code were analysed completely

 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.

 

  • Power plants

 

 

 

 

 

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.

MTU Friedrichshafen uses Astrée to demonstrate the correctness of control software s for emergency power generator power plants. Together with its qualification package, Astrée is part of the IEC 60880 certification process.

 

  • Space flight

 

 

 

 

 

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 manoeuvre not performed by a Russian vessel.

 

 

 

 

  • Ventilation

 

 

 

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.

 

 

 

 

Free 30-day trial

To download a free copy of Astrée, fill out and sign the license agreement form (PDF) and email or fax it to us.

Astrée runs under 64-bit Windows and 64-bit Linux. The trial version is technically identical to the full commercial version in every respect, but your license file will expire after 30 days.

If you have any questions before trying, email our customer support.

 

Free training

There’s no need to figure out Astrée by yourself or read the user manual cover to cover. Your trial begins with a free interactive Web-based training. We use Web-ex for sharing our desktop with you, and regular phone for the sound.

After just about 90 minutes, on a date and time of your own choosing, you are set to go. And it’s only then that your license file gets activated, so you still have a full 30 days left.

 

Free support to get you started

 

Don’t hesitate to contact info@phaedsys.com with any questions during your trial. You can even request additional Web-ex sessions if you need help with setting up an analysis, writing a complex annotation, or investigating a tricky part of your code.

All commercial licenses also include 180 days of free support and updates. Major new releases are published twice a year, which means you’ll receive at least one update for free.

 

 

Price quote

The one-time fee for a perpetual license depends on the number of installations and the number of analyses running in parallel. Qualification Support Kits are available at a fraction of the cost. You can also rent the tool, or commission us to analyze your code for you.

 

Email us for a quote tailored to your personal requirements

 

Further Reading

Quick Facts