Research activity

Les thèmes principaux de mes activités de recherche sont la modélisation, la vérification et le contrôle distribué de systèmes complexes.

Modélisation - Vérification

Mes recherches dans le cadre du projet FME3 commun avec le laboratoire TIMA et l'équipe ALSoC du LIP6 ont consisté en l'étude de la robustesse de circuits et plus particulièrement leur capacité "d'auto-réparation". Nous avons formellement défini un modèle de faute, un modèle d'injection des fautes et une métrique permettant de quantifier le caractère auto-réparant d'un circuit. Pour un circuit robuste, nous quantifions le "temps" nécessaire à sa réparation, pour un circuit non robuste nous identifions leur niveau de robustesse.

Une autre orientation de mes recherches dans cette thématique est de confronter les modèles formels que nous utilisons (et les théories et outils de vérification associés) à des problèmes qui sortent du domaine d'application habituel de nos études soit parce que le modèle présente a priori des spécificités que nous ne traitons pas, soit parce que les propriétés à vérifier ne sont pas exprimées assez formellement pour identifier l'outil de vérification à utiliser ou alors ne peuvent pas a priori être vérifiées telles quelles par les outils usuels. En identifiant un cas d'étude (représentatif d'un domaine d'application si possible) et en le modélisant formellement avec nos modèles nous pouvons alors identifier les problèmes particuliers qui se posent (ceux que nous pouvons résoudre et ceux qui nécessitent une évolution des modèles et/ou méthodes de vérification). Un objectif étant bien sûr de faire évoluer les modèles/outils si nécessaire et si possible. Une telle étude a été débutée dans le cadre du projet LIP6 « Serious Games et Modèles Formels » avec l'équipe Mocah du LIP6 ont le but est d'identifier des règles de construction d'un réseau de Petri pour la modélisation d'un serious game et d'identifier les propriétés attendues d'un serious game qui peuvent être vérifiées par model-checking à partir du réseau de Petri.

Contrôle distribué

Les travaux auxquels j'ai participé jusqu'à présent sur le contrôle distribué concernent essentiellement l'aspect théorique du problème : déterminer l'existence d'un contrôleur distribué pour une classe de système est-il décidable ou non ? Dans quels cas est-il possible de prouver l'existence d'un contrôleur distribué si nous savons qu'il en existe un centralisé ? Mes recherches actuelles considèrent le problème d'un point de vue plus « pragmatique » : le modèle formel du système que l'on souhaite contrôler. Nous cherchons à déterminer si le système est contrôlable et/ou sous quelles conditions un contrôleur distribué existe.

1994-2020 Publications

• 2020
  • M. Jaume, M. Journault, M.‑J. Lesot, P. Manoury, I. Mounier : “Logique pour l’informatique”, (Ellipses), (ISBN: 9782340042612) (2020)
• 2014
  • A. Yessad, I. Mounier, J.‑M. Labat, F. Kordon, Th. Carron : “Have you found the error? A Formal Framework for Learning Game Verification”, 9^th European Conference on Technology Enhanced Learning, vol. 8719, Lecture Notes in Computer Science, Graz, Austria, pp. 476-481, (Springer) (2014)
  • A. Yessad, I. Mounier, Th. Carron, F. Kordon, J.‑M. Labat : “Formal Framework to improve the reliability of concurrent and collaborative learning games”, EAI Endorsed Transactions on Serious Games, vol. 14 (2), pp. e4, (ICST) (2014)
• 2013
  • Th. Carron, F. Kordon, J.‑M. Labat, I. Mounier, A. Yessad : “Toward Improvement of Serious Game Reliability”, 7^th European Conference on Games Based Learning, vol. 2, Porto, Portugal, pp. 80-87, (Academic Conferences and Publishing International) (2013)
• 2011
  • S. Baarir, C. Braunstein, E. Encrenaz, J.‑M. Ilié, I. Mounier, D. Poitrenaud, S. Younes : “Feasibility Analysis for Robustness Quantification by Symbolic Model Checking”, Formal Methods in System Design, vol. 39 (2), pp. 165-184, (Springer Verlag) (2011)
  • C. Dutheillet, I. Mounier, N. Sznajder : “Distributed Control”, chapter in Models and Analysis in Distributed Systems, pp. 307-351, (Wiley), (ISBN: 9781848213142) (2011)
• 2010
  • S. Baarir, C. Braunstein, E. Encrenaz, J.‑M. Ilié, T. Li, I. Mounier, D. Poitrenaud, S. Younes : “Quantifying Robustness by Symbolic Model checking”, 1^st Hardware Verification Workshop (CAV workshop), Edinburgh, United Kingdom, pp. 1-12 (2010)
• 2009
  • X. Blanc, A. Mougenot, I. Mounier, T. Mens : “Incremental Detection of Model Inconsistencies based on Model Operations”, 21^st International Conference on Advanced Information Systems Engineering (CAiSE'09), vol. 5565, Lecture Notes in Computer Science, Amsterdam, Netherlands, pp. 32-46, (Springer) (2009)
  • S. Baarir, C. Braunstein, R. Clavel, E. Encrenaz, J.‑M. Ilié, R. Leveugle, I. Mounier, L. Pierre, D. Poitrenaud : “Complementary formal approaches for dependability analysis”, The 24^th IEEE International Symposium on Defect and Fault Tolerance in VLSI Systems, Chicago, Illinois, United States, pp. 331-339, (IEEE Computer Society) (2009)
• 2008
  • X. Blanc, I. Mounier, A. Mougenot, T. Mens : “Detecting Model Inconsistency Through Operation-Based Model Construction”, 30^th International Conference on Software Engineering (ICSE 2008), Leipzig, Germany, pp. 511-520, (ACM) (2008)
• 2006
  • X. Blanc, I. Mounier : “UML2 pour les développeurs”, 202 pages, (Eyrolles), (ISBN: 221212029X) (2006)
• 2004
  • F. Bréant, J.‑M. Couvreur, F. Gilliers, F. Kordon, I. Mounier, E. Paviot‑Adet, D. Poitrenaud, D. Regep, G. Sutre : “Modeling and Verifying Behavioral Aspects”, chapter in Formal Methods for Embedded Distributed Systems - How to master the complexity, pp. 171-211, (Kluwer Academic Publishers), (ISBN: 1-4020-7996-6) (2004)
• 2003
  • Y. Thierry‑Mieg, C. Dutheillet, I. Mounier : “Automatic Symmetry Detection in Well-Formed Nets”, 24^th International Conference on Theory and Application of Petri Nets, vol. 2679, Lecture Notes in Computer Science, Eindhoven, Netherlands, pp. 82-101, (Springer) (2003)
  • I. Vernier, E. Paviot‑Adet : “Modélisation et vérification de l’interopérabilité de services de télécommunication”, chapitre de Vérification et mise en oeuvre de réseaux de Petri, pp. 233-252, (Hermes Science), (ISBN: 2-7462-0445-2) (2003)
  • C. Dutheillet, J.‑M. Ilié, D. Poitrenaud, I. Vernier‑Mounier : “State-Space-Based Methods and Model Checking”, chapter in Petri nets for Systems Engineering : A Guide to Modeling, Verification, and Applications, pp. 201-275, (Springer-Verlag), (ISBN: 3-540-41217-4) (2003)
• 2001
  • G. Gaudière, A. de Groot, J. Hooman, F. Kordon, M. Lemoine, E. Paviot‑Adet, I. Vernier‑Mounier, V. Winter : “A Survey: Applying Formal Methods to a Software Intensive System”, 6^th IEEE International Symposium on Hight Assurance Systems Engineering (HASE'01), Boco Raton, FL, United States, pp. 55-64, (IEEE) (2001)
  • F. Kordon, I. Vernier‑Mounier, E. Paviot‑Adet, D. Regep : “Formal Verification of Embedded Distributed Systems in a Prototyping Approach”, International Workshop on Engineering Automation for Software Intensive System Integration, Monterey, United States (2001)
  • M. Doche, I. Vernier‑Mounier, F. Kordon : “Modular Approach to Specify and Validate an Electrical Fligh Control System”, Formal Method Europe (FME '2001), vol. 2021, Lecture Notes in Computer Science, Berlin, Germany, pp. 590-610, (Springer-Verlag) (2001)
• 1997
  • I. Vernier : “Model Checking and Parameterized Distributed Systems”, (1997)
• 1994
  • I. Vernier : “Graphe symbolique paramétré de réseaux de Petri et Logique temporelle”, thesis, phd defence 12/06/1994, supervision Haddad, Serge (1994)