LAURENT Yoann

doctorant à Sorbonne Université
Équipe : MoVe
https://perso.lip6.fr/Yoann.Laurent

Direction de recherche : Marie-Pierre GERVAIS

Co-encadrement : BENDRAOU Reda, BAARIR Souheib

Alloy4PV : Un Framework pour la Vérification de Procédés Métiers

En capturant l'ordonnancement des activités et le flux d'informations des données requises et produites, les modèles de procédés décrivent précisément les interactions entre les différents participants du procédé. Cependant, comme toute activité intellectuelle impliquant l'homme, un modélisateur peut introduire certaines erreurs ou incohérences lors de la modélisation. La modélisation de procédés est une tâche complexe. Un modèle de procédé peut contenir un flux de contrôle complexe impliquant boucles, synchronisation, parallélisme, contraintes temporelles et dépendances entre les données et les ressources. Pour ces raisons, et comme cela a été souligné par de récentes études, les modélisateurs tendent à faire beaucoup d'erreurs. La vérification de procédé avant sa mise en application est donc une étape critique afin d'assurer le bon fonctionnement de l'entreprise ainsi que la qualité des produits et services délivrés. Afin de vérifier un modèle de procédé, l'approche la plus communément utilisée consiste à recourir à des techniques de model-checking : une technique de vérification automatique et exhaustive de systèmes réactifs. Bien que de nombreuses approches aient été proposées par la communauté scientifique pour vérifier des procédés, aucune approche n’a réussi à s’imposer. Une des principales raisons provient du fait que la littérature s'adresse principalement à la perspective du flux de contrôle. Certaines approches proposent de vérifier une partie de la perspective des données et d'autres quelques contraintes temporelles. Cependant, aucune d'entre elles ne propose de vérifier toutes les perspectives des procédés de façon unifiée. En conséquence, une grande gamme de propriétés impliquant plusieurs perspectives n'est pas exprimable en utilisant les approches existantes. De plus, la complexité des outils proposés, leur nature pas toujours complètement automatique et intégrée dans un environnement de modélisation et d'exécution, ainsi que l'impossibilité, pour un simple modélisateur, d'exprimer des propriétés métiers, a empêché leur adoption. Dans cette thèse, nous avons tout d'abord fait une étude de l'état de l'art dans les différents domaines des procédés (métier, logiciel, militaire, médical, etc) afin d'identifier et de catégoriser les principales propriétés à garantir. À partir de cette étude, nous avons défini une bibliothèque de propriétés générique et paramétrable pour tout modèle de procédé. Ensuite, nous avons défini un framework pour la vérification de procédés appelé Alloy4PV. Il utilise un sous-ensemble des diagrammes d'activités UML 2 comme langage de modélisation. Afin d'effectuer la vérification de procédés, nous avons (1) défini un modèle formel des diagrammes d'activités basé sur la sémantique fUML (le standard de l'OMG donnant une sémantique à un sous-ensemble de UML) en utilisant la logique de premier ordre, (2) implémenté cette formalisation en utilisant le langage Alloy afin d'effectuer du model-checking borné, et (3) automatisé, dans un outil graphique intégré à Eclipse, la possibilité d'exprimer et de vérifier des propriétés sur toutes les perspectives du procédé.

Soutenance : 15/01/2015

Membres du jury :

Mireille Blay-Fornarino (Professeur, Université de Nice) [rapporteur]
Kais Klai (Maitre de conférences, HDR, Université Paris XIII) [rapporteur]
Pierre-Alain Muller (Professeur, Université de Haute-Alsace)
Bernard Coulette (Professeur, Université de Toulouse II)
Fabrice Kordon (Professeur, Université Paris VI)
Reda Bendraou (Maitre de conférences, Université Paris VI)
Souheib Baarir (Maitre de conférences, Université Paris X)
Marie-Pierre Gervais (Professeur, Université Paris X)

Date de départ : 16/01/2015

Publications 2013-2018