LAURENT Yoann
Научны(е)й руководител(и)ь : Marie-Pierre GERVAIS
Со-руководитель : 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.
Защита диссертаций : 15.01.2015
Члены жюри :
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
-
2018
- S. Baarir, R. Bendraou, H. Metin, Y. Laurent : “ProVer: an SMT-based approach for process verification”, Model-Driven Engineering Verification & Validation, MoDELS Workshop, vol. 2245, MODELS Workshops, Copenhague, Denmark, pp. 555-562 (2018)
-
2015
- Y. Laurent : “Alloy4PV : Un Framework pour la Vérification de Procédés Métiers”, диссертация, Защита диссертаций 15.01.2015, Научны(е)й руководител(и)ь Gervais, Marie-Pierre, Со-руководитель : Bendraou, Reda, Baarir, Souheib (2015)
- D. Khelladi, R. Bendraou, S. Baarir, Y. Laurent, M.‑P. Gervais : “A Framework to Formally Verify Conformance of a Software Process to a Software Method”, 30th ACM/SIGAPP Symposium On Applied Computing SAC, Salamanca, Spain, pp. 1518-1525, (ACM) (2015)
-
2014
- Y. Laurent, R. Bendraou, S. Baarir, M.‑P. Gervais : “Alloy4SPV : A Formal Framework for Software Process Verification”, ECMFA 2014 - 10th European Conference on Modelling Foundations and Applications, vol. 8569, Lecture Notes in Computer Science, York, United Kingdom, pp. 83-100, (Springer) (2014)
- Y. Laurent, R. Bendraou, S. Baarir, M.‑P. Gervais : “Formalization of fUML: An Application to Process Verification”, CAiSE 2014 - The 26th International Conference on Advanced Information Systems Engineering, vol. 8484, Lecture Notes in Computer Science, Thessaloniki, Greece, pp. 347-363, (Springer) (2014)
- Y. Laurent, R. Bendraou, S. Baarir, M.‑P. Gervais : “Planning for Declarative Processes”, SAC'14 - The 29th Annual ACM Symposium on Applied Computing, Gyeongju, Korea, Republic of, pp. 1126-1133, (ACM) (2014)
-
2013
- Y. Laurent, R. Bendraou, M.‑P. Gervais : “Generation of Process Using Multi-Objective Genetic Algorithm”, International Conference on Software and System Process, ICSSP 2013, San Francisco, CA, United States, pp. 161-165, (ACM) (2013)
- Y. Laurent, R. Bendraou, M.‑P. Gervais : “Executing and debugging UML models: an fUML extension”, SAC'13 - The 28th Annual ACM Symposium on Applied Computing, Coimbra, Portugal, pp. 1095-1102, (ACM) (2013)