PhD graduated
Team : MoVe
Departure date : 01/16/2015

Supervision : Marie-Pierre GERVAIS

Co-supervision : BENDRAOU Reda, BAARIR Souheib

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

By capturing the ordering of activities and the flow of required and produced artifacts, process models describe precisely all the interactions amongst the different process stakeholders. However, like any activity involving intellectual human tasks, a modeler can introduce errors or inconsistencies during the modeling phase. Indeed, a process model can contain a sophisticated control-flow involving loops, synchronization, parallelism, timing constraints, and dependencies between data and resources. Consequently, and as highlighted by some recent studies, process modelers tend to do a lot of mistakes. The verification of the process model before its deployment in an effective production context becomes more than critical in order to ensure a good quality of the company’s delivered products and services. In order to verify a process model, the most common approach consists in using model-checking, an automatic and exhaustive technique to verify reactive systems. Although a lot of approaches have been proposed in the literature to verify process models, no approach has succeeded to be largely adopted. One of the main reasons comes from the fact that these approaches addressed principally the control-flow perspective. Some approaches propose to verify a part of the data perspective, and others offer the possibility to check some temporal constraints. However, none of them verify all the perspectives of process models in a unified way. Consequently, a wide range of properties implying multiple perspectives is not expressible using these approaches. Moreover, the complexity of the associated tools, their lack of a fully automatic support of the entire verification chain, the fact that they are not integrated in a process environment and the impossibility for the average process modeler to express business properties prevent their adoption. In this thesis, we realized a study of the start-of-the-art on different process domains (business, software, military, medical, etc.). The aim was to identify and categorize critical properties that can be verified on any process model. This study resulted in a library of generic and configurable properties. As a second step, we have defined a framework for process verification called Alloy4PV. This framework uses a subset of UML 2 Activity Diagram as a process modeling language. For process verification, (1) we defined a formal model of UML 2 Activity Diagram based on the fUML semantics, the OMG standard that gives a semantic to a subset of UML 2. This was achieved using first-order logic, (2) we implemented this formalization using the Alloy language in order to perform bounded model-checking, and (3) we automatized in a graphical tool integrated to Eclipse, the possibility to express and verify properties on all the perspectives of a process model. This contribution resulted in a tool which is under evaluation by our MerGE project’s partners and to five publications in conferences proceedings.

Defence : 01/15/2015 - 14h30 - Site Jussieu 25-26/105

Jury members :

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)

2013-2018 Publications