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

 Mentions légales
Site map |