« L'Inria veut renforcer l'implication de ses équipes dans le transfert technologique », a souligné Claude Marché, directeur de recherche à l'Institut national de recherche en informatique et automatique, en présentant cette semaine le laboratoire ProofInUse. Celui-ci a été établi en commun avec l'éditeur français AdaCore qui conçoit des solutions pour le langage Ada, sous licence libre. Ce projet a pour objectif d'augmenter l'utilisation des outils de preuves mathématiques dans les activités de vérification des développements de logiciels critiques, notamment dans l'industrie aéronautique et spatiale, mais aussi dans des secteurs comme l'automobile, le transport ferroviaire ou la santé. Le recours à ces « méthodes formelles » permettrait de diminuer le coût des tests et les temps de développement des systèmes, hautement sensibles, conçus par ces industries.

La notion de contrats ajoutée dans Ada 2012

Le laboratoire commun ProofInUse est co-dirigé par Claude Marché et Yannick Moy, de la R&D d'AdaCore. Il est financé pour trois ans par l'ANR, l'agence nationale de la recherche. Lancé en avril 2014, le projet a conduit au recrutement de deux ingénieurs, en décembre et en janvier, ce qui porte son effectif à huit personnes, dont 3 chercheurs de l'Inria (à temps partiel) et 3 ingénieurs AdaCore. Voilà déjà presque 5 ans que l'éditeur de solutions pour Ada collabore avec l'institut de recherche en informatique, dans le cadre du projet Open Source Hi-Lite, visant déjà à augmenter le recours aux méthodes formelles, et d'une thèse Cifre. Les efforts conjoints de l'institut et de la PME se sont concentrés sur le langage Spark, devenu avec sa version 2014 un sous-ensemble de Ada 2012. Spark a notamment été utilisé pour iFacts, un projet d'assistance au contrôle aérien au Royaume-Uni, le plus important fait jusqu'à présent avec ce langage. Dans Ada 2012, la notion de contrats a été ajoutée. Elle permet d'exprimer les exigences de sécurité du logiciel que l'on développe (par des formules booléennes, avec des pré-conditions et post-conditions) et de les vérifier durant les tests.

ProofInUse

Rendre les preuves accessibles au-delà des mathématiciens

Pour l'instant, Spark n'a été adopté que par un petit nombre d'utilisateurs. Pour Cyrille Comar, co-fondateur et directeur général d'AdaCore, la problématique des méthodes formelles se pose comme le prochain challenge dans le développement de logiciels dans l'industrie. Parmi les industriels présents lors du lancement de ProofInUse, certains ont indiqué s'intéresser de plus en plus aux méthodes formelles tout en évoquant certains défis à relever pour les mettre en oeuvre dans les processus existants. Si les méthodes formelles resteront sans doute une niche, Claude Marché constate néanmoins que, dans les écoles d'ingénieur, les étudiants ont de plus en plus accès à des outils de preuve. « Notre objectif est de rendre les preuves faciles à utiliser pour des personnes qui ne sont pas des mathématiciens », a indiqué Cyrille Comar. « Ce sont des sujets particulièrement difficiles et qui ne sont pas finalisés en termes de recherche. » Le Comité scientifique et stratégique de ProofInUse comprend six personnes, représentant, outre l'Inria et AdaCore, l'Université de Rennes, le CEA de Saclay, Airbus Defence & Space et Dassault Aviation.