Sites Inria

English version

Partenariat industriel

Médiathena - CD - 17/10/2019

Prix FIEEC Carnot de la Recherche Appliquée : Claude Marché ''fait ses preuves''

De gauche à droite : Claude Marché de l'équipe Toccata, et Arnaud Charlet, responsable ingénierie produit d'AdaCore - © Inria - S.Gitton

Le 17 octobre 2019 à Paris, le chercheur Claude Marché, directeur de l'équipe de recherche Toccata du centre Inria Saclay - Île-de-France, a reçu le premier prix FIEEC Carnot de la Recherche Appliquée 2019 . Il récompense une coopération de longue date avec l'éditeur français de logiciels libres AdaCore , spécialisé dans la fourniture d'outils de développement et de vérification de logiciels. Entretien avec l'intéressé et Yannick Moy, ingénieur R&D chez AdaCore .

Pourquoi cette récompense et que représente-t-elle pour vous ?

Claude Marché  : Je suis honoré par ce prix qui récompense les partenariats de recherche appliquée menées avec un industriel ayant eu un réel impact économique. Nous avons conduit depuis 2010 avec la société AdaCore , un certain nombre de recherches sur la vérification déductive de programmes. Le prix est nominatif, mais à mon sens l'équipe Toccata et la société AdaCore mériteraient aussi d'être distinguées et récompensées.

Yannick Moy  : Avant de rejoindre AdaCore , j'ai fait partie d’équipe Inria ProVal dans laquelle travaillait Claude qui fut mon directeur de recherche, entre 2006 et 2009. Lorsque j'ai rejoint cet éditeur, j'ai rapidement proposé de remplacer la partie "preuve" de la solution utilisée à l'époque par la technologie open source Why3 (anciennement Why ) développée par Inria. Cela a été suivi d’un partenariat industriel donnant lieu à des collaborations multiples dans le cadre de projets coopératifs soutenus par les pôles de compétitivité, puis par la création d'un laboratoire commun (ProofInUse ) financé par l'Agence nationale de recherche (ANR) entre 2014 et 2017. Nous avons depuis signé un contrat de coopération bilatérale, qui court jusqu'en 2022, en vertu duquel AdaCore finance en partie les travaux de recherche de Toccata.

Qu'est-ce que la preuve informatique ?

C.M.  : Plusieurs équipes Inria se sont historiquement intéressées à ce sujet. Au niveau de Toccata, notre originalité est d'avoir décidé d'utiliser les techniques de preuve pour valider des programmes informatiques . Concrètement, les preuves de mathématiques sur des logiciels démontrent qu'ils réalisent bien ce qu'ils sont censés faire et qu'ils répondent à tous les critères de sûreté de fonctionnement définis par l'entreprise. Jusqu'ici, la méthode la plus courante consiste à effectuer des tests : cette technique est efficace mais elle est forcément limitée dans son périmètre et elle est coûteuse. Lorsque l'on "fait la preuve", on peut au contraire tester le programme dans le maximum de configurations possible . Nous avons ainsi développé un mécanisme qui permet d'exprimer mathématiquement l'ensemble des configurations possibles pour un programme et de vérifier qu'il s'exécute à chaque fois conformément à ce que souhaite l'utilisateur.

Y.M.  : Nous avons intégré plusieurs logiciels développés par l'équipe-projet Toccata au sein de notre environnement de vérification logicielle SPARK . En tant qu'industriel de l'open source , la preuve de programme nous aide à donner des garanties aux utilisateurs des logiciels que nous concevons  : ces sociétés – par exemple Airbus , Altran ou Nvidia – nous rémunèrent pour le support de la plate-forme et pour notre capacité à les aider à utiliser nos logiciels de façon ultrasécurisée.  

Qui sont les utilisateurs de ce type de technologies ?

C.M . : Beaucoup d'entreprises du secteur de l'aéronautique et des transports sont depuis longtemps intéressées : elles emploient des logiciels pour lesquels la fiabilité, l’efficacité et la sécurité sont critiques. Elles dépensent donc déjà beaucoup d'argent dans les tests de logiciels ; certaines d'entre elles espèrent optimiser leurs investissements grâce à des technologies de preuve. Notre partenariat avec AdaCore nous permet de développer des applications pour ces secteurs, et donc de faire en sorte que nos recherches, forcément très théoriques, aient des retombées concrètes dans l'industrie .

Y.M.  : Il s'agit d'une technologie de pointe, qui suscite de plus en plus d'intérêt en dehors de l'avionique ou du ferroviaire : elle intéresse aujourd'hui des constructeurs de voitures autonomes, des spécialistes de la sécurité, des acteurs des appareillages médicaux ou des fournisseurs de services de cloud computing . Les entreprises de ces secteurs ont, elles aussi, des impératifs de sûreté afin d'éviter qu'une erreur ou qu’une attaque délibérée ne mette en danger la vie de leurs utilisateurs. Il s’agit par exemple d’assurer l'absence de failles de sécurité des plates-formes embarquées dans ces voitures ou implémentées dans des humains, tout en permettant de les connecter à des réseaux comme Internet. À nous de comprendre leurs besoins et de les partager avec Inria pour que nous puissions avancer ensemble sur les aspects les plus complexes.

Quels sont vos objectifs pour l'avenir ?

C.M.  : J'espère diversifier notre écosystème de partenaires, par exemple en travaillant avec d'autres éditeurs d'outils de programmation et de logiciels critiques destinés à d'autres secteurs d'activité. D'un point de vue académique, mon rêve est que nous réussissions à ce que les outils de preuve de programmes puissent être de plus en plus utilisés tout au long du cycle de conception  : la preuve se ferait en même temps que le développement du logiciel et la prise en compte de la sûreté serait donc beaucoup plus précoce.

Y.M.  : Du côté d’AdaCore , notre principale tâche sera de développer les briques technologiques permettant de faciliter l'utilisation des techniques de preuve.

Prix FIEEC Carnot de la recherche appliquée 2019

Le concours, qui tient sa neuvième édition en 2019, récompense des chercheurs ayant mené, avec une PME ou une entreprise de taille intermédiaire (ETI) « un partenariat de recherche ayant eu un réel impact économique » . Il est organisé par la Fédération des industries électriques, électroniques et de communication (FIEEC), qui rassemble 29 organisations professionnelles, et l’Association des instituts Carnot, qui réunit 38 laboratoires publics labellisés par le ministère de la Recherche, dont Inria, et valorise leur engagement dans la recherche partenariale avec des entreprises.

Claude Marché en bref

Après un parcours d'enseignant-chercheur à l'Université Paris-Sud (entre 1995 et 2006), Claude Marché a rejoint Inria en 2006 pour se consacrer à 100 % à la recherche sur la preuve de programmes. Il dirige depuis 2012, l'équipe-projet Toccata commune à Inria Saclay Ile-de-France et l'Université Paris-Sud. Elle travaille au développement de la preuve assistée par ordinateur dans le développement de logiciels qui exigent des garanties élevées en matière de sécurité et de conformité vis-à-vis du comportement prévu.

Mots-clés : Partenariat industriel Programmation Démonstration automatique Vérification déductive de programmes Logiciels et architectures

Haut de page

Suivez Inria