|
 
|
[KBI17] Formal verification of complex of complex business processes based on high-level Petri nets business processes based on high-level Petri nets
Revue Internationale avec comité de lecture : Journal Information Sciences, vol. 385-386(385), pp. 39-54 , 2017, (doi:10.1016/j.ins.2016.12.044)Mots clés: Business process modelling BPMN RECATNets Conditional rewriting logic Maude language and tool
Résumé:
The Business Process Modeling Notation (BPMN) has been widely used as a tool for business process modeling. However, BPMN suffers from a lack of standard formal semantics. This weakness can lead to inconsistencies, ambiguities, and incompletenesses within the developed models. In this paper, we propose a formal semantics of BPMN using recursive ECATNets. Owing to this formalism, a large set of BPMN features such as cancellation, multiple instantiation of subprocesses and exception handling can be covered while taking into account the data flow aspect. The benefits and usefulness of this modelling are illustrated through three examples. Moreover, since recursive ECATNets semantics is defined in terms of conditional rewriting logic, one can use the Maude LTL model checker to verify several behavioral properties related to BPMN models. The work presented in this document has been automated through the development of a first prototype.
Collaboration:
USTHB
BibTeX
| @article { | |||
| KBI17, | |||
| title | = | "{Formal verification of complex of complex business processes based on high-level Petri nets business processes based on high-level Petri nets}", | |
| author | = | "A. Kheldoun and K. Barkaoui and M. Ioulalen", | |
| journal | = | "Information Sciences", | |
| year | = | 2017, | |
| volume | = | 385-386, | |
| number | = | 385, | |
| pages | = | "39-54 ", | |
| doi | = | "10.1016/j.ins.2016.12.044", | |
| } | |||
