Abstract
BPMN is suitable to model not only intra-organization workflows but also inter-organization collaborations. There has been a great effort in providing a formal semantics for BPMN, and then in building verification tools on top of this semantics. However, communication aspects are often discarded in the literature. This is an issue since BPMN has gained interest outside its original scope, e.g., for the IoT, where the configuration of communication modes plays an important role. In this paper, we propose a formal semantics for a subset of BPMN, taking into account inter-process communication and parametric verification with reference to communication modes. As opposed to transformational approaches, that map BPMN into some formal model such as transition systems or Petri nets, we give a direct formalization in First-Order Logic that is then implemented in TLA\(^+\) to enable formal verification. Our approach is tool supported. The tool, as well as the TLA\(^+\) theories, and experiment models are available online.
This work was supported by project PARDI ANR-16-CE25-0006.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Business Process Modeling Notation. http://www.omg.org/spec/BPMN/2.0.2/
ProM Framework. http://www.processmining.org/prom
fbpmn repository. https://github.com/pascalpoizat/fbpmn, v0.3.0 (c389b6d)
Casati, F., et al.: Towards business processes orchestrating the physical enterprise with wireless sensor networks. In: Proceedings of ICSE (2012)
Chevrou, F., Hurault, A., Quéinnec, P.: On the diversity of asynchronous communication. Form. Asp. Comput. 28(5), 847–879 (2016)
Chevrou, F., Hurault, A., Quéinnec, P.: A Modular Framework for Verifying Versatile Distributed Systems. Journal of Logical and Algebraic Methods in Programming (to appear)
Corradini, F., et al.: A classification of BPMN collaborations based on safeness and soundness notions. In: Proceedings of EXPRESS/SOS (2018)
Corradini, F., et al.: A formal approach to modeling and verification of business process collaborations. Sci. Comput. Program. 166, 35–70 (2018)
Corradini, F., Muzi, C., Re, B., Rossi, L., Tiezzi, F.: Animating multiple instances in BPMN collaborations: from formal semantics to tool support. In: Weske, M., Montali, M., Weber, I., vom Brocke, J. (eds.) BPM 2018. LNCS, vol. 11080, pp. 83–101. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-98648-7_6
Dechsupa, C., Vatanawood, W., Thongtak, A.: Transformation of the BPMN design model into a colored Petri net using the partitioning approach. IEEE Access 6, 38421–38436 (2018)
Dijkman, R.M., Dumas, M., Ouyang, C.: Semantics and analysis of business process models in BPMN. Inf. Softw. Technol. 50(12), 1281–1294 (2008)
Fahland, D., et al.: Instantaneous soundness checking of industrial business process models. In: Dayal, U., Eder, J., Koehler, J., Reijers, H.A. (eds.) BPM 2009. LNCS, vol. 5701, pp. 278–293. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03848-8_19
Houhou, S., et al.: A first-order logic semantics for communication-parametric BPMN collaborations (extended version). http://pardi.enseeiht.fr/BPM19
Kheldoun, A., Barkaoui, K., Ioualalen, M.: Formal verification of complex business processes based on high-level Petri nets. Inf. Sci. 385, 39–54 (2017)
Krishna, A., Poizat, P., Salaün, G.: Checking business process evolution. Sci. Comput. Program. 170, 1–26 (2019)
Lam, V.S.: A precise execution semantics for BPMN. Int. J. Comput. Sci. 39(1), 20–33 (2012)
Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison Wesley, Boston (2002)
Meyer, S., Ruppen, A., Hilty, L.: The things of the internet of things in BPMN. In: Persson, A., Stirna, J. (eds.) CAiSE 2015. LNBIP, vol. 215, pp. 285–297. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19243-7_27
Nguyen, H.N., Poizat, P., Zaïdi, F.: A symbolic framework for the conformance checking of value-passing choreographies. In: Liu, C., Ludwig, H., Toumani, F., Yu, Q. (eds.) ICSOC 2012. LNCS, vol. 7636, pp. 525–532. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34321-6_36
Van Gorp, P., Dijkman, R.: A visual token-based formalization of BPMN 2.0 based on in-place transformations. Inf. Softw. Technol. 55(2), 365–394 (2013)
Wong, P.Y., Gibbons, J.: Formalisations and applications of BPMN. Sci. Comput. Program. 76(8), 633–650 (2011)
Ye, J., Sun, S., Song, W., Wen, L.: Formal semantics of BPMN process models using YAWL. In: Proceedings of IITA (2008)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2019 Springer Nature Switzerland AG
About this paper
Cite this paper
Houhou, S., Baarir, S., Poizat, P., Quéinnec, P. (2019). A First-Order Logic Semantics for Communication-Parametric BPMN Collaborations. In: Hildebrandt, T., van Dongen, B., Röglinger, M., Mendling, J. (eds) Business Process Management. BPM 2019. Lecture Notes in Computer Science(), vol 11675. Springer, Cham. https://doi.org/10.1007/978-3-030-26619-6_6
Download citation
DOI: https://doi.org/10.1007/978-3-030-26619-6_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-26618-9
Online ISBN: 978-3-030-26619-6
eBook Packages: Computer ScienceComputer Science (R0)