Astrée
Static source code analysis tool:
Detection of run-time errors and concurrency errors
Five reasons to choose Astrée
Astrée is a high-end tool, based on formal methods, that guarantees that when it does not detect run-time errors, the application truly has no run-time errors.
Currently, there are only two tools on the market, based on formal methods, that can provide this guarantee.
1. It works
It works for applications written in C language.
2. It detects
- Concurrency errors in the OSEK operating system and ARINC 653 profile.
- Division by zero errors.
- Out-of-bounds array access errors.
- Incorrect pointer manipulations.
- Integer and floating-point variable overflows.
- Rounding errors in floating-point calculations.
- Accesses to uninitialized variables.
- Problematic concurrent accesses to variables shared by multiple processes.
- Variable locking inconsistency errors.
3. It allows
- It allows the diagnosis of user-defined assertions to test additional properties at runtime.
- It allows to test which portions of code are not executable under any circumstances (dead code detection).
4. It checks
It checks the source code against the following software coding standards:
- MISRA C (2004 and 2012, including Amendment 1)
- C99 language (Annex J of ISO/IEC 9899:1999)
- CWE (CCR accuracies Exact, CWE-more-abstract and CWE-more-specific)
- SEI CERT C
- ISO/IEC TS 17961:2012
5. In addition
- It has an IDE and command-line interface, allowing batch execution to facilitate regression testing.
- It has integrations with Jenkins, SCADE, TargetLink (dSPACE), SymtaVision and RT-Druid.
- It has a Certification Package for DO-178, ISO 26262, EN-50128 and FDA.
