Unification des Techniques d'Analyse de Code C Critique – U3CAT

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.