HILLAH Lom Messan

doctorant à Sorbonne Université
Équipe : MoVe
https://perso.lip6.fr/Lom-Messan.Hillah

Direction de recherche : Fabrice KORDON

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

Nous intégrons à la démarche de développement dirigé par les modèles (MDD), une approche mettant fortement en oeuvre les méthodes formelles pour la vérification de systèmes complexes. Le MDD, largement répandu dans l'industrie, est notamment mis en oeuvre pour le développement des systèmes de transport intelligents (ITS). Notre approche est motivée par le besoin de maîtriser les spécifications comportementales de tels systèmes et ainsi garantir leur sûreté. Elle s'articule selon trois aspects.
Le premier aspect concerne la recherche de stratégies de contrôle pour la supervision de système devant satisfaire une spécification donnée. Il s'agit de restreindre leur comportement par un contrôleur (s'il existe et peut être synthétisé) afin d'éviter les états dangereux. Le problème de l'explosion combinatoire de l'espace d'état nous oblige à mettre en oeuvre une structure de données performante comme les diagrammes de décisions hiérarchiques. Nous appliquons la recherche de stratégies de contrôle à l'évitement de collisions sur route automatisée.
Le deuxième aspect porte sur la vérification formelle de spécifications comportementales d'applications ITS en diagrammes d'activité UML. Les réseaux de Petri constituant le modèle formel le plus proche de ces diagrammes, nous les avons adaptés aux concepts orientés objet d'UML via la définition des Instantiable Petri Net (IPN). Les IPN intègrent la notion de type et d'instance de type, gèrent la modularité et la hiérarchie. Nous appliquons cette démarche à une application du projet européen SAFESPOT.
Enfin, le troisième aspect concerne l'interopérabilité des outils de réseaux de Petri pour l'échange de modèles. Cette interopérabilité doit aider les démarches de vérification comme celle proposée plus haut, à élargir à faible coût la portée de la vérification sur différents aspects comportementaux d'un même système. Le problème de compatibilité sémantique au niveau des différents types de réseaux de Petri et des formats propriétaires supportés par ces outils nous incite à élaborer un cadre normalisé pour l'échange. C'est ainsi que nous définissons, au sein de la norme ISO/IEC 15909, le format d'échange Petri Net Markup Language, (PNML), dans un cadre sémantique unifiant les définitions des réseaux de Petri place/transition et colorés.

Soutenance : 23/09/2009

Membres du jury :

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

Date de départ : 31/08/2010

Un doctorant à Sorbonne Université (Direction de recherche / Co-encadrement)

  • XU Hao : Hybridation de méthode de compilation de contraintes, Solveurs SAT, méthodes d'apprentissage pour maîtriser la complexité de la gamme Renault.

Publications 2005-2024