Analyse statique d'un logiciel embarqué critique | Page personnelle

Analyse statique d'un logiciel embarqué critique

Dans le cadre d’une certification de sécurité IEC 61508, j’ai eu à effectuer l’analyse du code en C d’un contrôleur embarqué.

L’analyse a été faite avec le logiciel spécialisé Frama-C, développé par notre partenaire technologique, le laboratoire Sûreté du Logiciel du CEA-List. Frama-C est un analyseur statique de code écrit en langage C, et qui possède des propriétés logique primordiale pour valider la robustesse d’un logiciel, comme l’exhaustivité ou la correction (au sens logique).

Pour mener à bien l’analyse, il a fallu pré-processer le code, puis régler les paramètres d’analyse du logiciel, en prenant en compte les tailles de boucle et les interruptions matérielles possiblement rencontrées en cas réel par le microcontrôleur.