Résumé du projet CAT (C Analysis Toolbox)

Analyse de programmes C issus de l'aéronautique et de l'automobile

1) Introduction

L'objectif de ce projet est de développer une boîte à outils en logiciel libre permettant d'analyser des codes de taille industrielle écrits en C pendant les phases de :


Ces activités représentent une part largement prépondérante dans le coût du développement d'un logiciel, en particulier quand celui-ci est destiné à être embarqué dans un système critique. Notre projet se propose d'aider à réduire les coûts liés à ces activités à travers la mise en place d'une infrastructure générique qui permettra une interaction des différentes techniques.


Cette infrastructure sera utilisée pour construire des outils spécialisés répondant aux besoins précis des utilisateurs industriels. Ces outils se distingueront des outils existants par la levée des restrictions quant au fragment du langage C supporté et des performances accrues. Cela sera permis par l’expérience acquise, une meilleure coopération entre chercheurs, l’évolution de la technologie et de la théorie. En particulier on s’appuiera sur des outils existants puissants de large diffusion.



Nous fournirons aussi un outil de spécialisation de logiciel intégré dans l'infrastructre globale qui permettra aux techniques qui ne s'appliquent pas bien à des codes complets génériques de donner des résultats pertinents.


Domaine concerné : vérification des systèmes embarqués critiques

Les mots clés sont : vérification, preuve, systèmes critiques embarqués, automobile, aéronautique, programmes C, interprétation abstraite, logique de Hoare, contraintes, spécialisation de code, méthodes formelles

2) Objectifs de recherche du projet

Il existe aujourd'hui une offre concernant les outils de vérification de code C (PolySpace, Astrée, Caveat, Caduceus, etc).

L'originalité de notre boîte à outils est :

Ces objectifs exigent à la fois des travaux théoriques justifiant la correction de cette approche hybride de la vérification et des travaux technologiques pointus afin de mettre en oeuvre ces techniques de façon suffisament efficace pour que la boîte à outils puisse analyser des codes de taille importante.

3) Objectifs industriels du projet

Le premier objectif est de tirer partie de la combinaison des techniques d'analyse et de spécialisation de code afin de vérifier des logiciels de taille réelle. Il s'agit de définir des méthodologies qui garantissent que l'ensemble de l'activité de vérification est cohérente et apporte des éléments de confiance dans les logiciels étudiés.

Le second objectif est de mener une réflexion sur la qualification des outils de vérification développés. C'est une étape absolument fondamentale pour pouvoir intégrer ces outils dans les chaînes de production en obtenant l'accord des organismes de certification.



4) Partenaires, compétences

Le CEA List a développé l'outil Caveat qui a été utilisé par Airbus pour la vérification en développement de parties critiques du logiciel de commande de vol de l’A380.

L’outil Caveat a aussi été utilisé par EDF pour vérifier a posteriori des logiciels déjà écrits et pour constituer des dossiers de sûreté. Cette utilisation a conduit à introduire des techniques d’interprétation abstraite pour synthétiser des propriétés qui servent à détecter des menaces.

Le CEA List a effectué pour l’IRSN des travaux exploratoires sur les applications de la spécialisation de logiciel à l’aide à la compréhension et à l’analyse d’impact pour la certification de la version n+1 d’un logiciel.


Le projet ProVal du PCRI (Université Paris-Sud, INRIA-Futurs) développe l'outil de spécification et de preuve de logiciels C Caduceus qui est experimenté dans le cadre de collaborations avec Dassault-Aviation et Axalto.


Le projet ProVal possède une grande expériences dans le développement d'outils de preuves automatiques (CiME) et interactives (Coq).


Le CEA List et le projet ProVal coopèrent pour développer une souche théorique et technique commune à leurs outils d’analyse statique et de preuve de logiciels C.


Le CEA List et l'IRISA coopèrent sur l’exploitation des techniques de résolution de contraintes pour la génération de tests et la preuve de propriétés (action V3F de l’ACI-SI).


Le CEA List coordonnera les acteurs académiques et industriels afin d'aboutir à une interaction entre les différentes techniques. Ces techniques seront développées autour d'un noyau technologique centré sur l'analyseur CIL et comportant les services de base pour garantir une possibilité d'interaction entre les différents développements. Le noyau sera distribué sous une licence libre mais chaque analyse restera la propriété de ses concepteurs.

6) Charges, coûts et aide demandée

Les frais de personnel pour l'ensemble du projet sont de : 311 hommes*mois.

Le coût global, tout compris, de l'ensemble du projet a été estimé à 3 476 800 Euros.

L'aide globale demandée pour l'ensemble du projet est de 1 184 251 Euros.