RNTL - Réseau National en Technologies Logicielles

Analyse de programmes C critiques embarqués (C Analysis Toolbox) – CAT

Résumé de soumission

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 :

* développement, afin de garantir la réutilisabilité de composants
* vérification, pour étudier la robustesse (détection d'opérations indésirables
telles que division par zéro...), pour établir la propagation des fautes et
pour établir des propriétés globales (par exemple pour une certification)
* maintenance et évolution pour mettre en évidence les liens de dépendance
(flots de contrôle, flots de données,...) pour trouver l'impact de
modificationsou aider à la compréhension du code

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 :

* d'une part d'intégrer les différentes techniques existantes (interprétation
abstraite, preuve à la Hoare, spécialisation de code) en permettant de les
faire collaborer de façon très fine. Les outils existants utilisent chacun
une technique unique et les utilisateurs industriels ayant opté pour une
technique regrettent souvent l'absence d'intégration des autres techniques ;
* d'autre part de lever les limitations habituelles concernant le fragment du
langage C traité par certains outils (traitement des casts, dépendance envers
le schéma de compilation, traitement des pointeurs de fonctions, des alias,
...) ;
* de mener des analyses sur les parties pertinentes du code (en procédant par
spécialisation). Après spécialisation, on peut appliquer des techniques qui
ne pourraient s'appliquer sur le code complet ;
* et enfin d'augmenter l'automatisation des preuves en combinant les prouveurs existants.

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

Coordinateur du projet

CEA - LIST (CEA - LIST)

L'auteur de ce résumé est le coordinateur du projet, qui est responsable du contenu de ce résumé. L'ANR décline par conséquent toute responsabilité quant à son contenu.

Partenaire

INRIA
INRIA
CEA - LIST

Aide de l'ANR 1 012 938 euros
Début et durée du projet scientifique : - 36 Mois

Liens utiles

Inscrivez-vous à notre newsletter
pour recevoir nos actualités
S'inscrire à notre newsletter