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.

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

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.

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 :