Formal semantics and transformation of BPMN models

Autor: Maarouk, Toufik Messaoud, Merah, Elkamel, Ghaoui, Sara, Rahabi, Nihed
Zdroj: International Journal of Business Process Integration and Management; 2019, Vol. 9 Issue: 3 p158-169, 12p
Abstrakt: Business process modelling notation (BPMN) represents an industrial standard created in order to provide a graphical semi-formal notation that is readily understandable by all business users, from the business analyst to the technical developers, and, finally, to the business people who will manage those processes. However, BPMN models are expressed in a semi-formal modelling language and need a well-defined formal semantics base for their notations. This formalisation enables analysis and verification tasks. Some efforts have been made to transform BPMN models into formal representations including Petri nets, but, to the best of our knowledge, no work has been done for transforming BPMN models into a language that supports a true concurrency semantics, DD-LOTOS. The DD-LOTOS language is defined for the formal specification of distributed real-time systems and has been defined on a semantic model of true concurrency. The main goal of this paper is to propose a formal semantics for a subset of BPMN, defined in terms of DD-LOTOS code. The paper also proposes a model transformation approach to generate DD-LOTOS code from BPMN models. This approach has been implemented using Eclipse Sirius and Eclipse Acceleo. Two well-known case studies are given to illustrate the transformation.
Databáze: Supplemental Index