Partenariat franco-tchèque pour le labo R&D de l’EPITA
Après avoir rejoint l’EDITE, le Laboratoire de recherche et développement de l’EPITA (LRDE) officialise désormais un partenariat avec la Faculté d’Informatique de la Masaryk University à Brno (République tchèque) dans le cadre de Spot, un des projets phares du LRDE traitant de model checking.
Spot : la solution du LRDE pour le model checking
« Le model checking, c’est vérifier qu’un modèle réponde aux contraintes qu’on lui a fixé », détaille Olivier Ricou, le responsable du LRDE, avant de poursuivre son explication avec un exemple simple. « Prenez un carrefour avec des feux de circulation : on n’a pas envie que tous les feux soient rouges ou verts en même temps. À cette première contrainte s’ajoute une seconde comme celle française qui consiste à dire que le feu fonctionne toujours dans le sens « rouge, orange, vert » et qu’il ne va jamais s’amuser à faire quelque chose comme « rouge, orange, rouge, orange, vert, vert, rouge, vert ». » Derrière cela, il y a donc « un petit programme » qui va être chargé d’allumer les couleurs qu’il faut les unes après les autres mais va également être chargé d’allumer les couleurs de chaque feu du carrefour. « S’il s’occupe d’un seul feu, on imagine bien qu’il risque d’y avoir doucement un décalage dans le temps et donc un risque de se retrouver avec tous les feux « rouges »ou « verts » en même temps », précise-t-il. Le « petit programme » en question, même s’il n’a rien de compliqué, doit donc être propre et ne comporter aucune erreur. C’est là que le model checking entre en jeu : grâce à lui et à toute une algorithmie, la vérification devient possible.
« Des calculs qui mettent à genoux les ordinateurs les plus puissants »
La bibliothèque Spot du LRDE est une des bibliothèques de model checking largement reconnue dans le monde académique. Son but ne réside pour autant pas que dans les carrefours avec des feux tricolores. Il est encore plus ambitieux. « C’est d’être capable de vérifier qu’aucun train ne circule à contre-sens sur une voie ou que toute l’électronique embarquée dans un avion ne fera jamais aucune faute – ce qu’aujourd’hui, personne n’est encore capable de mettre en œuvre, poursuit Olivier Ricou. On en est encore aux balbutiements de la vérification. L’un des utilisateurs de la bibliothèque Spot, c’est la NASA qui utilise les algorithmes de traduction de propriétés de Spot dans un de leurs outils. C’est encore un domaine de recherche ou les applications sont difficiles à mettre en œuvre car dès que les systèmes deviennent un peu réels, ils deviennent plus complexes. Cela génère alors des calculs trop lourds même pour les ordinateurs les plus puissants. »
Dans la recherche, l’union fait la force
Retenu pour le programme de recherche bilatéral franco-tchèque PHC Barrande 2014, qui a pour objectif de favoriser les échanges scientifiques et technologiques entre des laboratoires de recherche des deux pays, le LRDE va renforcer l’expérience de ses équipes travaillant sur le model checking. Olivier Ricou en a bien conscience. « Le fonctionnement de la recherche, c’est simple : les chercheurs travaillent avec d’autres chercheurs selon les affinités, explique-t-il. On écrit des articles, on va à des conférences, on y rencontre des gens, on pose des questions, on discute et, au bout d’un moment, on se dit que ça serait bien de travailler ensemble. Voilà comment a commencé l’histoire avec la Masaryk University : comme le courant passait bien et les travaux étaient complémentaires, on a fait une demande de subvention pour nos doctorants afin qu’ils puissent profiter de la synergie entre les deux équipes. » Un financement, accordé grâce au programme Barrande, va permettre de réaliser des actions de mobilité de jeunes chercheurs, de doctorants et post-doctorants. Tout ça pour développer encore davantage la bibliothèque Spot. Autant dire qu’avec ce partenariat franco-tchèque, Spot n’a pas fini de briller.