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

Les erreurs trouvées par Astrée sont :

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, ISO 26262 ou IEC 61508.

Evaluation gratuite

Commandez votre version d’évaluation gratuite aujourd’hui.


Pour de plus amples informations, veuillez voir la page anglaise, ou contactez info@absint.com.