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

CosyVerif: The Path to Formalisms Cohabitation

Dernière publication

Étienne André, Jaime Arias, Benoît Barbot, Francis Hulin-Hubard, Fabrice Kordon, Van-François Le et Laure Petrucci. CosyVerif: The Path to Formalisms Cohabitation. Sous la direction de Lars Michael Kristensen and Jan Martijn van der Werf (éditeurs), PetriNets’24, Springer LNCS, juin 2024. À paraître. (English)

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 CNRSPAN
🇫🇷 🇵🇱
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

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

Expert scientifique

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.

Étudiants

Doctorants

Dylan Marinho

(2020-2023)

Dylan Marinho Détection d’attaques temporisées à l’aide de méthodes formelles

Jawher Jerray

(2018-2021)

Jawher Jerray Analyses formelles de systèmes temps-réel
Co-encadrement avec Laurent Fribourg

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 à 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 : ingénieur R&D chez Thales (France)

Post-docs

Laetitia Laversa (2023-…)

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

Étudiants de master

Nom Année
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, LIPN, CNRS UMR 7030, 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.