Projet ANR-08-SEGI-0021 – U3CAT : Unification des Techniques d'Analyse de Code C Critique
Programme : Systèmes Embarqués et Grandes Infrastructures (ARPEGE) 2008
Année de financement : 2008
Coordinateur du projet : Monsieur Virgile PREVOSTO (COMMISSARIAT A L'ENERGIE ATOMIQUE - CENTRE D'ETUDES NUCLEAIRES SACLAY)
Partenaires : Entreprise autre que TPE ou PME; Entreprise autre que TPE ou PME; Commissariat à l'énergie atomique et aux énergies alternatives; Conservatoire national des arts et métiers; Entreprise autre que TPE ou PME; Entreprise autre que TPE ou PME; Inria Centre Paris - Rocquencourt; Inria Centre Paris - Rocquencourt; Inria Centre Paris - Rocquencourt; Entreprise autre que TPE ou PME
Montant : 1727730.0 euros
Durée : 36 mois
Résumé : Le logiciel embarqué est de plus en plus répandu dans la vie quotidienne. De plus les applications embarquées atteignent des tailles de plus en plus importantes, de quelques centaines de milliers de lignes de code à plusieurs millions tout en restant extrêmement critiques. Cette situation est particulièrement présente dans les systèmes utilisés dans les domaines de l'aéronautique, de l'automobile, du spatial, de la santé, et des télécommunications. Les techniques traditionnelles de validation de ces systèmes (revue de code et tests) deviennent de plus en plus difficiles à mettre en oeuvre au fur et à mesure de l'accroissement de la taille des systèmes. Il est donc nécessaire de fournir aux développeurs de ces systèmes des outils leur permettant de spécifier avec précision les propriétés attendues de l'application et de contrôler statiquement que l'implantation les vérifie effectivement. Dans ce contexte, l'analyse statique de code C joue un rôle particulièrement important, dans la mesure où une part très importante des programmes embarqués sont soit écrits directement en C, soit écrits dans un langage de plus haut niveau, comme Scade, qui utilise C comme langage intermédiaire.  Il n'y a par contre pas d''analyse miracle' qui permettrait de résoudre d'un coup tous les problèmes de vérification possible. Différentes techniques, dont les plus importantes sont le model-checking, l'interprétation abstraites et le calcul de plus faibles pré-conditions, ont chacune leurs avantages et leurs inconvénients. Il convient donc d'offrir un cadre unifié permettant d'utiliser ces différentes techniques sur un même code, et de les faire coopérer entre elles afin d'arriver à établir des propriétés qui seraient hors d'atteinte de chacune d'entre elles prise séparément. Ce point constitue l'objectif principal de U3CAT. Il se base sur les résultats du projet RNTL CAT, labellisé en 2005, qui a permis de mettre au point la plateforme d'analyse de programmes C Frama-C (http://www.frama-c.cea.fr) et le langage de spécification ACSL. Ces deux réalisations forment le socle sur lequel U3CAT s'appuiera pour développer des composantes plus précises et plus spécifiques à certains problèmes importants du monde de l'embarqué. Un certain nombre des sujets abordés dans le cadre d'U3CAT sont de nature très exploratoire, mais leur développement sera guidé par les problèmes concrets rencontrés par les industriels participants au projet, ce qui fait d'U3CAT un projet de recherche industrielle. Le projet CAT a en effet montré que ce type de partenariat était très stimulant. Un autre défi relevé par le projet U3CAT est de promouvoir l'utilisation de l'analyse statique dans les cycles de développement logiciel industriels.  Ce défi sera relevé par une collaboration étroite entre les fournisseurs d'outils, les utilisateurs industriels finaux et les sociétés de service du monde du logiciel critique.