Logo PTI Logo FedCSIS

Communication Papers of the 18th Conference on Computer Science and Intelligence Systems

Annals of Computer Science and Information Systems, Volume 37

Formal verification of BPMN diagrams in Integrated Model of Distributed Systems (IMDS)

,

DOI: http://dx.doi.org/10.15439/2023F8794

Citation: Communication Papers of the 18th Conference on Computer Science and Intelligence Systems, M. Ganzha, L. Maciaszek, M. Paprzycki, D. Ślęzak (eds). ACSIS, Vol. 37, pages 65–74 ()

Full text

Abstract. Business process model and notation (BPMN) is a way of describing business processes using convenient diagrams. In the last decade, it became a de-facto industry standard, widely used by software architects and business analysts to describe business requirements and the overall structure of a designed information system. Ensuring that diagrams model their intended behavior is of utmost importance for notation users. This article deals with the definition of BPMN through the conversion to the Integrated Model of Distributed Systems (IMDS) and automated verification of BPMN diagrams. The translation of a subset of BPMN preserves information about the processes in the formal model. This allows finding partial deadlocks and checking partial termination (concerning a subset of processes), verification in terms of BPMN processes, and mapping found errors onto source BPMN definition. Moreover, IMDS is tailored to model distributed systems, which is the very nature of business processes. A tool for automated translation of BPMN diagrams to IMDS, automated verification, and visualization of results is developed.

References

  1. W. M. P. van der Aalst, “The Application of Petri Nets to Workflow Management,” J. Circuits, Syst. Comput., vol. 08, no. 01, pp. 21–66, Feb. 1998. http://dx.doi.org/10.1142/S0218126698000043
  2. W. Reisig, Understanding Petri Nets. Berlin, Heidelberg: Springer Berlin Heidelberg, 2013. http://dx.doi.org/10.1007/978-3-642-33278-4
  3. Object Management Group, “Business Process Model and Notation (BPMN) Version 2.0.2,” 2013. http://www.omg.org/spec/BPMN/2.0.2
  4. C. Baier and J.-P. Katoen, Principles of Model Checking. Cambridge, MA: MIT Press, 2008. http://dx.doi.org/10.1007/978-3-030-12835-7_6
  5. F. Kossak et al., A Rigorous Semantics for BPMN 2.0 Process Diagrams. Cham: Springer International Publishing, 2014. http://dx.doi.org/10.1007/978-3-319-09931-6
  6. W. B. Daszczuk, “Specification and Verification in Integrated Model of Distributed Systems (IMDS),” MDPI Comput., vol. 7, no. 4, pp. 1–26, Dec. 2018. http://dx.doi.org/10.3390/computers7040065
  7. W. B. Daszczuk, “Using the Dedan Program,” in Integrated Model of Distributed Systems, Cham, Switzerland: Springer Nature, 2020, pp. 87–97. http://dx.doi.org/10.1007/978-3-030-12835-7_6
  8. W. B. Daszczuk, “Fairness in Temporal Verification of Distributed Systems,” in 13th International Conference on Dependability and Complex Systems DepCoS-RELCOMEX, 2-6 July 2018, Brunów, Poland, AISC vol.761, 2019, pp. 135–150. http://dx.doi.org/10.1007/978-3-319-91446-6_14
  9. R. M. Dijkman, M. Dumas, and C. Ouyang, “Semantics and analysis of business process models in BPMN,” Inf. Softw. Technol., vol. 50, no. 12, pp. 1281–1294, Nov. 2008. http://dx.doi.org/10.1016/j.infsof.2008.02.006
  10. J. Billington et al., “The Petri Net Markup Language: Concepts, Technology, and Tools,” in ICATPN 2003: Applications and Theory of Petri Nets, Eindhoven, The Netherlands, 23–27 June 2003, LNCS vol. 2679, 2003, pp. 483–505. http://dx.doi.org/10.1007/3-540-44919-1_31
  11. A. Rachdi, “Liveness and Reachability Analysis of BPMN Process Models,” J. Comput. Inf. Technol., vol. 24, no. 2, pp. 195–207, Jun. 2016. http://dx.doi.org/10.20532/cit.2016.1002774
  12. K. Kluza, K. Jobczyk, P. Wiśniewski, and A. Ligęza, “Overview of Time Issues with Temporal Logics for Business Process Models,” in 11 Federated Conference on Computer Science and Information Systems (FedCSIS), 11-14 Sept 2016, Gdansk, Poland, 2016, pp. 1115–1123. http://dx.doi.org/10.15439/2016F328
  13. C. Dechsupa, W. Vatanawood, and A. Thongtak, “Hierarchical Verification for the BPMN Design Model Using State Space Analysis,” IEEE Access, vol. 7, pp. 16795–16815, 2019. http://dx.doi.org/10.1109/ACCESS.2019.2892958
  14. L. Li and F. Dai, “Transformation and Visualization of BPMN Models to Petri Nets,” in International Conference of Green Buildings and Environmental Management (GBEM 2018), Qingdao, China, 23–25 Aug. 2018, IOP Conference Series: Earth and Environmental Science vol. 186, 2018, vol. 186, p. 012047. http://dx.doi.org/10.1088/1755-1315/186/5/012047
  15. R. Boussetoua, H. Bennoui, A. Chaoui, K. Khalfaoui, and E. Kerkouche, “An automatic approach to transform BPMN models to Pi-Calculus,” in 2015 IEEE/ACS 12th International Conference of Computer Systems and Applications (AICCSA), Marrakech, Morocco, 17-20 Nov. 2015, 2015, pp. 1–8. http://dx.doi.org/10.1109/AICCSA.2015.7507176
  16. S. Yamasathien and W. Vatanawood, “An approach to construct formal model of business process model from BPMN workflow patterns,” in Fourth International Conference on Digital Information and Communication Technology and its Applications (DICTAP), Bangkok, Thailand, 6-8 May 2014, 2014, pp. 211–215. http://dx.doi.org/10.1109/DICTAP.2014.6821684
  17. D. Prandi, P. Quaglia, and N. Zannone, “Formal Analysis of BPMN Via a Translation into COWS,” in International Conference on Coordination Models and Languages COORDINATION 2008: Oslo, Norway, 4-6 June 2008, LNCS, vol. 5052, 2008, pp. 249–263. http://dx.doi.org/10.1007/978-3-540-68265-3_16
  18. M. Szpyrka, G. J. Nalepa, and K. Kluza, “From Process Models to Concurrent Systems in Alvis Language,” Informatica, vol. 28, no. 3, pp. 525–545, Jan. 2017. http://dx.doi.org/10.15388/Informatica.2017.143
  19. J. Ye and W. Song, “Transformation of BPMN Diagrams to YAWL Nets,” J. Softw., vol. 5, no. 4, pp. 396–404, Apr. 2010. http://dx.doi.org/10.4304/jsw.5.4.396-404
  20. V. Rafe and A. T. Rahmani, “A Graph Transformation-Based Approach to Formal Modeling and Verification of Workflows,” in CSICC 2008: Advances in Computer Science and Engineering, Kish Island, Iran, 9-11 March 2008, 2008, pp. 291–298. http://dx.doi.org/10.1007/978-3-540-89985-3_36
  21. F. Corradini, F. Fornari, A. Polini, B. Re, F. Tiezzi, and A. Vandin, “BProVe: Tool support for business process verification,” in 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE), Urbana, IL, 30 Oct.-3 Nov. 2017, 2017, pp. 937–942. http://dx.doi.org/10.1109/ASE.2017.8115708
  22. F. Corradini, F. Fornari, A. Polini, B. Re, F. Tiezzi, and A. Vandin, “BProVe: A formal verification framework for business process models,” in 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE), Urbana, IL, 30 Oct.-3 Nov. 2017, 2017, pp. 217–228. http://dx.doi.org/10.1109/ASE.2017.8115635
  23. A. Krishna, P. Poizat, and G. Salaün, “VBPMN: Automated Verification of BPMN Processes,” in 13th International Conference on integrated Formal Methods (iFM 2017), Turin, Italy, Sep 2017, 2017, pp. 1–8. http://convecs.inria.fr/doc/publications/Krishna-Poizat-Salaun-17.pdf. Accessed on 23.07.2023
  24. G. Salaün and P. Poizat, “VBPMN Samples.” 2017. https://pascalpoizat.github.io/vbpmn-web/ Accessed on 23.07.2023
  25. N. Tantitharanukul, P. Sugunnasil, and W. Jumpamule, “Detecting deadlock and multiple termination in BPMN model using process automata,” in 2010 ECTI International Confernce on Electrical Engineering/Electronics, Computer, Telecommunications and Information Technology, Chiang Mai, Thailand, 19-21 May 2010, 2010, pp. 478–482. https://ieeexplore.ieee.org/document/5491443 Accessed on 23.07.2023
  26. W. B. Daszczuk, “Graphic modeling in Distributed Autonomous and Asynchronous Automata (DA3),” Softw. Syst. Model., vol. 20, no. 5, pp. 363–398, 2021. http://dx.doi.org/10.1007/s10270-021-00917-7
  27. K. Kluza and G. J. Nalepa, “Towards Rule-based Pattern Perspective for BPMN 2.0 Business Process Models,” in 11 Federated Conference on Computer Science and Information Systems (FedCSIS), 11-14 Sept 2016, Gdansk, Poland, 2016, pp. 1359–1364. http://dx.doi.org/10.15439/2016F324
  28. K. Kluza and P. Wiśniewski, “Spreadsheet-Based Business Process Modeling,” in 11 Federated Conference on Computer Science and Information Systems (FedCSIS), 11-14 Sept 2016, Gdansk, Poland, 2016, pp. 1355–1358. http://dx.doi.org/10.15439/2016F376
  29. W. M. P. van der Aalst, “Using Free-Choice Nets for Process Mining and Business Process Management,” in 16 Federated Conference on Computer Science and Information Systems (FedCSIS), 2-5 Sept 2021, Sofia, Bulgaria, 2021, pp. 9–15. http://dx.doi.org/10.15439/2021F002
  30. S. J. Niepostyn and I. Bluemke, “The Function-Behaviour-Structure Diagram for Modelling Workflow of Information Systems,” in CAiSE 2012: International Conference on Advanced Information Systems Engineering, Gdańsk, Poland, 25-26 June 2012, 2012, pp. 425–439. http://dx.doi.org/10.1007/978-3-642-31069-0_34
  31. S. Robak, B. Franczyk, and M. Robak, “Applying Linked Data concepts in BPM,” in 6 Federated Conference on Computer Science and Information Systems (FedCSIS), 9-12 Sept 2012, Wrocław, Poland, 2012, pp. 1105–1110. url: https://ieeexplore.ieee.org/abstract/document/6354386 Accessed on 23.07.2023
  32. A. Suchenia, P. Wiśniewski, and A. Ligęza, “Overview of Verification Tools for Business Process Models,” in 12 Federated Conference on Computer Science and Information Systems (FedCSIS), 3-6 Sept 2017, Prague, Czech Republic, 2017, pp. 295–302. http://dx.doi.org/10.15439/2017F308 http://dx.doi.org/10.15439/2017F308
  33. T. Lopes and S. Guerreiro, “Assessing business process models: a literature review on techniques for BPMN testing and formal verification,” Bus. Process Manag. J., vol. 29, no. 8, pp. 133–162, Apr. 2023. http://dx.doi.org/10.1108/BPMJ-11-2022-0557
  34. Z. Manna and A. Pnueli, The Temporal Logic of Reactive and Concurrent Systems. New York, NY: Springer, 1992. http://dx.doi.org/10.1007/978-1-4612-0931-7
  35. J. Jałowiec, “Translation of Business Process Model and Notation into Integrated Model of Distributed Systems,” B.Sc. thesis, Warsaw University of Technology, Institute of Computer Science, 2019. https://repo.pw.edu.pl/info/bachelor/WUT31de757656da422c87be61e7ede00630/?r=diploma&tab=&lang=pl Accessed on 23.07.2023
  36. F. Corradini, C. Muzi, B. Re, L. Rossi, and F. Tiezzi, “Global vs. Local Semantics of BPMN 2.0 OR-Join,” in 44th International Conference on Current Trends in Theory and Practice of Computer Science, Krems, Austria, 29 Jan. - 2 Feb., 2018, LNCS, vol. 10706, 2018, pp. 321–336. http://dx.doi.org/10.1007/978-3-319-73117-9_23
  37. G. Behrmann, A. David, K. G. Larsen, P. Pettersson, and W. Yi, “Developing UPPAAL over 15 years,” Softw. Pract. Exp., vol. 41, no. 2, pp. 133–142, Feb. 2011. http://dx.doi.org/10.1002/spe.1006
  38. W. B. Daszczuk, “Evaluation of temporal formulas based on ‘Checking By Spheres,’” in Euromicro Symposium on Digital Systems Design, Warsaw, Poland, 4-6 Sept. 2001, 2001, pp. 158–164. http://dx.doi.org/10.1109/DSD.2001.952267