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 à la vérification compositionnelle ou encore à la spécification de systèmes avec des extensions formelles d’UML.

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

Dernière publication

Dernière publication

Étienne André, Nguyễn Hoàng Gia et Laure Petrucci. Efficient parameter synthesis using optimized state exploration strategies. Sous la direction de Zhenjiang Hu and Guangdong Bai, (éditeurs), ICECCS’17, IEEE CPS, novembre 2017. Taux d’acceptation : 40%. À paraître. (English)

Projets de recherche

Porteur de projets

Année Appel Nom du projet Rôle Permanents Budget
2014–2018
en cours
ANR
🇫🇷
PACS
Parametric analyses of concurrent systems
Porteur 8 450k€
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€
Total 505k€

Participant à des projets

Année Appel Nom du projet Porteur Permanents Budget
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 26k€
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 pilotage

Rapporteur de thèses de doctorat

Année Doctorant Institution
2017 Wu Zhimin Nanyang Technological University, Singapour
2013 Zhu Huiquan Université Nationale de Singapour

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

Post-docs

Louis Fippo-Fitime (2017—…)

Louis Fippo Fitime Analyses paramétrées de systèmes biologiques

Doctorants

Mathias Ramparison

(2016—…)

Vérification de systèmes temps-réel paramétrés avec préemption
Co-encadrement avec Didier Lime

Nguyễn Hoàng Gia

(2015—…)

Synthèse de paramètres efficace et distribuée pour les automates temporisés paramétrés
Co-encadrement avec Laure Petrucci

Mohamed Mahdi Benmoussa

(2013—2016)

Spécification avec UML
Co-encadrement avec Christine Choppy
Situation actuelle : maître assistant à 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)

Étudiants de master

Nom Année
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

Post-doctorat

National University of Singapore

J’ai effectué de décembre 2010 à août 2011 un post-doctorat au sein de l’équipe du professeur Dong Jin Song (董劲松) à l’Université Nationale de Singapour.
Je maintiens des collaborations avec plusieurs chercheurs singapouriens.

Contact

Affiliation

Université Paris 13, LIPN, CNRS, UMR 7030, F-93430, Villetaneuse, France

Adresse postale

Étienne André
Laboratoire d’Informatique de Paris-Nord
Institut Galilée
Université Paris 13
99 avenue Jean-Baptiste Clément
93430 Villetaneuse
France

Adresse électronique

Etienne.Andre(arobase)univ-paris13.fr

Téléphone

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

Fax

…en 2017…? vraiment…?

ha-index

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