Towards a Formal Semantics and Analysis of BPMN Gateways

  • Outman El HichamiEmail author
  • Mohamed Naoum
  • Mohammed Al Achhab
  • Ismail Berrada
  • Badr Eddine El Mohajir
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9466)


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.


Business process BPMN Formal semantics 


  1. 1.
    OMG.: Business Process Modeling Notation (BPMN) Version 2.0. OMG Final Adopted Specification. Object Management Group (2011)Google Scholar
  2. 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
  3. 3.
    van der Aalst, W.M.P., van Dongen, B.F.: Discovering petri nets from event logs. In: Jensen, K., Aalst, W.M.P., Balbo, G., Koutny, M., Wolf, K. (eds.) Transactions on Petri Nets and Other Models of Concurrency VII. LNCS, vol. 7480, pp. 372–422. Springer, Heidelberg (2013) CrossRefGoogle Scholar
  4. 4.
    Fahland, D., Favre, C., Koehler, J., Lohmann, N., Volzer, H., Wolf, K.: Analysis on demand: instantaneous soundness checking of industrial business process models. Data Knowl. Eng. 70(5), 448–466 (2011)CrossRefGoogle Scholar
  5. 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
  6. 6.
    Murata, T., Koh, J.Y.: Petri nets: properties, analysis and applications. an invited survey paper. Proc. IEEE 77(4), 541–580 (1989)CrossRefGoogle Scholar
  7. 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
  8. 8.
    Dijkman, R.M., Dumas, M., Ouyang, C.: Semantics and analysis of business process models in BPMN. Inf. Softw. Technol 50(12), 1281–1294 (2008)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • Outman El Hichami
    • 1
    Email author
  • Mohamed Naoum
    • 1
  • Mohammed Al Achhab
    • 2
  • Ismail Berrada
    • 3
  • Badr Eddine El Mohajir
    • 1
  1. 1.Faculty of SciencesUAETetouanMorocco
  2. 2.National School of Applied SciencesUAETetouanMorocco
  3. 3.Faculty of Sciences and TechnologyUSMBAFezMorocco

Personalised recommendations