Astrée
Static source code analysis tool:
Runtime error and concurrency error detection
Five reasons to choose Astrée
Astrée is a high-end tool, based on formal methods, which guarantees that when it does not detect runtime errors, the application really has no runtime errors.
To date, 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-range array access errors.
- Incorrect pointer manipulations.
- Overflows of integer and floating point variables.
- Rounding errors in floating point calculations.
- Access to uninitialized variables.
- Problematic concurrent access to variables shared by several 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 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 aCertification Packagefor DO-178, ISO 26262, EN-50128 and FDA.
