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.

1 Doctorant (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-2023