VBPMN: Automated Verification of BPMN Processes (Tool Paper)

  • Ajay Krishna
  • Pascal Poizat
  • Gwen SalaünEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10510)


Business process modeling is an important concern in enterprise. Formal analysis techniques are crucial to detect semantic issues in the corresponding models, or to help with their refactoring and evolution. However, business process development frameworks often fall short when it comes to go beyond simulation or syntactic checking of the models. In this paper, we present our VBPMN verification framework. It features several techniques for the automatic analysis of business processes modeled using BPMN, the de facto standard for business process modeling. As such, it supports a more robust development of business processes.


Business processes BPMN Verification Evolution Tool Process algebra LNT Labelled transition system Model transformation 


  1. 1.
  2. 2.
    Bose, R.P.J.C., Verbeek, E.H.M.W., Aalst, W.M.P.: Discovering hierarchical process models using ProM. In: Nurcan, S. (ed.) CAiSE Forum 2011. LNBIP, vol. 107, pp. 33–48. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-29749-6_3 CrossRefGoogle Scholar
  3. 3.
    Champelovier, D., Clerc, X., Garavel, H., Guerte, Y., Lang, F., McKinty, C., Powazny, V., Serwe, W., Smeding, G.: Reference Manual of the LNT to LOTOS Translator, Version 6.1. INRIA/VASY (2014)Google Scholar
  4. 4.
    Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of ICSE 1999, pp. 411–420. ACM (1999)Google Scholar
  5. 5.
    Fahland, D., Favre, C., Koehler, J., Lohmann, N., Völzer, H., Wolf, K.: Analysis on demand: instantaneous soundness checking of industrial business process models. Data Knowl. Eng. 70(5), 448–466 (2011)CrossRefGoogle Scholar
  6. 6.
    Garavel, H., Lang, F.: SVL: a scripting language for compositional verification. In: Kim, M., Chin, B., Kang, S., Lee, D. (eds.) FORTE 2001. IIFIP, vol. 69, pp. 377–392. Springer, Boston, MA (2002). doi: 10.1007/0-306-47003-9_24 CrossRefGoogle Scholar
  7. 7.
    Garavel, H., Lang, F., Mateescu, R., Serwe, W.: CADP 2011: a toolbox for the construction and analysis of distributed processes. STTT 15(2), 89–107 (2013)CrossRefzbMATHGoogle Scholar
  8. 8.
    Güdemann, M., Poizat, P., Salaün, G., Ye, L.: VerChor: a framework for the design and verification of choreographies. IEEE Trans. Serv. Compu. 9(4), 647–660 (2016)CrossRefGoogle Scholar
  9. 9.
    ISO/IEC: International Standard 19510, Information technology - Business Process Model and Notation (2013)Google Scholar
  10. 10.
    Ivanov, S., Kalenkova, A.A., van der Aalst, W.M.P: BPMNDiffViz: a tool for BPMN models comparison. In: Proceedings of BPMN 2015 Demo Session, CEUR Workshop Proceedings, BPMN 2015, vol. 1418, pp. 35–39 (2015).
  11. 11.
    OMG: Business Process Model and Notation (BPMN) - Version 2.0, January 2011Google Scholar
  12. 12.
    Poizat, P., Salaün, G., Krishna, A.: Checking business process evolution. In: Kouchnarenko, O., Khosravi, R. (eds.) FACS 2016. LNCS, vol. 10231, pp. 36–53. Springer, Cham (2017). doi: 10.1007/978-3-319-57666-4_4 CrossRefGoogle Scholar
  13. 13.
    van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555–600 (1996)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Univ. Grenoble Alpes, CNRS, Grenoble INP, Inria, LIGGrenobleFrance
  2. 2.Université Paris Lumières, Univ Paris NanterreNanterreFrance
  3. 3.Sorbonne Universités, UPMC Univ Paris 06, CNRS, LIP6 UMR7606ParisFrance

Personalised recommendations