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.

Publications 2019-2022

• 2022
  • S. Houhou, S. Baarir, P. Poizat, Ph. Quéinnec, L. Kahloud : “A First-Order Logic Verification Framework for Communication-Parametric and Time-Aware BPMN Collaborations”, Information Systems, vol. 104, pp. 101765, (Elsevier) (2022)
• 2021
  • S. Houhou : “Parameterised Verification from Formal Specifications of Information Systems”, thèse, soutenance 22/12/2021, direction de recherche Poizat, Pascal Kahloul, Laîd, co-encadrement : Baarir, Souheib (2021)
  • R. Saddem‑Yagoubi, P. Poizat, S. Houhou : “Business Processes Meet Spatial Concerns: the sBPMN Verification Framework”, FM 2021 - 24^th International Symposium on Formal Methods, vol. 13047, Lecture Notes in Computer Science, Beijing, China, pp. 218-234 (2021)
  • S. Houhou, S. Baarir, P. Poizat, Ph. Quéinnec : “A Direct Formal Semantics for BPMN Time-Related Constructs”, ENASE 2021 - 16^th International Conference on Evaluation of Novel Approaches to Software Engineering, online, Czechia, pp. 138-149 (2021)
• 2019
  • S. Houhou, S. Baarir, P. Poizat, Ph. Quéinnec : “A First-Order Logic Semantics for Communication-Parametric BPMN Collaborations”, BPM 2019: Business Process Management, vol. 11675, Lecture Notes in Computer Science book series (LNCS), Vienna, Austria, pp. 52-68 (2019)