HOUHOU Sara

doctorant à Sorbonne Université
Équipe : MoVe
https://lip6.fr/Sara.Houhou

Direction de recherche : Pascal POIZAT, Laîd KAHLOUL

Co-encadrement : BAARIR Souheib

Vérification paramétrée à partir des spécifications formelles des systèmes d’information

La vérification des modèles de processus métiers est cruciale pour permettre d'y détecter d'éventuelles erreurs dès la conception, plutôt qu'à l'exécution sur des moteurs de processus métier. BPMN est la notation principale pour la modélisation de processus métier. Il s'agit d'un standard ISO, largement utilisé à la fois en enseignement et dans l'industrie. La sémantique de BPMN est cependant définie de façon semi-formelle au sein du standard. C'est pourquoi de nombreux travaux se sont attaqués à la définition d'une sémantique formelle pour BPMN. Dans cette thèse, nous avons tout d’abord fourni une étude détaillée des principaux travaux portant sur la vérification de modèles BPMN. Cela nous a permis d'identifier plusieurs fragments de la notation qui sont souvent mis de côté dans les travaux de formalisation, tels que les différents modèles de communication, la gestion temporelle, ou le caractère multi-instance. Ces aspects sont pourtant cruciaux pour l'élargissement du domaine d'application de BPMN vers des cadres tels que l'Internet des Objets ou l'Usine du Futur. Nous avons alors défini une approche pour la vérification de modèles de collaboration de processus métiers qui supporte plusieurs de ces perspectives, à savoir les différents modèles de communication et les contraintes liées au temps. Pour cela nous avons défini une sémantique d'exécution formelle, en termes de logique du premier ordre, au fragment de BPMN pris en compte. Nous avons ensuite défini des implantations de cette sémantique dans les langages formels TLA+ et Alloy. Ceci a, enfin, permis la vérification des modèles à l'aide des outils dédiés à ces langages formels. Notre approche est supportée par un outil, fbpmn, permettant les transformations formelles de modèles BPMN vers TLA+ et Alloy, la vérification des modèles, et l'animation de contre-exemples lorsque les propriétés à vérifier ne sont pas satisfaites. Ce retour se fait directement sur le modèle BPMN initial ce qui rend l'approche praticable dans un contexte d'utilisation par des non-spécialistes des méthodes formelles. Une application Web a aussi été développée pour rendre encore plus aisée l'application de notre approche formelle dans un cadre industriel. Nos outils, nos implantations en TLA+ et Alloy de la sémantique formelle, et notre bibliothèque d'exemples sont open source et disponibles en ligne.

Soutenance : 22/12/2021

Membres du jury :

RE Barbara (Maître de conférence à Camerino Université, HDR, PROS) [Rapporteur]
SALAÜN Gwen (Professeur à Grenoble Alpes Université, LIG, CNRS) [Rapporteur]
BÉRARD Béatrice (Professeur à Sorbonne Université, LIP6, CNRS)
HAMZA Lamia (Maître de conférence à Bejaia Université, HDR, LIMED)
OKBA Tibermacine (Maître de conférence à Biskra Université, HDR,LESIA)
BAARIR Souheib (Maître de conférence à Paris Nanterre Université, HDR, LIP6, CNRS)
KAHLOUL Laîd (Professeur à Biskra Université, LINFI)
POIZAT Pascal (Professeur à Paris Nanterre Université, LIP6, CNRS)

Date de départ : 31/12/2021

Publications 2019-2022