Astrée automatically proves the absence of runtime errors and invalid concurrent behavior in C applications. It is sound for floating-point computations, very fast, and exceptionally precise. The analyzer also checks for MISRA coding rules and supports qualification for ISO 26262, DO-178C level A, and other safety standards. Jenkins and Eclipse plugins are available.
Key Features of Astrée:
- Astrée is sound: If the analysis does not detect any errors, the absence of runtime errors has been proven. Control and data coverage is 100%.
- Astrée is precise: Its state-of-the-art analysis engine enables very low false alarm rates.
- Astrée is scalable: Industrial avionics software with more than 500 KLOC has successfully been analyzed with zero false alarms on a PC in a few hours.
- Astrée supports precise floating-point arithmetics taking rounding errors into account.
- False alarms can be safely eliminated by tuning the precision to the software under analysis.
- Astrée enables you to interactively explore the analysis results.
- A Qualification Support Kit is available, providing support for automatic tool qualification up to the highest criticality levels.
- Astrée automatically takes the OS configuration of ARINC653/OSEK/AUTOSAR projects into account.
- Astrée can be seamlessly integrated with dSPACE TargetLink; dedicated domains ensure unparalleled analysis precision.