Analyse statique de code C critique

L’analyseur statique Astrée prouve l’absence d’erreurs à l’exécution dans les codes critiques embarqués écrits en C.

Copie d’écran d’Astrée
Copie d’écran d’Astrée

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, 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 :

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

Airbus logo

Astrée a été utilisé pour vérifier l’absence d’erreurs à l’exécution dans le logiciel de com­mande de vol électrique primaire de deux types d’avion Airbus.

Bosch

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 ».

ebm-papst logo

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.

ESA logo

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.

Helbako logo

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 logo

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éci­fiques des utilisateurs. Il peut être également facilement étendu pour inclure de nouvelles abst­ractions permettant d’atteindre l’objectif de précision, sans aucune fausse alarme, sur des fa­milles 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 en­gendré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 :