Xavier Rival : vérifier automatiquement la sûreté des logiciels critiques

Une erreur dans un logiciel peut avoir des conséquences humaines ou économiques catastrophiques, surtout s’il s’agit d’un logiciel critique comme ceux qui commandent des systèmes aéronautiques, aérospatiaux, nucléaires, médicaux ou automobiles. Comment être sûr que le logiciel s’exécutera systématiquement sans erreur ? C’est à cette question complexe que tente de répondre Xavier Rival. Et ce jeune trentenaire, normalien, a de quoi faire quand on sait que 99% des industriels vérifient leurs logiciels, tout simplement en testant tout ou partie de leur exécution des centaines de fois de suite… et en gageant que le résultat sera reproductible.

Dans l’équipe Abstraction, nous développons des méthodes d’analyse automatique de code qui permettent de vérifier l’ensemble des exécutions d’un programme en un seul calcul

Autrement dit, ces analyseurs calculent des preuves au sens mathématique. Outre l’intérêt économique – des logiciels de taille industrielle sont testés en une journée de calcul - le résultat est parfaitement fiable. C’est d’ailleurs suite à l’explosion d’Ariane 5, en 1996, due à une erreur logicielle, que les outils de vérification de logiciels ont commencé à conquérir le monde industriel. L’analyseur Astrée  a été conçu dans ce contexte, depuis 2001. Xavier Rival a participé à son développement dès sa thèse (École polytechnique) dans un laboratoire de l’École normale supérieure. De manière plus générale, ces dernières années, des progrès importants ont été accomplis, en particulier pour les logiciels qui effectuent des calculs numériques, comme ceux vérifiés par Astrée.

 Il reste beaucoup à faire pour les logiciels qui manipulent des structures de données complexes en mémoire (listes, arborescences, files d'attente).

« En revanche, on ne sait pas analyser aussi bien les nombreux logiciels embarqués, moins critiques, mais qui ont besoin de faire appel à des données complexes en mémoire, comme les logiciels de communication, de navigation, les protocoles d’échange de données... C’est l’objet de mon projet ERC »,  précise t-il. Cela permettrait d’élargir le domaine d’application de ces outils. Xavier Rival a eu l’occasion de se frotter à ces problématiques ardues depuis 2006 dans le cadre d’une collaboration avec Bor-Yuh Evan Chang, amorcée lors de son postdoc à Berkeley, puis lorsqu’il a rejoint l’institut en 2007. De bons algorithmes existaient pour rendre automatique l’analyse de logiciels effectuant des calculs numériques, en décomposant des propriétés logiques en éléments simples. Pourtant, il reste beaucoup à faire pour les logiciels qui manipulent des structures de données complexes en mémoire, que ce soit sous forme de listes, d’arborescence, de files d’attente… Cela rend les raisonnements et leur automatisation très compliqués. « Après avoir mûri mon idée pendant un an ou deux, je me sens prêt à relever le défi », conclut-il. Sa bourse ERC lui permettra de travailler avec trois doctorants, trois postdoc et un ingénieur pendant cinq ans, ainsi que d’inviter des professeurs pour des collaborations courtes.