Jean-Michel Ilié

(+33) 01 40 39 03 08
jean-michel.ilie (at) lip6.fr

Thèmes de recherche :

Mes recherches concernent l'analyse des systèmes informatiques distribués et des systèmes embarqués. Il s'agit d'améliorer ou d'adapter les techniques d'analyse largement répandues, comme la vérification de propriétés de logique temporelle ou l'évaluation stochastique des performances des systèmes, pour traiter les systèmes concrêts, souvent complexes et de très grande tailles.
Des techniques complémentaires de réduction et de compression d'espace d'états ont été définies tels que l'exploitation des symétries de fonctionnement des processus, l'observation partielle des composantes du système et le codage symbolique des infomations conservées en mémoire.
Les approches proposées ont été mises en pratique pour des systèmes distribués décrits en réseaux de Petri. La version colorée de ces réseaux (dite symétrique) a permi d'automatiser le calcul des symétries de façon particulièrement efficace. Les réseaux de Petri récursifs temporels représentent une toute nouvelle extension qui offre aux concepteurs la création dynamique de processsus communiquants et une gestion temporisée de leurs événements. Les premiers travaux ont permi d'exhiber des conditions suffisantes pour une analyse d'accessibilité des états.
J'élabore aussi des méthodes formelles permettant d'évaluer la robustesse des circuits embarqués plongés dans des environnements satellitaires perturbés.

Mots clefs : model checking, logique temporelle, évaluation stochastique, graphe d'état quotient, chaîne de Markov aggrégée, représentation symbolique, symétrie, observation, modularité, réseau de Petri, système à structure dynamique, système fini et infini, influence de l'environnement.

• Projet en cours
  ANR FME3

Sélection sur mes publications

• S. Baarir, E. Encrenaz, J-M. Ilié, I. Mounier, D. Poitrenaud et al Quantifying Robustness by Symbolic Model checking, HWVW10 - 1st Hardware verification Workshop, associated with CAV 2010, Edimboug, Juillet 2010.
• S. Haddad, J-M. Ilié, Symmetry and Temporal Logic , Livre: Petri Nets - Fundamental models, Verification and Applications, Chapitre 14, direction Diaz, editeur ISTE Wesley, pg435-460, Aout 2009.
• D. Dahmani, J-M. Ilié, M. Boukala, Reachability analysis for Recursive Petri Nets with shared places, APNOC - Abstractions for Petri Nets and Other Models of Concurrency, LNCS 5606, juin 2009.
• D. Dahmani, J-M. Ilié, M. Boukala, Time Recursive Petri Nets - revisited, Revue TopNoc - Transactions on Petri Nets and Other Models of Concurrency , LNCS, pp104-118, novembre 2008.
• J-M. Ilié, Y- Thierry-Mieg, S. Baarir , Vérification efficace des systèmes finis, Livre : Modèle formel pour les systèmes coopératifs chapitre 8 (35 pages), Editeur Hermes - Lavoisier – collection informatiques et système d'information, octobre 2006.
• K. Klai, S. Haddad, J-M. Ilié , Modular Verification of Petri nets Properties: a Structure-based Approach, pourr la 25ème conférence internationale IFIP "Formal Techniques for Networked and Distributed Systems - FORTE'05", Taïwan, Octobre 2005.
• B. Soheib, C. Dutheillet, S. Haddad, J-M. Ilié, On the use of exact lumpability in partially symmetrical Well-formed Nets, pour la 2ème conférence internationale IEEE "Quantitative Evaluation of Systems - QEST’05", Turin, Italie, pages 23-32, Septembre 2005, 'Best paper award'.
• S. Haddad, J-M. Ilié, K. Klai, Design and Evaluation of a Symbolic and Abstraction-Based Model Checker, pour la 2ème conférence internationale IEEE "Automated Technology for Verification and Analysis", Taipei, Taïwan, volume LNCS 3299, pg 196-210, novembre 2004.
• Y. Thierry-Mieg, J-M. Ilié, D. Poitrenaud, A Symbolic Symbolic State Space Representation, pour la conférence internationale IFIP " Formal Techniques for Networked and Distributed Systems - FORTE 2004", Madrid, Espagne, volume 3235, pg 276-291, septembre 2004.