Étienne André a rejoint l’équipe Mosel-Véridis (département 2 : Méthodes formelles) au Loria en septembre dernier en tant que professeur à l’université de Lorraine. Enseignant à l’IUT Charlemagne, sa recherche porte sur la vérification des systèmes en particulier sur le « temps-réel ». Son portrait en quelques questions.
Sur quelle thématique scientifique travaillez-vous ?
Je travaille sur la vérification des systèmes informatiques des machines, afin qu’elles effectuent correctement les tâches que le programmeur lui a assignées. À l’aide de méthodes formelles, techniques rigoureuses utilisant la logique mathématique, je mets en place des procédés qui me permettent d’obtenir l’assurance qu’il n’y aura pas de dysfonctionnement ou de bug dans le logiciel ou le système. Pour vous donner un exemple, certains aéronefs sans-pilote (« drones ») peuvent réaliser une partie de leur mission, mettons la capture d’images, de façon entièrement automatisée. Mon travail permettra de vérifier via une procédure précise et automatisée que le protocole utilisé par cette mission, ici la capture d’images, fonctionne conformément à sa spécification. Je m’intéresse particulièrement aux aspects dits temps-réel, par exemple que la capture d’images se fait à une vitesse donnée, et qui ne soit pas trop rapide pour par exemple un traitement ultérieur par le processeur.
Je fais principalement de la recherche théorique, avec un intérêt fort pour les systèmes quantitatifs, à savoir des quantités telles que durée temporelle, mais aussi coût financier, humain, énergétique. Et j’étudie l’impact de ces types de quantités sur la difficulté de vérifier de tels systèmes. Je m’intéresse tout particulièrement aux « systèmes temps-réel », c’est-à-dire aux systèmes soumis à des contraintes temporelles fortes. Prenons pour exemple l’atterrissage d’un avion. Pour ce faire, l’appareil émet des signaux entre lui et l’aéroport pour déterminer à quelle distance se trouve la piste d’atterrissage. Le temps de réponse entre l’envoi d’un signal par l’avion et sa réception de la réponse de l’aéroport déterminera à quelle distance est l’appareil de la piste. En fonction des résultats, l’avion va donc adapter sa vitesse car en amont nous lui avons donné un protocole à suivre. Il s’agit donc d’un système temps-réel car un retard dans la réponse de l’aéroport va avoir un impact sur la connaissance par l’avion de sa position, et peut donc avoir des conséquences dramatiques.
Quel a été votre parcours d’études et professionnel ?
Après quelques années d’étude comme élève-ingénieur à l’INSA de Rennes, j’ai souhaité poursuivre un Master 2 recherche, Université de Rennes 1 en 2007. Je rejoins le LSV (Laboratoire Spécification et Vérification) de l’ENS Cachan, aujourd’hui ENS Paris-Saclay pour préparer mon doctorat sur l’« Analyse de systèmes temporisés paramétrés » dans le cadre d’un projet ANR « VALMEM » avec ST-Microelectronics. Je décide de m’envoler une année à Singapour, à la NUS, Université Nationale pour faire un post-doctorat sur la « Vérification à l’aide d’algèbres de processus ». En 2011, je rentre en France et j’obtiens le concours pour être Maître de conférences à l’Université Paris 13. J’y fais ma recherche au sein de l’équipe LoVe (Logique et vérification) du LIPN (Laboratoire d’Informatique de Paris Nord) et je me spécialise dans la vérification de systèmes cyber-physiques. En septembre 2019, je rejoins donc le Loria et la suite reste à écrire.
Quels sont vos projets actuels et à venir ?
Je souhaite poursuivre mes travaux sur la supervision de systèmes cyber-physiques, à savoir la vérification d’une exécution donnée. La supervision offre moins de garanties que la vérification formelle, car elle ne vérifie qu’une seule exécution, et non toutes les exécutions possibles. Néanmoins, elle offre un compromis intéressant entre les garanties offertes et la taille des systèmes que l’on peut vérifier. Ces travaux se feront en collaboration avec le projet ERATO MMSD à Tokyo, mais aussi en collaboration avec les nouveaux collègues de mon équipe du Loria. Par ailleurs, je suis porteur d’un nouveau projet international ANR-NRF* nommé ProMis d’une durée de 3 ans, impliquant le Loria (Nancy), le LS2N (Nantes), et deux partenaires singapouriens. Ce projet a pour ambition d’appliquer les méthodes formelles à la détection de faille de sécurité dans les programmes informatiques, notamment dues aux aspects temporels, et de parer au risque de piratage. Une collaboration potentielle pourrait se faire avec des membres de l’équipe PESTO du même département que mon équipe Mosel-Véridis .
*Agence Nationale de la Recherche (France) – National Research Foundation (Singapour)