L’analyseur statique Astrée prouve l’absence d’erreurs à l’exécution dans les codes critiques embarqués écrits en C et C++.
Astrée est constitué prioritairement pour l’analyse d’applications embarquées instables, en particulier dans les domaines de l’astronautique et de l’aéronautique, du transport, de technologie médicale et d’installation nucléaire. En principe, Astrée peut analyser des programmes quelconques écrit en C ou C++, tant manuscrit que généré automatiquement, avec d’utilisation du stockage complexe, d’allocation du stockage dynamique et de récursivité.
Quelles propriétés de durée sont contrôlées par Astrée ?
Les erreurs trouvées par Astrée sont :
- Tout usage de C ou C++ défini dans les normes internationales ayant un comportement indéfini (divisions par zéro, débordements d’index de tableau, manipulations et déréférences de pointeurs nuls et invalides)
- Toute violation de la norme ISO/IEC 9899:1999 relative aux comportements spécifiques d’une implémentation sur une machine donnée (comme la taille des entiers et les débordements arithmétiques)
- Tout usage potentiellement erroné ou incorrect de C ou C++ contraire à des règles optionnelles de bon usage définies par l’utilisateur (comme l’exclusion de l’arithmétique modulaire pour les entiers signés même si c’est l’option implantée par le matériel)
- Toute violation d’assertions optionnelles insérées par l’utilisateur dans le code source
- Violations des règles MISRA, CWE, SEI CERT, ISO/IEC et AUTOSAR
Astrée traite précisément et sûrement les calculs de virgule flottante.
Toute erreur d’arrondi possible ainsi que leurs effets cumulatifs sont prit
en compte. Le même s’applique pour des valeurs −∞, +∞ et NaN
dans tous des calculs et des comparaisons.
Champs d’application
Astrée a été utilisé pour vérifier l’absence d’erreurs à l’exécution dans le logiciel de commande de vol électrique primaire de deux types d’avion Airbus.
Astrée est déployé par l’équipementier automobile Robert Bosch, après une expérimentation intensive d’un an dans sa Division « Automotive Steering ».
Leader mondial dans les moteurs et les ventilateurs pour les systèmes de climatisation et de réfrigération, ebm-papst utilise Astrée pour la vérification entièrement automatique continue de logiciels de contrôle critique pilotés par interruption pour la commutation de moteurs EC à haut rendement pour des systèmes de ventilateurs.
En Avril 2008, Astrée pouvait prouver l’absence de tout erreur d’exécution dans une version C des logiciels d’accostage automatique du Véhicule automatique de transfert européen (ATV) Jules Verne développé pour ravitailler la Station spatiale internationale (ISS). L’analyse était effectuée de façon complètement automatique.
Le fournisseur automobile global Helbako utilise Astrée dans le processus de développement pour démontrer la conformité du code avec MISRA et pour vérifier qu’aucune erreur à l’exécution ne peut arriver dans les logiciels de contròle électronique.
MTU Friedrichshafen utilise Astrée pour démontrer la justesse du logiciel de contrôle pour les générateurs de secours dans les centrales électriques. Les outils combinés avec leurs kits de qualification (QSK et QSLCD) font partie du processus de certification selon l’IEC60880.
Caractéristiques
Astrée est basé sur l’interprétation abstraite de la sémantique des programmes analysés et calcule donc une sur-approximation de l’ensemble des comportements possibles du code à l’exécution. Astrée est donc correct et ne peut jamais omettre de signaler une erreur à l’exécution.
Par contre, Astrée est incomplet à cause de la sur-approximation qui peut introduire des comportements et donc des erreurs fictives impossibles dans toutes les exécutions réelles. On parle alors de fausses alarmes. L’objectif est donc de calculer des approximations suffisamment précises pour éviter toute fausse alarme (les vraies alarmes devant conduire à une correction du code).
Astrée est paramétrable et dispose de directives d’analyses pour s’adapter aux besoins spécifiques des utilisateurs. Il peut être également facilement étendu pour inclure de nouvelles abstractions permettant d’atteindre l’objectif de précision, sans aucune fausse alarme, sur des familles précises de programmes.
Un exemple de famille de programmes pour lequel Astrée est très précis est celui des codes de contrôle commande temps réel engendrés automatiquement à partir d’une spécification synchrone de haut niveau (comme SCADE).
Qualification de l’outil
Nous offrons des kits de qualification speciales pour Astrée, qui simplifient votre processus de certification DO-178B/C, ISO 26262 ou IEC 61508.
Evaluation gratuite
Commandez votre version d’évaluation gratuite aujourd’hui ou bien contactez nos distributeurs officiels :
- en France : Antycip, Groupe Hensoldt, Massy, didier.dusclaux@hensoldt.fr, +33 (0)1 70 26 55 35
- au Canada : Joral Technologies, Ottawa, robert.campbell@joraltechnologies.com, 1-877-380-3366
- au Benelux : Indes, Culemborg, Pays-Bas, sales@indes.com, +31 (0)3 45 54 55 35
