Je m’intéresse à la spécification et à la vérification formelle de systèmes distribués, notamment temporisés. Ma recherche porte particulièrement sur la vérification de systèmes temporisés (voire temps-réel) en présence de paramètres temporels, et notamment au model-checking paramétré. Je m’intéresse également au monitoring de systèmes cyber-physiques, ainsi qu’à la détection d’attaques par canaux cachés à l’aide de model-checking quantitatif.

Mots-clés : model-checking, vérification, systèmes concurrents et distribués, systèmes temporisés, automates temporisés paramétrés, synthèse de paramètres.

Derniers travaux

Verifying Timed Properties of Programs in IoT nodes using Parametric Time Petri Nets

Dernière publication

Étienne André, Jean-Luc Béchennec, Sudipta Chattopadhyay, Sébastien Faucou, Didier Lime, Dylan Marinho, Olivier H. Roux et Sun Jun. Verifying Timed Properties of Programs in IoT nodes using Parametric Time Petri Nets. Sous la direction de Justyna Petke, Anton Wijs, Juw Won Park and Adam Przybylek (éditeurs), SAC’25, ACM/IEEE, mars 2025. À paraître. (English)

Tuning Trains Speed in Railway Scheduling

Dernier exposé

4 décembre 2024 : Tuning Trains Speed in Railway Scheduling (ICFEM’24, 🇯🇵 Hiroshima)

Projets de recherche

Porteur de projets

Année Appel Nom du projet Rôle Membres Budget
2024
en cours		 PHC Polonium
🇫🇷 🇵🇱 		MoCcA
Analyses of multi-agent systems		 Porteur 6 3k€ (*2)
2020–2024
en cours		 ANR-NRF
🇫🇷 🇸🇬 		ProMiS
Provable Mitigation of Side Channel through Parametric Verification		 Porteur 5 276k€ (*2)
2020 IFD
🇫🇷 🇩🇰 		SECReTS
Synthesis of Energy-optimal Constraints for REal-Time Systems		 Porteur 4 3k€
2014–2019 ANR
🇫🇷 		PACS
Parametric analyses of concurrent systems		 Porteur 8 450k€
2018 DIM RFSI
🇫🇷 		ASTREI
Analyse de systèmes temps-réel modélisés par Time4sys en présence d’incertitude		 Porteur 1 10k€
2014–2015 CNRS–PAN
🇫🇷 🇵🇱		 BehaPPi-BMC
Behavior preserving parametric bounded model checking		 co-porteur 4 8k€
2014 BQR
🇫🇷		 SynPaTiC
Synthèse de paramètres temporels distribuée et multi-cœurs		 Porteur 2 15k€
2013 Actions émergentes GDR GPL
🇫🇷		 IOP
Intégration d’outils à la plate-forme CosyVerif		 Porteur 1 2k€
2012–2014 PHC Merlion
🇫🇷 🇸🇬		 BRAVOS
Software Verification from Design to Implementation		 co-porteur 6 30k€

Participant à des projets

Année Appel Nom du projet Porteur Membres Budget
2023–2027 ANR
🇫🇷		 BisoUS Didier Lime 15 409k€
2018–2019 ERATO
🇯🇵		 MMSD
Metamathematics for Systems Design		 Ichiro Hasuo (蓮尾 一郎) >20 10000k€
2019–2020 PICS
🇫🇷 🇵🇱		 PARTIES
verification of PARametric TIme constrained strategic abilitiES for agents acting under incomplete information		 Laure Petrucci 7 8k€
2018–2019 PHC Van Gogh
🇫🇷 🇳🇱		 PAMPAS
Parallel algorithms for model-checking and parameter synthesis		 Laure Petrucci 11 7k€
2018 BQR
🇫🇷		 AMoJAS
Arbres attaque-défense et Modèles de Jeux pour l’Analyse de la Sécurité		 Laure Petrucci 7 6k€
2015 PEPS JCJC
🇫🇷		 PSyCoS
Parallel SYnthesis for COncurrent Systems		 Camille Coti 2 10k€
2013–2014 STIC Asie
🇫🇷 🇸🇬 🇻🇳		 CATS
Compositional analysis of timed systems		 Laure Petrucci 6 34k€
2013 PHC Merlion
🇫🇷 🇸🇬		 FSFMA
French Singaporean Workshop on Formal Methods and Applications		 Christine Choppy + Sun Jun 9 8k
2010 PHC Galilée
🇫🇷 🇮🇹 		Synthèse et contraintes Laurent Fribourg 3 12k€
2007–2010 ANR
🇫🇷 		VALMEM
Validation fonctionnelle et temporelle des mémoires embarquées, décrites au niveau transistor, par des méthodes formelles		 Laurent Fribourg 7 572k€
2007–2009 Institut Farman
🇫🇷 		SIMOP
Simulation et model-checking paramétré		 Laurent Fribourg 6 20k€

Comités de programme et évaluations

Comités de programme

2026
2025
2024
2023
2022
2021
2020
2019
2018
2017
2016
2015
2014
2013

Comités de pilotage

Organisation de congrès

Rapporteur de thèses de doctorat

Année Doctorant⋅e Institution
2024 Yushi Cao Nanyang Technological University, Singapour 🇸🇬
2024 Tomáš Kolárik Czech technical university in Prague 🇨🇿
2023 Akshay Mambakam Université Grenoble Alpes 🇫🇷
2022 Bastien Serée École Centrale Nantes Drapeau Bretagne, France
2021 Léo Henry Université de Rennes 1 Drapeau Bretagne, France
2020 Clément Bertrand Université d’Evry, Université Paris-Saclay 🇫🇷
2020 Victor Roussanaly Université de Rennes 1 Drapeau Bretagne, France
2020 Jiao Jiao Nanyang Technological University, Singapour 🇸🇬
2019 Du Xiaoning Nanyang Technological University, Singapour 🇸🇬
2018 Wang Junjie Nanyang Technological University, Singapour 🇸🇬
2018 Chandramohan Mahinthan Nanyang Technological University, Singapour 🇸🇬
2017 Wu Zhimin Nanyang Technological University, Singapour 🇸🇬
2013 Zhu Huiquan Université Nationale de Singapour 🇸🇬

Expert scientifique

Année Institution
2020 🇯🇵 EIG CONCERT-Japan
2015, 2016 🇫🇷 Agence nationale de la recherche
2014 🇳🇱 Nederlandse Organisatie voor Wetenschappelijk Onderzoek

Développement logicel

Behavioral cartography by IMITATOR

IMITATOR : synthèse de paramètres pour les systèmes temps-réel

J’ai créé l’outil IMITATOR en 2008, et suis depuis son principal développeur.

IMITATOR est un logiciel pour synthétiser des valeurs de paramètres temporels dans les systèmes temporisés concurrents modélisés par des extensions des automates temporisés paramétrés.

IMITATOR a été utilisé dans le cadre de plusieurs collaborations avec l’industrie, notamment pour la vérification de systèmes matériels et pour l’analyse d’ordonnancement en présence d’incertitude.

Un langage d’entrée expressif

IMITATOR effectue de la synthèse de paramètres pour les systèmes temps-réel modélisés par une extension des automates temporisés paramétrés.

Des analyses puissantes

Plusieurs algorithmes sont implémentés dans IMITATOR, dont la synthèse pour la sûreté, l’absence de deadlocks, le model-checking paramétré non-Zeno, ou encore l’analyse de robustesse.

Sorties graphiques

En plus des sorties normalisées, IMITATOR génère des sorties graphiques tells que les zones de bon fonctionnement des paramètres temporels.

Autres outils logiciels

PAT

Membre de l’équipe de développement (2010-2013)

PAT est un model-checker puissant pour de multiples formalismes, dont timed CSP, les systèmes probabilistes, les systèmes paramétrés… PAT est principalement développé à Singapour (NUS, STUD, NTU).

PolyOp

Développeur

PolyOp est une interface simple pour encapsuler des opérations sur les polyèdres fournies par la bibliothèque PPL (Parma Polyhedra Library).

PSyHCoS

Développeur

PSyHCoS est un outil de synthèse de paramètres pour l’algèbre de processus Parametric Stateful Timed CSP (PSTCSP).

HyMITATOR

Développeur

HyMITATOR est une variante d’IMITATOR pour les automates hybrides paramétrés.

InSPEQTor

Développeur

InSPEQTor est une implémentation de la méthode inverse pour les graphes orientés valués paramétrés.

ImpRator

Développeur

ImpRator est une implémentation de la méthode inverse pour les processus de décision markoviens paramétrés.

Étudiant⋅e⋅s

Doctorants

Sarah Dépernet

(2024-…)

Vérification de propriétés de cybersécurité à l’aide de méthodes formelles
Co-encadrement avec Engel Lefaucheux

Dylan Marinho

(2020-2023)

Dylan Marinho Détection d’attaques temporisées à l’aide de méthodes formelles
🏆 Prix de thèse 2024 de l’Académie Lorraine des Sciences (France)
Situation actuelle : maître de conférences à Sorbonne Université (France)

Jawher Jerray

(2018-2021)

Jawher Jerray Analyses formelles de systèmes temps-réel
Co-encadrement avec Laurent Fribourg
Situation actuelle : maître de conférences à Université de Pau (France)

Mathias Ramparison

(2016-2019)

Vérification de systèmes temps-réel paramétrés avec préemption
Co-encadrement avec Didier Lime
Situation actuelle : maître de conférences à l’INP Grenoble et Verimag

Nguyễn Hoàng Gia

(2015-2018)

Nguyễn Hoàng Gia Synthèse de paramètres efficace et distribuée pour les automates temporisés paramétrés
Co-encadrement avec Laure Petrucci
Situation actuelle : Post-doc au CEA (France)

Mohamed Mahdi Benmoussa

(2013-2016)

Mahdi Benmoussa Spécification avec UML
Co-encadrement avec Christine Choppy
Situation actuelle : maître de conférences à l’École Nationale Polytechnique de Constantine (Algérie)

Romain Soulat

(2010-2013)

Romain Soulat Synthèse d’ordonnanceurs corrects par construction pour les systèmes hybrides
Co-encadrement avec Laurent Fribourg
Situation actuelle : Technical Lead for Certification, Input Output

Post-docs

Emily Clement (2024-…)

Monitoring de systèmes cyber-physiques

Laetitia Laversa (2023-2024)

Contrôle de l’opacité dans les systèmes temporisés
Co-encadrement avec Marie Duflot, Engel Lefaucheux

Johan Arcile (2020-2022)

Johan Arcile Détection de failles temporelles avec des méthodes formelles
Situation actuelle : maître de conférences à l’Université Paris-Saclay

Étudiant⋅e⋅s de master

Nom Année
Sarah Dépernet 2024
Shapagat Bolat 2022
Aleksander Kryukov 2020
Jawher Jerray 2018
Sahar Mhiri 2018
Mathias Ramparison 2016
Nguyễn Hoàng Gia 2014
Christopher Makanga 2014
Mohamed Mahdi Benmoussa 2013
Taieb Ben Niha 2013
Giuseppe Pellegrino 2012−2013
Shweta Garg (श्वॆता) 2012
Inès Jguirim 2012
Daphné Dussaud 2010
Sandeep Grewal 2008

Parcours universitaire

Un peu de responsabilité environnementale

Et si on partait en congrès en train…?

Le monde en train, ou tout pour assister aux congrès européens et asiatiques en train !

Contact

Affiliation

Université Sorbonne Paris Nord, CNRS, Laboratoire d’Informatique de Paris Nord, LIPN, F-93430 Villetaneuse, France

Adresse postale

Étienne André
Institut Galilée
LIPN
Université Sorbonne Paris Nord
93430 Villetaneuse
France

Adresse électronique

Etienne.Andre（arobase）lipn.fr

Téléphone

Il est préférable de m’envoyer un courriel d’abord

Fax

…en 2024…? vraiment…?

ha-index

Je suis très fier d’avoir un ha-index de 78.