Towards a Formal Semantics and Analysis of BPMN Gateways
This paper deals with formal verification of BPMN models. The lack of an unambiguous definition of the BPMN notations, and the mixing of incompatible BPMN patterns may lead to wrong or incomplete semantics, resulting in some behavioral errors such as deadlocks and multiple termination problems. As formal verification requires formal specification models and in order to create a correct business process, most used approaches consider the formalization of either a subclass of BPMN patterns or specific forms of these patterns. In this paper, thanks to Max+ Algebra, we propose to extend existing approaches by including most of BPMN notations.
KeywordsBusiness process BPMN Formal semantics
- 1.OMG.: Business Process Modeling Notation (BPMN) Version 2.0. OMG Final Adopted Specification. Object Management Group (2011)Google Scholar
- 2.El Hichami, O., Al Achhab, M., Berrada, I., El Mohajir, B.: Short: graphical specification and automatic verification of business process. In: Noubir, G., Raynal, M. (eds.) Networked Systems. LNCS, vol. 8593, pp. 341–346. Springer, Heidelberg (2014) Google Scholar
- 5.El Hichami, O., Al Achhab, M., Berrada, I., El Mohajir, B.: Visual specification language and automatic checking of business process. In: 8th International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS 2014), vol. 1256, pp. 93–101. CEUR Workshop Proceedings, Bejaia, Algeria, 29–30 September (2014)Google Scholar
- 7.Dijkman, R.M., Dumas, M., Ouyang, C.: Formal semantics and analysis of BPMN process models using Petri nets. Technical report 7115, Queensland University of Technology, Brisbane (2007)Google Scholar