Astrée Sound Static code Analyzer
Astrée is a static code analyzer that proves the absence of runtime errors and invalid concurrent behavior in safety-critical software written or generated in C. It takes Static analysys one step further by doing a Formal Verification of the code by using the mathematical methodology of Abstract Interpretation. As a result the verification can guarantee there are no run-time errors!
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 signaled, the absence of errors has been proven.
Most static analyzers 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.
Which runtime properties are analyzed by Astrée?
Astrée analyzes 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 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 also 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 cyclomatic 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 semantical 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.
Who uses Astrée?
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.
Tailor it to you 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 (click for more) >
dSPACE logo Jenkins logo Eclipse logo
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.
In contrast to other Static Analyzers Astrée is...
Most static analyzers 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.
Certain 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.
Request your free trial package today.
Learn more (follow the links) :
- How the analysis works >>
- Compliance with C99, CWE, SEI CERT, MISRA, ISO/IEC >>
Integration with TargetLink, Jenkins, Eclipse >>
Current release: 18.10 >>
Introductory slide slow >>
Also note the links to datasheets at the right of this page !
Please do not hesitate to contact Gerard Fianen at INDES-IDS BV to discuss your S/W verification & test requirments and for inquiries about pricing and licensing models.