×

Formal verification of complex business processes based on high-level Petri nets. (English) Zbl 1429.68147

Summary: The Business Process Modeling Notation (BPMN) has been widely used as a tool for business process modeling. However, BPMN suffers from a lack of standard formal semantics. This weakness can lead to inconsistencies, ambiguities, and incompletenesses within the developed models. In this paper, we propose a formal semantics of BPMN using recursive ECATNets. Owing to this formalism, a large set of BPMN features such as cancellation, multiple instantiation of subprocesses and exception handling can be covered while taking into account the data flow aspect. The benefits and usefulness of this modelling are illustrated through three examples. Moreover, since recursive ECATNets semantics is defined in terms of conditional rewriting logic, one can use the Maude LTL model checker to verify several behavioral properties related to BPMN models. The work presented in this document has been automated through the development of a first prototype.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q42 Grammars and rewriting systems
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

YAWL; Woflan; PNML; ATL
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] van der Aalst, W. M.P.; ter Hofstede, A. H.M., YAWL: yet another workflow language, Inf. Syst., 30, 4, 245-275 (2005)
[2] Barkaoui, K.; Boucheneb, H.; Hicheur, A., Modelling and analysis of time-constrained flexible workflows with time recursive ecatnets, (Bruni, R.; Wolf, K., Web Services and Formal Methods. Web Services and Formal Methods, Lecture Notes in Computer Science, vol. 5387 (2009), Springer Berlin Heidelberg), 19-36
[3] Barkaoui, K.; Hicheur, A., Towards analysis of flexible and collaborative workflow using recursive ecatnets, (ter Hofstede, A.; Benatallah, B.; Paik, H.-Y., Business Process Management Workshops. Business Process Management Workshops, Lecture Notes in Computer Science, vol. 4928 (2008), Springer Berlin Heidelberg), 232-244
[4] Billington, J.; Christensen, S.; van Hee, K.; Kindler, E.; Kummer, O.; Petrucci, L.; Post, R.; Stehno, C.; Weber, M., The Petri net markup language: concepts, technology, and tools, (van der Aalst, W.; Best, E., Applications and Theory of Petri Nets 2003. Applications and Theory of Petri Nets 2003, Lecture Notes in Computer Science, vol. 2679 (2003), Springer Berlin Heidelberg), 483-505
[5] Ou-Yang, C.; Lin, Y. D., BPMN-based business process model feasibility analysis: a Petri net approach, Int. J. Prod. Res., 46, 14, 3763-3781 (2008)
[6] Dijkman, R. M.; Dumas, M.; Ouyang, C., Semantics and analysis of business process models in BPMN, Inf. Softw. Technol., 50, 12, 1281-1294 (2008)
[7] Dufourd, C.; Finkel, A.; Schnoebelen, P., Reset nets between decidability and undecidability, 25th International Colloquium on Automata, Languages and Programming, ICALP ’98, 103-115 (1998), Springer-Verlag · Zbl 0909.68124
[8] Eker, S.; Meseguer, J.; Sridharanarayanan, A., The maude LTL model checker, Electron Notes Theor. Comput. Sci., 71, 162-187 (2004) · Zbl 1272.68243
[9] El-Saber, N.; Boronat, A., BPMN formalization and verification using maude, Proceedings of the 2014 Workshop on Behaviour Modelling-Foundations and Applications, BM-FA ’14, 1:1-1:12 (2014), ACM
[10] Haddad, S.; Poitrenaud, D., Recursive Petri nets, Acta Inf., 44, 7-8, 463-508 (2007) · Zbl 1133.68056
[11] Hicheur, A., Modélisation et Analyse des Processus Workflows Reconfigurables et Distribués par les Ecatnets Récursifs (2009), CNAM 2009, Paris, Thèse de doctorat en Informatique
[12] Rao, J.; Chiotti, O.; Villarreal, P., Specification of behavioral anti-patterns for the verification of block-structured collaborative business processes, Inf. Softw. Technol., 75, 148-170 (2016)
[13] Jouault, F.; Allilaire, F.; Bzivin, J.; Kurtev, I., ATL: a model transformation tool, Sci. Comput. Program., 72, 12, 31-39 (2008) · Zbl 1154.68366
[14] Kheldoun, A.; Barkaoui, K.; Ioualalen, M., Specification and verification of complex business processes - a high-level Petri net-based approach, (Motahari-Nezhad, H. R.; Recker, J.; Weidlich, M., Business Process Management. Business Process Management, Lecture Notes in Computer Science, vol. 9253 (2015), Springer International Publishing), 55-71
[15] Liu, C.; Zhang, F., Petri net based modeling and correctness verification of collaborative emergency response processes, Cybern. Inf. Technol., 16, 3, 122-136 (2016)
[16] Lu, F.; Zeng, Q.; Bao, Y.; Duan, H., Hierarchy modeling and formal verification of emergency treatment processes, Syst Man Cybern, 44, 2, 220-234 (2014)
[17] Meseguer, J., Conditional rewriting logic as a unified model of concurrency, Theor. Comput. Sci., 96, 1, 73-155 (1992) · Zbl 0758.68043
[18] Morimoto, S., A survey of formal verification for business process modeling, (Bubak, M.; van Albada, G.; Dongarra, J.; Sloot, P., Computational Science ICCS 2008. Computational Science ICCS 2008, Lecture Notes in Computer Science, vol. 5102 (2008), Springer Berlin Heidelberg), 514-522
[19] (OMG), O. M.G., Business Process Model and Notation (BPMN) Version 2.0, Technical Report (2011)
[20] Ouyang, C.; Verbeek, E.; van der Aalst, W.; Breutel, S.; Dumas, M.; ter Hofstede, A., WofBPEL: a tool for automated analysis of BPEL processes, (Benatallah, B.; Casati, F.; Traverso, P., Service-Oriented Computing - ICSOC 2005. Service-Oriented Computing - ICSOC 2005, Lecture Notes in Computer Science, vol. 3826 (2005), Springer Berlin Heidelberg), 484-489
[21] Puhlmann, F.; Weske, M., Investigations on soundness regarding lazy activities, (Dustdar, S.; Fiadeiro, J.; Sheth, A., Business Process Management. Business Process Management, Lecture Notes in Computer Science, vol. 4102 (2006), Springer Berlin Heidelberg), 145-160
[22] Russell, N.; ter Hofstede, A. H.M.; van der Aalst, W. M.P.; Mulyar, N., Workflow Control-Flow Patterns: A Revised View, Technical Report (2006), BPMcenter.org
[23] Verbeek, E.; van der Aalst, W., Woflan 2.0 a Petri-net-based workflow diagnosis tool, (Nielsen, M.; Simpson, D., Application and Theory of Petri Nets 2000. Application and Theory of Petri Nets 2000, Lecture Notes in Computer Science, vol. 1825 (2000), Springer Berlin Heidelberg), 475-484 · Zbl 0986.68781
[24] Villarreal, P. D.; Lazarte, I.; Roa, J.; Chiotti, O., A Modeling Approach for Collaborative Business Processes Based on the UP-ColBPIP Language, 318-329 (2010), Springer: Springer Berlin, Heidelberg
[25] Watahiki, K.; Ishikawa, F.; Hiraishi, K., Formal verification of business processes with temporal and resource constraints, Systems, Man, and Cybernetics (SMC), 2011 IEEE International Conference on, 1173-1180 (2011)
[26] Wong, P. Y.; Gibbons, J., Formalisations and applications of BPMN, Sci. Comput. Program., 76, 8, 633-650 (2011) · Zbl 1213.68212
[27] Ye, J.; Sun, S.; Song, W.; Wen, L., Formal semantics of BPMN process models using YAWL, Intelligent Information Technology Application, 2008. IITA ’08. Second International Symposium on, volume 2, 70-74 (2008)
[28] Zeng, Q.; Lu, F.; Liu, C.; Duan, H.; Zhou, C., Modeling and verification for cross-department collaborative business processes using extended Petri nets, Syst. Man Cybern, 45, 2, 349-362 (2015)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.