Étienne André : une chaire sur la vérification formelle des systèmes cyber-physiques

En 1996, la fusée Ariane 5 explose en plein vol seulement 36 secondes après son décollage. La cause : une faute oubliée parmi les milliers de lignes de codes de son système de guidage. Cet exemple illustre comment la moindre erreur informatique peut avoir de graves conséquences physiques et économiques. Les éviter est d’autant plus nécessaire que notre société regorge de ces systèmes, à l’image des lignes automatiques du métro parisien. Mais contrairement à la fusée partie en fumée, ces lignes sont parmi les rares au monde à être certifiées par des méthodes formelles. 

Ces techniques mathématiques permettent de vérifier et d’assurer le bon fonctionnement de systèmes avant leur mise en œuvre. Mais encore faut-il avoir des formalismes, c’est-à-dire des représentations mathématiques, adaptées au système à vérifier. C’est là qu’interviennent les recherches d’Étienne André, professeur à l’Université Sorbonne Paris Nord et membre du Laboratoire d'Informatique de Paris-Nord (LIPN - CNRS/Université Sorbonne Paris Nord).

Dans le cadre de sa nomination sur une chaire fondamentale de l’Institut universitaire de France (IUF), il développera et adaptera des méthodes automatiques pour s'assurer que des systèmes cyber-physiques - indépendamment de leur nature - fonctionnent correctement lorsqu’ils sont soumis à des contraintes d'énergie et de temps. « Le temps est important pour de nombreuses applications, comme les transports autonomes. Dans le cas du métro, il y a des contraintes temporelles sur la durée du trajet entre les stations, la durée d’ouverture des portes, etc. Notre société fait également face à des contraintes énergétiques de plus en plus fortes qui nous invitent à développer des systèmes plus économes », explique le scientifique du LIPN.

Une particularité de son projet est son approche paramétrée. Elle consiste d’abord à identifier des formalismes à même de s’attaquer à des problèmes mêlant des contraintes de temps et d’énergie, puis à concevoir un algorithme de manière flexible en définissant certains aspects sous forme de paramètres, ici temporels ou énergétiques, dont on ne connaît pas encore les valeurs. « Notre vérification apporte alors des réponses sur les meilleures valeurs temporelles et énergétiques nécessaires pour que les propriétés générales de notre système soient vérifiées (absence de collision, durée maximale de trajet de 30 minutes, etc.) », décrit Étienne André. Cela lui permettra ensuite d'adapter la même méthode à différents cas d'utilisation, à des environnements variés ou de permettre des variations du système à l’exécution sans remettre en cause sa correction.

Un autre axe de son projet se concentre sur des approches de vérification légère (ou monitoring) toujours sous des contraintes de temps et d’énergie. Ici, l’application principale est le véhicule autonome ou semi-autonome. « Il est impossible de vérifier ces systèmes formellement dans leur intégralité avec les méthodes existantes. Ces véhicules évoluent dans un environnement complexe (code de la route, autres véhicules, piétons, etc.) et ils s’appuient sur des méthodes d’intelligence artificielle qui ne sont pas toujours explicables », précise Étienne André. L’enseignant-chercheur proposera donc des outils de vérification légère sur des logs, des fichiers ayant enregistré les actions effectuées par un véhicule.

De là, l’enjeu sera de vérifier des propriétés quantitatives, notamment sur le temps et l’énergie, par exemple : le véhicule a-t-il réalisé trop de changements de vitesse qui pourraient nuire au confort des passagers ? A-t-il eu une consommation d’énergie importante alors que la vitesse était réduite ? Le véhicule est ainsi vérifié sur un temps de fonctionnement long afin de réduire au maximum les bugs logiciels et de renforcer la sécurité.