Logo PTI
Polish Information Processing Society
Logo FedCSIS

Annals of Computer Science and Information Systems, Volume 13

Communication Papers of the 2017 Federated Conference on Computer Science and Information Systems

Overview of Verification Tools for Business Process Models

, ,

DOI: http://dx.doi.org/10.15439/2017F308

Citation: Communication Papers of the 2017 Federated Conference on Computer Science and Information Systems, M. Ganzha, L. Maciaszek, M. Paprzycki (eds). ACSIS, Vol. 13, pages 295–302 ()

Full text

Abstract. Formal verification of process models is an important issue in Business Process Management. Such a verification provides the information about the correctness of a process model, can be also used for checking business compliance or as a preliminary step to simulation. In this paper, we provide an overview of the existing tools for such a verification.

References

  1. F. Friedrich, J. Mendling, and F. Puhlmann, “Process model generation from natural language text,” in Advanced Information Systems Engineering, ser. Lecture Notes in Computer Science, H. Mouratidis and C. Rolland, Eds. Springer Berlin Heidelberg, 2011, vol. 6741, pp. 482–496.
  2. K. Kluza and K. Honkisz, “From SBVR to BPMN and DMN models. proposal of translation from rules to process and decision models,” in Artificial Intelligence and Soft Computing: 15th International Conference, ICAISC 2016, Zakopane, Poland, June 12-16, 2016, Proceedings, Part II, ser. Lecture Notes in Computer Science, L. Rutkowski, M. Korytkowski, R. Scherer, R. Tadeusiewicz, L. A. Zadeh, and J. M. Zurada, Eds. Springer International Publishing, 2016, vol. 9693, pp. 453–462.
  3. K. Kluza and P. Wiśniewski, “Spreadsheet-based business process modeling,” in Computer Science and Information Systems (FedCSIS), 2016 Federated Conference on. IEEE, 2016, pp. 1355–1358.
  4. J. R. Nawrocki, T. Nedza, M. Ochodek, and L. Olek, “Describing business processes with use cases,” in BIS, 2006, pp. 13–27.
  5. A. A. Kalenkova, M. de Leoni, and W. M. van der Aalst, “Discovering, analyzing and enhancing BPMN models using ProM?” in Business Process Management-12th International Conference, BPM, 2014, pp. 7–11.
  6. A. Ligęza, K. Kluza, and T. Potempa, “AI approach to formal analysis of BPMN models. towards a logical model for BPMN diagrams,” in Proceedings of the Federated Conference on Computer Science and Information Systems – FedCSIS 2012, Wroclaw, Poland, 9-12 September 2012, M. Ganzha, L. A. Maciaszek, and M. Paprzycki, Eds., 2012, pp. 931–934.
  7. A. Suchenia and A. Ligęza, “Event anomalies in modeling with BPMN,” International Journal of Computer Technology & Applications, vol. 6, no. 5, pp. 789–797, 2015.
  8. A. Mroczek and A. Ligeza, “A note on BPMN analysis. Towards a taxonomy of selected potential anomalies,” in Computer Science and Information Systems (FedCSIS), 2014 Federated Conference on. IEEE, 2014, pp. 1097–1102.
  9. M. A. Mach and M. L. Owoc, “Validation as the integral part of a knowledge management process,” in Proceeding of Informing Science Conference, 2001.
  10. M. Mach-Król and K. Michalik, “Validation and verification of temporal knowledge as an important aspect of implementing a temporal knowledge base system supporting organizational creativity,” in Computer Science and Information Systems (FedCSIS), 2015 Federated Conference on. IEEE, 2015, pp. 1315–1320.
  11. M. Mach-Król and K. Michalik, “Verification of temporal knowledge bases as an important aspect of knowledge management processes in organization,” in Advances in Business ICT: New Ideas from Ongoing Research. Springer, 2017, pp. 1–15.
  12. OMG, “Business Process Model and Notation (BPMN): Version 2.0 specification,” Object Management Group, Tech. Rep. formal/2011-01-03, January 2011.
  13. A. Yousfi, C. Bauer, R. Saidi, and A. K. Dey, “ubpmn: A bpmn extension for modeling ubiquitous business processes,” Information and Software Technology, vol. 74, pp. 55–68, 2016.
  14. R. Martinho, D. Domingos, and J. Varajão, “Cf4bpmn: a bpmn extension for controlled flexibility in business processes,” Procedia Computer Science, vol. 64, pp. 1232–1239, 2015.
  15. R. M. Pillat, T. C. Oliveira, P. S. Alencar, and D. D. Cowan, “Bpmnt: A bpmn extension for specifying software process tailoring,” Information and Software Technology, vol. 57, pp. 95–115, 2015.
  16. K. Kluza, K. Jobczyk, P. Wiśniewski, and A. Ligęza, “Overview of time issues with temporal logics for business process models,” in Computer Science and Information Systems (FedCSIS), 2016 Federated Conference on. IEEE, 2016, pp. 1115–1123.
  17. K. Kluza and K. Kaczor, “Overview of BPMN model equivalences: towards normalization of BPMN diagrams,” in 8th Workshop on Knowledge Engineering and Software Engineering (KESE2012) at the at the biennial European Conference on Artificial Intelligence (ECAI 2012): August 28, 2012, Montpellier, France, J. Canadas, G. J. Nalepa, and J. Baumeister, Eds., 2012, pp. 38–45. [Online]. Available: http://ceur-ws.org/Vol-949/
  18. V. S. W. Lam, “Equivalences of BPMN processes,” Service Oriented Computing and Applications, vol. 3, no. 3, pp. 189–204, 2009.
  19. S. Bobek, G. J. Nalepa, and O. Grodzki, “Integration of activity modeller with bayesian network based recommender for business processes,” in Proceedings of 10th Workshop on Knowledge Engineering and Software Engineering (KESE10) co-located with 21st European Conference on Artificial Intelligence (ECAI 2014), Prague, Czech Republic, August 19 2014, ser. CEUR Workshop Proceedings, G. J. Nalepa and J. Baumeister, Eds., vol. 1289, 2014. [Online]. Available: http://ceur-ws.org/Vol-1289/kese10-05_submission_10.pdf
  20. S. Bobek, M. Baran, K. Kluza, and G. J. Nalepa, “Application of bayesian networks to recommendations in business process modeling,” in Proceedings of the Workshop AI Meets Business Processes 2013 co-located with the 13th Conference of the Italian Association for Artificial Intelligence (AI*IA 2013), Turin, Italy, December 6, 2013, L. Giordano, S. Montani, and D. T. Dupre, Eds., 2013. [Online]. Available: http://ceur-ws.org/Vol-1101/
  21. K. Kluza, M. Baran, S. Bobek, and G. J. Nalepa, “Overview of recommendation techniques in business process modeling,” in Proceedings of 9th Workshop on Knowledge Engineering and Software Engineering (KESE9) co-located with the 36th German Conference on Artificial Intelligence (KI2013), Koblenz, Germany, September 17, 2013, G. J. Nalepa and J. Baumeister, Eds., 2013. [Online]. Available: http://ceur-ws.org/Vol-1070/
  22. G. J. Nalepa, K. Kluza, and U. Ciaputa, “Proposal of automation of the collaborative modeling and evaluation of business processes using a semantic wiki,” in Proceedings of the 17th IEEE International Conference on Emerging Technologies and Factory Automation ETFA 2012, Kraków, Poland, 28 September 2012, 2012.
  23. K. Kluza, K. Kaczor, G. Nalepa, and M. Slazynski, “Opportunities for business process semantization in open-source process execution environments,” in Computer Science and Information Systems (FedCSIS), 2015 Federated Conference on, Sept 2015, pp. 1307–1314.
  24. K. Kluza, G. J. Nalepa, M. Ślażyński, K. Kutt, E. Kucharska, K. Kaczor, and A. Łuszpaj, “Overview of selected business process semantization techniques,” in Advances in Business ICT: New Ideas from Ongoing Research. Springer, 2017, pp. 45–64.
  25. W. T. Adrian, S. Bobek, G. J. Nalepa, K. Kaczor, and K. Kluza, “How to reason by HeaRT in a semantic knowledge-based wiki,” in Proceedings of the 23rd IEEE International Conference on Tools with Artificial Intelligence, ICTAI 2011, Boca Raton, Florida, USA, November 2011, pp. 438–441. [Online]. Available: http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=6103361&tag=1
  26. J. Mendling, H. Verbeek, B. F. van Dongen, W. M. van der Aalst, and G. Neumann, “Detection and prediction of errors in epcs of the sap reference model,” Data & Knowledge Engineering, vol. 64, no. 1, pp. 312–329, 2008.
  27. A. Hallerbach, T. Bauer, and M. Reichert, “Capturing variability in business process models: the provop approach,” Journal of Software Maintenance and Evolution: Research and Practice, vol. 22, no. 6-7, pp. 519–546, 2010.
  28. A. Suchenia, T. Potempa, A. Ligęza, K. Jobczyk, and K. Kluza, “Selected approaches towards taxonomy of business process anomalies,” in Advances in Business ICT: New Ideas from Ongoing Research. Springer, 2017, pp. 65–85.
  29. I. Group et al., “1044-2009-ieee standard classification for software anomalies,” IEEE, New York, 2010. [Online]. Available: https: //standards.ieee.org/findstds/standard/1044-2009.html
  30. R. Laue and A. Awad, “Visualization of business process modeling anti patterns,” Electronic Communications of the EASST, vol. 25, 2009.
  31. S. Kühne, H. Kern, V. Gruhn, and R. Laue, “Business process modeling with continuous validation,” Journal of Software Maintenance and Evolution: Research and Practice, vol. 22, no. 6-7, pp. 547–566, 2010.
  32. N. Trčka, W. M. Van der Aalst, and N. Sidorova, “Data-flow antipatterns: Discovering data-flow errors in workflows,” in Advanced Information Systems Engineering. Springer, 2009, pp. 425–439.
  33. A. Kheldoun, K. Barkaoui, and M. Ioualalen, “Formal verification of complex business processes based on high-level petri nets,” Information Sciences, vol. 385–386, pp. 39 – 54, 2017.
  34. V. S. W. Lam, “Formal analysis of BPMN models: a NuSMV-based approach,” International Journal of Software Engineering and Knowledge Engineering, vol. 20, no. 7, pp. 987–1023, 2010.
  35. N. Lohmann and K. Wolf, “How to implement a theory of correctness in the area of business processes and services,” in Business Process Management. Springer, 2010, pp. 61–77.
  36. S. A. White, “Process modeling notations and workflow patterns,” Workflow handbook, vol. 2004, pp. 265–294, 2004.
  37. L. Olkhovich, “Semi-automatic business process performance optimization based on redundant control flow detection,” in Telecommunications, 2006. AICT-ICIW’06. International Conference on Internet and Web Applications and Services/Advanced International Conference on. IEEE, 2006, pp. 146–146.
  38. S. Roy and A. S. M. Sajeev, “A formal framework for diagnostic analysis for errors of business processes,” in Transactions on Petri Nets and Other Models of Concurrency XI, M. Koutny, J. Desel, and J. Kleijn, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2016, pp. 226–261.
  39. H. Groefsema and D. Bucur, “A survey of formal business process verification: From soundness to variability,” in Proceedings of International Symposium on Business Modeling and Software Design. SciTePress, 2013, pp. 198–203.
  40. R. Klimek, “A system for deduction-based formal verification of workflow-oriented software models,” International Journal of Applied Mathematics and Computer Science, vol. 24, no. 4, pp. 941–956, 2014.
  41. C. Ou-Yang and Y. D. Lin, “BPMN-based business process model feasibility analysis: a petri net approach,” International Journal of Production Research, vol. 46, no. 14, pp. 3763–3781, 2008.
  42. R. Liu and A. Kumar, “An analysis and taxonomy of unstructured workflows,” in Business Process Management. Springer, 2005, pp. 268–284.
  43. O. Allani and S. A. Ghannouchi, “Verification of BPMN 2.0 process models: An event log-based approach,” Procedia Computer Science, vol. 100, pp. 1064 – 1070, 2016.
  44. A. Badica and C. Badica, “Formal verification of business processes represented as role activity diagrams,” in Federated Conference on Computer Science and Information Systems – FedCSIS 2011, Szczecin, Poland, 18-21 September 2011, Proceedings, M. Ganzha, L. A. Maciaszek, and M. Paprzycki, Eds., 2011, pp. 277–280.
  45. A. Badica and C. Badica, “Fsp and fltl framework for specification and verification of middle-agents,” Applied Mathematics and Computer Science, vol. 21, no. 1, pp. 9–25, 2011.
  46. J. Stepaniuk, J. G. Bazan, and A. Skowron, “Modelling complex patterns by information systems,” Fundam. Inform., vol. 67, no. 1-3, pp. 203–217, 2005.
  47. D. Xu, K. Xia, D. Zhang, and H. Zhang, “Model checking the inconsistency and circularity in rule-based expert systems,” Computer and Information Science, vol. 2, no. 1, p. 12, 2009.
  48. A. K. Zaidi and A. H. Levis, “Validation and verification of decision making rules,” Automatica, vol. 33, no. 2, pp. 155–169, 1997.
  49. M. Dohring and S. Heublein, “Anomalies in rule-adapted workflows—a taxonomy and solutions for vbpmn,” in Software Maintenance and Reengineering (CSMR), 2012 16th European Conference on. IEEE, 2012, pp. 117–126.
  50. A. Ligęza and G. J. Nalepa, “A study of methodological issues in design and development of rule-based systems: proposal of a new approach,” Wiley Interdisciplinary Reviews: Data Mining and Knowledge Discovery, vol. 1, no. 2, pp. 117–137, 2011.
  51. M. A. Mach and P. J. Kalczynski, “Technique for reducing the number of rules in a temporal knowledge base.” in BIS, 2006, pp. 442–454.
  52. A. Rachdi, A. En-Nouaary, and M. Dahchour, “Verification of common business rules in bpmn process models,” in Networked Systems: 4th International Conference, NETYS 2016, Marrakech, Morocco, May 18-20, 2016, Revised Selected Papers, P. A. Abdulla and C. Delporte-Gallet, Eds. Cham: Springer International Publishing, 2016, pp. 334–339.
  53. S. Cheikhrouhou, S. Kallel, N. Guermouche, and M. Jmaiel, “The Temporal Perspective in Business Process Modeling : An Evaluative Survey and Research Challenges,” Service Oriented Computing and Applications, vol. 9, no. 1, pp. 75–85, 2015.
  54. R. Klimek and P. Szwed, “Verification of archimate process specifications based on deductive temporal reasoning,” in Computer Science and Information Systems (FedCSIS), 2013 Federated Conference on. IEEE, 2013, pp. 1109–1116.
  55. Y. Du, P. Xiong, Y. Fan, and X. Li, “Dynamic checking and solution to temporal violations in concurrent workflow processes,” IEEE Transactions on Systems, Man, and Cybernetics - Part A: Systems and Humans, vol. 41, no. 6, pp. 1166–1181, 2011.
  56. K. Watahiki, F. Ishikawa, and K. Hiraishi, “Formal verification of business processes with temporal and resource constraints,” in Systems, Man, and Cybernetics (SMC), 2011 IEEE International Conference on, 2011, pp. 1173–1180.
  57. L. E. Mendoza Morales, C. Monsalve, and M. Villavicencio, “Application of formal methods to verify business processes,” in Formal Methods: Foundations and Applications: 19th Brazilian Symposium, SBMF 2016, Natal, Brazil, November 23-25, 2016, Proceedings, L. Ribeiro and T. Lecomte, Eds. Cham: Springer International Publishing, 2016, pp. 41–58.
  58. L. Giordano, A. Martelli, M. Spiotta, and D. T. Dupre, “Business process verification with constraint temporal answer set programming,” Theory and Practice of Logic Programming, vol. 13, no. 4-5, pp. 641–655, 2013.
  59. L. E. Mendoza Morales, “Business process verification: The application of model checking and timed automata,” CLEI Electronic Journal, vol. 17, no. 2, 2014.
  60. W. M. van der Aalst, A. Hirnschall, and H. Verbeek, “An alternative way to analyze workflow graphs,” in Advanced Information Systems Engineering. Springer, 2002, pp. 535–552.
  61. L. Hong and Z. J. Bo, “Research on workflow process structure verification,” in e-Business Engineering, 2005. ICEBE 2005. IEEE International Conference on. IEEE, 2005, pp. 158–165.
  62. H. Lin, Z. Zhao, H. Li, and Z. Chen, “A novel graph reduction algorithm to identify structural conflicts,” in System Sciences, 2002. HICSS. Proceedings of the 35th Annual Hawaii International Conference on. IEEE, 2002, pp. 10–pp.
  63. G.-W. Kim, J. H. Lee, and J. H. Son, “Classification and analyses of business process anomalies,” in Communication Software and Networks, 2009. ICCSN’09. International Conference on. IEEE, 2009, pp. 433–437.
  64. E. Börger, O. Sörensen, and B. Thalheim, “On defining the behavior of or-joins in business process models.” Journal of Universal Computer Science, vol. 15, no. 1, pp. 3–32, 2009.
  65. Signavio, “Following academic signavio,” http://www.signavio.com/bpm-academic-initiative/, 2009, accessed: 2017-05-01.
  66. C. Pan, J. Guo, L. Zhu, J. Shi, H. Zhu, and X. Zhou, “Modeling and verification of can bus with application layer using uppaal,” Electronic Notes in Theoretical Computer Science, vol. 309, pp. 31–49, 2014.
  67. Basic Research in Computer Science at Aalborg University in Denmark and the Department of Information Technology at Uppsala University in Sweden, “Uppaal,” http://www.uppaal.org/, 1999, accessed: 2017-05-01.
  68. G. Rodriguez-Navas, J. Proenza, and H. Hansson, “An uppaal model for formal verification of master/slave clock synchronization over the controller area network,” in Proc. of the 6th IEEE International Workshop on Factory Communication Systems, Torino, Italy, IEEE Computer Society Press, Los Alamitos, 2006.
  69. Bell Labs, “Spin,” http://spinroot.com/spin/whatispin.html, 1990, accessed: 2017-05-01.
  70. W. M. Van Der Aalst, “Woflan: a petri-net-based workflow analyzer,” Systems Analysis Modelling Simulation, vol. 35, no. 3, pp. 345–358, 1999.
  71. H. M. Verbeek, T. Basten, and W. M. van der Aalst, “Diagnosing workflow processes using woflan,” The computer journal, vol. 44, no. 4, pp. 246–279, 2001.
  72. Eindhoven University of Technology, “Woflan – the workflow analyser,” http://www.win.tue.nl/woflan/, 1998, accessed: 2017-05-01.
  73. A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri, “Nusmv: A new symbolic model verifier,” in International conference on computer aided verification. Springer, 1999, pp. 495–499.
  74. A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri, “Nusmv: a new symbolic model checker,” International Journal on Software Tools for Technology Transfer, vol. 2, no. 4, pp. 410–425, 2000.
  75. M. Szpyrka, A. Biernacka, and J. Biernacki, “Methods of translation of petri nets to nusmv language.” in CS&P, 2014, pp. 245–256.
  76. P. Szwed, “Evaluating efficiency of archimate business processes verification with nusmv,” in Information Technology for Management. Springer, 2016, pp. 179–196.
  77. R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, and S. Tonetta, “The nuxmv symbolic model checker,” in International Conference on Computer Aided Verification. Springer, 2014, pp. 334–342.
  78. A. Biernacka, J. Biernacki, M. Szpyrka, T. E. Simos, Z. Kalogiratou, and T. Monovasilis, “State-based verification of rtcp-nets with nuxmv,” in AIP Conference Proceedings, vol. 1702, no. 1. AIP Publishing, 2015, p. 100011.
  79. M. Szpyrka, P. Matyasik, and R. Mrówka, “Alvis – modelling language for concurrent systems,” in Intelligent Decision Systems in Large-Scale Distributed Environments, ser. Studies in Computational Intelligence, P. Bouvry, H. Gonzalez-Velez, and J. Kołodziej, Eds. Springer-Verlag, 2011, vol. 362, ch. 15, pp. 315–341.
  80. M. Szpyrka, P. Matyasik, and M. Wypych, “Generation of labelled transition systems for alvis models using haskell model representation,” in Proceedings of the 22nd International Workshop on Concurrency, Specification and Programming (CS&P 2013), vol. 1032. Warsaw, Poland: CEUR Workshop Proceedings, 2013, pp. 409–420.
  81. M. Szpyrka, P. Matyasik, R. Mrówka, and L. Kotulski, “Formal description of Alvis language with α 0 system layer,” Fundamenta Informaticae, vol. 129, no. 1-2, pp. 161–176, 2014.
  82. T. Szmuc and M. Szpyrka, “Formal methods – support or scientific decoration in software development,” in Proc. of Mixdes 2015, the 22nd International Conference Mixed Design of Integrated Circuits and Systems, Torun, Poland, June 25–27 2015, pp. 24–31.
  83. M. Szpyrka, P. Matyasik, J. Biernacki, A. Biernacka, M. Wypych, and L. Kotulski, “Hierarchical communication diagrams,” Computing and Informatics, vol. 35, no. 1, pp. 55–83, 2016.
  84. M. Wypych, M. Szpyrka, and P. Matyasik, “Extension of Alvis compiler front-end,” in International Conference of Computational Methods in Sciences and Engineering (ICCMSE 2015), ser. AIP Conference Proceedings, vol. 1702. Athens, Greece: AIP Publishing, March 20-23 2015, pp. 100 015–1–100 015–4.
  85. M. Szpyrka, G. J. Nalepa, A. Ligęza, and K. Kluza, “Proposal of formal verification of selected BPMN models with Alvis modeling language,” in Intelligent Distributed Computing V. Proceedings of the 5th International Symposium on Intelligent Distributed Computing – IDC 2011, Delft, the Netherlands – October 2011, ser. Studies in Computational Intelligence, F. M. Brazier, K. Nieuwenhuis, G. Pavlin, M. Warnier, and C. Badica, Eds. Springer-Verlag, 2011, vol. 382, pp. 249–255. [Online]. Available: http://www.springerlink.com/content/m181144037q67271/
  86. K. Kluza, G. J. Nalepa, M. Szpyrka, and A. Ligęza, “Proposal of a hierarchical approach to formal verification of BPMN models using Alvis and XTT2 methods,” in 7th Workshop on Knowledge Engineering and Software Engineering (KESE2011) at the Conference of the Spanish Association for Artificial Intelligence (CAEPIA 2011): November 10, 2011, La Laguna (Tenerife), Spain, J. Canadas, G. J. Nalepa, and J. Baumeister, Eds., 2011, pp. 15–23. [Online]. Available: http://ceur-ws.org/Vol-805/
  87. M. Szpyrka, P. Matyasik, and M. Wypych, “Alvis language with time dependence,” in Proceedings of the Federated Conference on Computer Science and Information Systems, Krakow, Poland, 2013, pp. 1607–1612.
  88. P. Matyasik, “Alvis virtual machine,” in Proceedings of the Federated Conference on Computer Science and Information Systems, 2014, pp. 1639–1645.
  89. M. Szpyrka, P. Matyasik, L. Podolski, and M. Wypych, Simulation of Multi-agent Systems with Alvis Toolkit. Zakopane, Poland: Springer International Publishing, 2017, pp. 599–608. [Online]. Available: http://dx.doi.org/10.1007/978-3-319-59060-8_54
  90. M. Mach-Król, “Tools for building a temporal knowledge base system supporting organizational creativity,” Procedia Computer Science, vol. 65, pp. 1031–1037, 2015.
  91. E. Kucharska, K. Grobler-Dębska, J. Gracel, and M. Jagodziński, “Idea of impact of erp-aps-mes systems integration on the effectiveness of decision making process in manufacturing companies,” in International Conference: Beyond Databases, Architectures and Structures. Springer, 2015, pp. 551–564.
  92. E. Dudek-Dyduch, E. Kucharska, L. Dutkiewicz, and K. Rączka, “Almm solver-a tool for optimization problems,” in International Conference on Artificial Intelligence and Soft Computing. Springer, 2014, pp. 328–338.
  93. E. Kucharska, K. Grobler-Dębska, and K. Rączka, “Almm-based methods for optimization makespan flow-shop problem with defects,” in Information Systems Architecture and Technology: Proceedings of 37th International Conference on Information Systems Architecture and Technology–ISAT 2016–Part I. Springer, 2017, pp. 41–53.