Tel. +31­ 345 545535
 
Embedded
Products
 
Solutions
Coming soon...
 
Partners
Who we work with
 
News
What's going on
 
Media
Something to read
 
About
Who we are
 
Contact
Where we are
You are on the following page: Products > Safety Critical & Certified Systems > Formal Verification > Astrée Sound Static code Analyzer Nederlands | French
 
 

Astrée Sound Static code Analyzer

Astrée is a static code analyzer that proves the absence of run­time errors and invalid con­current behavior in safety-critical software written or gen­er­ated 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 aero­nautics, earth trans­por­tation, medical instrumen­tation, nuclear energy, and space flight. Never­theless, 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.

Sound verification

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 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.


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 run­time 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:

  • 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 TerminateTask 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 also 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.

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 com­ment den­sity 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?
Automotive
Aviation
Power plants
Space flight
Ventilation


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.

Bosch logo
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 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.

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

 

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.

 

In contrast to other Static Analyzers 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.

  • Automatic

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.

 

Fast
Domain-aware
Parametric
Modular
Precise
Up-to-date

 


Free trial
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 !

 

Contact :

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.

 

   

 
 

INDES-IDS BV offers solutions for Embedded Software Development as well as for the Telecommunication NEMS and Service Providers. In these markets we offer products of either the market leader or the innovation leaders. Our goal is to assist you to get to the market sooner by offering a combination of products, knowledge and services.