Astrée
Outil d'analyse statique du code source :
Détection des erreurs d'exécution et de concurrence
Cinq raisons de choisir Astrée
Astrée est un outil haut de gamme, basé sur des méthodes formelles, qui garantit que lorsqu'il ne détecte pas d'erreurs d'exécution, l'application n'a pas réellement d'erreurs d'exécution.
À ce jour, il n'existe que deux outils sur le marché, basés sur des méthodes formelles, qui peuvent fournir cette garantie.
1. il fonctionne
Fonctionne pour les applications écrites en langage C.
2. Détecter
- Erreurs de simultanéité dans le système d'exploitation OSEK et le profil ARINC 653.
- Erreurs de division par zéro.
- Erreurs d'accès au tableau hors plage.
- Manipulations incorrectes des pointeurs.
- Débordements de variables entières et à virgule flottante.
- Erreurs d'arrondi dans les calculs en virgule flottante.
- Accès à des variables non initialisées.
- Accès concurrent problématique à des variables partagées par plusieurs processus.
- Erreurs d'incohérence du verrouillage des variables.
3. Permet
- Permet de diagnostiquer des assertions définies par l'utilisateur pour tester des propriétés supplémentaires au moment de l'exécution.
- Permet de tester quelles portions de code ne sont en aucun cas exécutables(détection de code mort).
4. Contrôler
Vérifier le code source par rapport aux normes de codage de logiciels suivantes :
- MISRA C (2004 et 2012, y compris l'amendement 1)
- Langage C99 (Annexe J de l'ISO/IEC 9899:1999)
- CWE (précisions CCR exactes, CWE plus abstraites et CWE plus spécifiques)
- SEI CERT C
- ISO/IEC TS 17961:2012
5. En outre...
- Il dispose d'un IDE et d'une interface de ligne de commande, permettant l'exécution par lots pour faciliter les tests de régression.
- Il est intégré à Jenkins, SCADE, TargetLink (dSPACE), SymtaVision et RT-Druid.
- Il dispose d'un ensemble decertifications pour DO-178, ISO 26262, EN-50128 et FDA.
