HILLAH Lom-Messan

PhD graduated
Team : MoVe
Departure date : 08/31/2010
http://move.lip6.fr/~Lom-Messan.Hillah

Supervision : Fabrice KORDON

Integration of formal methods into Model-Driven Development, for distributed systems and applications design and verification

We integrate into the framework of Model-Driven Development, widely adopted in the industry, a formal methods approach for the verification of complex systems, like intelligent transport systems. This approach is driven by the need to control the behavioral specification of such systems. It is structured in three parts.
The first part is about searching for control strategies to supervise systems that must stay within the set of their admissible behaviors. To tackle the state space explosion problem, we use set decision diagrams, very compact and performant data structures. In this approach we look for collision avoidance strategies on an automated highway.
The second part is about formal verification of behavioral specifications of ITS applications in UML activity diagrams. Petri nets being the closest formal models to these diagrams, we have tailored them to meet UML object-oriented concepts by defining Instantiable Petri Nets (IPN). IPNs encompass the notions of type, instance and they handle modularity and hierarchy. In this approach we verify the design of a software of the european project SAFESPOT.
The last part is about Petri nets tools interoperability over Petri net models. This long-sought interoperability is meant to help easily extend the verification range of interesting behavioral characteristics of a system, using different specialized tools. The semantic compatibility issue over different Petri nets types and proprietary supporting formats between the tools made us set up a standardized framework for models interchange. We thus define the interchange format Petri Net Markup Language (PNML), second part of the international standard ISO/IEC 15909. It relies upon the explicit semantic unification of place/transition and colored Petri nets definitions.

Defence : 09/23/2009 - 14h - Site Passy-Kennedy - salle 549
Jury members :
Fabrice Kordon, Professeur à l'université P. & M. Curie [Directeur]
Isabel Demongodin, Professeur à l'université Aix-Marseille [Rapporteur]
Michel Lemoine, Directeur de recherche à l'ONERA [Rapporteur]
Claude Girault, Professeur émérite à l'université P. & M. Curie
Marie-Pierre Gervais, Professeur à l'université Paris Ouest Nanterre
Ekkart Kindler, Associate professor, Technical University of Denmark
Laure Petrucci, Professeur à l'université Paris 13

2005-2019 Publications

2019
- F. Kordon, H. Garavel, L. Hillah, E. Paviot‑Adet, L. Jezequel, F. Hulin‑Hubard, E. Amparore, M. Beccuti, B. Berthomieu, H. Evrard, P. Jensen, D. Le Botlan, T. Liebke, J. Meijer, J. Srba, Y. Thierry‑Mieg, J. Van De Pol, K. Wolf : “Presentation of the 9^th edition of the model checking contest”, 25^th TACAS@ETAPS 2019, vol. 11090, Lecture Notes in Computer Science, Prague, Czech Republic, pp. 181-209, (Springer) (2019)
- E. Amparore, B. Berthomieu, G. Ciardo, S. Dal Zilio, F. Gallà, L. Hillah, F. Hulin‑Hubard, P. Jensen, L. Jezequel, F. Kordon, D. Le Botlan, T. Liebke, J. Meijer, A. Miner, E. Paviot‑Adet, J. Srba, Y. Thierry‑Mieg, T. van Dijk, K. Wolf : “Presentation of the 9^th Edition of the Model Checking Contest”, Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Proceedings, Part III, vol. 11429, Prague, Czech Republic, pp. 50-68 (2019)
2018
- T. Ziadi, L. Hillah : “Software Product Line Extraction from Bytecode based applications”, International Conference on Engineering of Complex Computer Systems, Melbourne, Australia (2018)
2017
- L. Hillah, A.‑P. Maesano, F. De Rosa, F. Kordon, P.‑H. Wuillemin, R. Fontanelli, S. Di Bona, D. Guerri, L. Maesano : “Automation and Intelligent Scheduling of Distributed System Functional Testing: Model-Based Functional Testing in Practice”, International Journal on Software Tools for Technology Transfer, vol. 19 (3), pp. 281-308, (Springer Verlag) (2017)
- L. Hillah, R. Assad, A. Bertolino, L. Maesano, J. Iyoda : “Automated Deployment and Management of Self-* Applications on Hybrid Clouds”, Cloudscape Brazil and Workshop on Cloud Networks 2017, São Paulo, Brazil (2017)
- L. Hillah, F. Kordon : “Petri Nets Repository, a tool to benchmark and debug Petri Net tools”, 38^th International Conference, PETRI NETS 2017, vol. 10258, Lecture Notes in Computer Science, Zaragoza, Spain, pp. 125-135, (Springer) (2017)
- L. Hillah, R. Assad, A. Bertolino, M. Delamaro, F. De Rosa, V. Garcia, F. Lonetti, A.‑P. Maesano, L. Maesano, E. Marchetti, B. Miranda, A. Vincenzi, J. Iyoda : “Towards automated deployment of self-adaptive applications on hybrid clouds”, 15^th International Conference on Software Engineering and Formal Methods (SEFM 2017), Trento, Italy (2017)
2016
- F. Kordon, H. Garavel, L. Hillah, E. Paviot‑Adet, L. Jezequel, C. Rodríguez, F. Hulin‑Hubard : “MCC’2015 – The Fifth Model Checking Contest”, LNCS Transactions on Petri Nets and Other Models of Concurrency, vol. 9930, Lecture Notes in Computer Science, pp. 262-273, (Springer) (2016)
- A. Linard, B. Barbot, D. Buchs, M. Colange, C. Démoulins, L. Hillah, A. Martin : “Layered Data: A Modular Formal Definition without Formalisms”, Petri Nets and Software Engineering (PNSE 2016), vol. 1591, CEUR Workshops Proceedings, Toruń, Poland, pp. 287-306, (CEUR-WS.org) (2016)
- L. Hillah, A.‑P. Maesano, L. Maesano, F. De Rosa, F. Kordon, P.‑H. Wuillemin : “Service functional testing automation with intelligent scheduling and planning”, Symposium on Applied Computing (SAC), Proceeding of the 31^st Annual ACM Symposium on Applied Computing, Pisa, Italy, pp. 1605-1610 (2016)
2015
- S. Lamprier, N. Baskiotis, T. Ziadi, L. Hillah : “The CARE Platform for the Analysis of Behavior Model Inference Techniques”, Information and Software Technology, vol. 60, pp. 32-50, (ISBN: 0950-5849) (2015)
- L. Hillah, A.‑P. Maesano, F. De Rosa, L. Maesano, M. Lettere, R. Fontanelli : “Service functional test automation”, 10^th Workshop on System Testing and Validation, A. Rennoch (Ed.), Sophia Antipolis, France (2015)
- S. Herbold, J. Grabowski, P. Harms, L. Hillah, F. Kordon, A.‑P. Maesano, L. Maesano, C. Di Napoli, F. De Rosa, M. Schneider, N. Tonelloto, M.‑F. Wendland, P.‑H. Wuillemin : “The MIDAS Cloud Platform for Testing SOA Applications”, 8^th International IEEE Conference on Software Testing, Verification and Validation (ICST), Graz, Austria, pp. 1-8, (IEEE Press) (2015)
2014
- Y. Zhang, B. Bérard, L. Hillah, F. Kordon, Y. Thierry‑Mieg : “Controllability for Discrete Event Systems Modeled in VeriJ”, International Journal of Critical Computer-Based Systems, vol. 5 (3/4), pp. 218-240, (ISBN: 1757-8779) (2014)
- S. Lamprier, T. Ziadi, N. Baskiotis, L. Hillah : “Exact and Efficient Temporal Steering of Software Behavioral Model Inference”, Proc. of 19^th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS), Tianjin, China, pp. 166-175, (IEEE) (2014)
2013
- É. André, B. Barbot, C. Démoulins, L. Hillah, F. Hulin‑Hubard, F. Kordon, A. Linard, L. Petrucci : “A Modular Approach for Reusing Formalisms in Verification Tools of Concurrent Systems”, 15^th International Conference on Formal Engineering Methods (ICFEM'13), vol. 8144, Lecture Notes in Computer Science, Queenstown, New Zealand, pp. 199-214, (Springer) (2013)
- S. Lamprier, N. Baskiotis, T. Ziadi, L. Hillah : “CARE: a platform for reliable Comparison and Analysis of Reverse-Engineering techniques”, 18^th IEEE International Conference on Engineering of Complex Computer Systems -- ICECCS, Singapore, Singapore, pp. 252-255, (IEEE) (2013)
- É. André, Y. Lembachar, L. Petrucci, F. Hulin‑Hubard, A. Linard, L. Hillah, F. Kordon : “CosyVerif: an Open Source Extensible Verification Environment”, 18^th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'13), Singapore, Singapore, pp. 33-36, (IEEE Computer Society) (2013)
- Y. Zhang, B. Bérard, L. Hillah, Y. Thierry‑Mieg : “Semi-Automatic Controller Design of Java-like Models”, Workshop on Formal Techniques for Java-like Programs, FTfJP 2013, Montpellier, France, pp. 3:1-3:7, (ACM) (2013)
2012
- L. Hillah, F. Kordon, Ch. Lakos, L. Petrucci : “Extending PNML Scope: a Framework to Combine Petri Nets Types”, LNCS Transactions on Petri Nets and Other Models of Concurrency, vol. 7400 (VI), Lecture Notes in Computer Science, pp. 46-70, (Springer Berlin Heidelberg), (ISBN: 1867-7193) (2012)
- M. Colange, L. Hillah, F. Kordon, P. Parutto : “Extreme Symmetries in Complex Distributed Systems: the Bag-Oriented Approach”, Development, Operation and Management of Large-Scale Complex IT Systems, 17^th Monterey Workshop, Revised Selected Papers, vol. 7539, Lecture Notes in Computer Science, Oxford, United Kingdom, pp. 330-352, (Springer) (2012)
- F. Kordon, A. Linard, D. Buchs, M. Colange, S. Evangelista, L. fronc, L. Hillah, N. Lohmann, E. Paviot‑Adet, F. Pommereau, Ch. Rohr, Y. Thierry‑Mieg, K. Wolf : “Raw Report on the Model Checking Contest at Petri Nets 2012”, CoRR (2012)
2011
- T. Ziadi, M. Almeida da Silva, L. Hillah, M. Ziane : “A Fully Dynamic Approach to the Reverse Engineering of UML Sequence Diagrams”, 16^th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS, Las Vegas, USA, pp. 107-116, (IEEE Computer Society) (2011)
- L. Hillah, F. Kordon, Ch. Lakos, L. Petrucci : “Extending PNML Scope: the Prioritised Petri Nets Experience”, Petri Net and Software Engineering (PNSE 2011), vol. 723, CEUR-WS, Newcastle, United Kingdom, pp. 92-106, (CEUR) (2011)
- Y. Zhang, B. Bérard, L. Hillah, F. Kordon, Y. Thierry‑Mieg : “Modeling complex systems with VeriJ”, 5^th Verification and Evaluation of Computer and Communication System (VECOS), Tunis, Tunisia, pp. 34-45, (British Informatics Society Ltd) (2011)
2010
- L. Hillah, L. Petrucci : “Standardisation des réseaux de Petri : état de l’art et enjeux futurs”, Génie Logiciel, vol. 93, pp. 5-10 (2010)
- L. Hillah, F. Kordon, L. Petrucci, N. Trèves : “PNML Framework: an extendable reference implementation of the Petri Net Markup Language”, 31^st International Conference on Petri Nets and Other Models of Concurrency (ICATPN 2010), vol. 6128, Lecture Notes in Computer Science, Braga, Portugal, pp. 318-327, (Springer) (2010)
- S. Baarir, L. Hillah, F. Kordon, E. Renault : “Self-Reconfigurable Modular Robots and their Symbolic Configuration Space”, Modeling, Development and Verification of Adaptative Computer Systems: the Grand Challenge for Robust Software, 16^th Monterey Workshop 2010, Redmond, Revised Selected Papers, vol. 6662, Lecture Notes in Computer Science, Redmond, USA, pp. 103-121, (Springer) (2010)
2009
- L. Hillah, E. Kindler, F. Kordon, L. Petrucci, N. Trèves : “A primer on the Petri Net Markup Language and ISO/IEC 15909-2”, Petri Net Newsletter, vol. 76, pp. 9-28, (Gesellschaft für Informatik), (ISBN: 0391-1804) (2009)
- N. Trèves, L. Hillah, F. Kordon, L. Petrucci : “A primer on the Petri Net Markup Language and ISO/IEC 15909-2”, 10^th International workshop on Practical Use of Colored Petri Nets and the CPN Tools (CPN'09), Aarhus, Denmark, pp. 19 (2009)
- L.‑M. Hillah : “Intégration des méthodes formelles au développement dirigé par les modèles, pour la conception et la vérification des systèmes et applications répartis”, these, defence 09/23/2009, supervision Kordon, Fabrice (2009)
2008
- L. Hillah, F. Kordon, L. Petrucci : “Application des méthodes formelles à la robotique modulaire”, Journal Européen des Systèmes Automatisés (JESA), vol. 42 (4), pp. 459-478, (ISBN: 1269-6935) (2008)
- Y. Thierry‑Mieg, L. Hillah : “UML Behavioral Consistency Checking Using Instantiable Petri nets”, Innovations in Systems and Software Engineering, vol. 4 (3), pp. 293-300, (ISBN: 1614-5046) (2008)
- B. Bérard, S. Haddad, L. Hillah, F. Kordon, Y. Thierry‑Mieg : “Collision Avoidance in Intelligent Transport Systems: towards an Application of Control Theory”, 9^th International Workshop on Discrete Event Systems (WODES'08), Goteborg, Sweden, pp. 346-351, (IEEE Computer Society) (2008)
2007
- F. Bonnefoi, L. Hillah, F. Kordon, X. Renault : “Design, Modeling and Analysis of ITS using UML and Petri Nets”, 10^th International IEEE Conference on Intelligent Transportation Systems, Seattle, WA, USA, pp. 314-319, (IEEE) (2007)
2006
- F. Bonnefoi, L. Hillah, F. Kordon, G. Fremont : “An Approach to Model Variations of a Scenario: Application to Intelligent Transport Systems”, Fourth International Workshop on Modelling of Objects, Components and Agents (MOCA '06), D. Moldt (Ed.), Turku, Finland, pp. 65-86 (2006)
- A. Hamez, L. Hillah, F. Kordon, A. Linard, E. Paviot‑Adet, X. Renault, Y. Thierry‑Mieg : “New Features in CPN-AMI 3 : Focusing on the Analysis of Complex Distributed Systems”, Application of Concurrency to System Design 6^th International Conference on Application of Concurrency to System Design (ACSD '06), Turku, Finland, pp. 273-275, (IEEE Computer Society) (2006)
- L. Hillah, F. Kordon, L. Petrucci, N. Trèves : “PN Standardisation : a Survey”, 26^th international conference on Formal Methods for Networked and Distributed Systems (FORTE'06), vol. 4229, Lecture Notes in Computer Science, Paris, France, pp. 307-322, (Springer-Verlag) (2006)
2005
- L. Hillah, F. Kordon, L. Petrucci, N. Trèves : “Model Engineering on Petri Nets for ISO/IEC 15909-2: API Framework for Petri Net Types Metamodels”, Petri Net Newsletter, vol. 69, pp. 22-40 (2005)