×

Reduction of workflow nets for generalised soundness verification. (English) Zbl 1484.68139

Bouajjani, Ahmed (ed.) et al., Verification, model checking, and abstract interpretation. 18th international conference, VMCAI 2017, Paris, France, January 15–17, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10145, 91-111 (2017).
Summary: This paper proposes a reduction method to verify the generalised soundness of large workflows described as workflow nets-a suited class of Petri nets. The proposed static analysis method is based on the application of six novel reduction transformations that transform a workflow net into a smaller one while preserving generalised soundness. The soundness of the method is proved. As practical contributions, this paper presents convincing experimental results obtained using a dedicated tool, developed to validate and demonstrate the effectiveness, efficiency and scalability of this method over a large set of industrial workflow nets.
For the entire collection see [Zbl 1355.68009].

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] van der Aalst, W.M.: Three good reasons for using a Petri-net-based workflow management system. J. Inf. Process Integr. Enterprises 428, 161–182 (1997)
[2] Dittrich, G.: Specification with nets. In: Pichler, F., Moreno-Diaz, R. (eds.) EUROCAST 1989. LNCS, vol. 410, pp. 111–124. Springer, Heidelberg (1990). doi: 10.1007/3-540-52215-8_10 · doi:10.1007/3-540-52215-8_10
[3] van der Aalst, W.M.P., Barros, A.P., Hofstede, A.H.M., Kiepuszewski, B.: Advanced workflow patterns. In: Scheuermann, P., Etzion, O. (eds.) CoopIS 2000. LNCS, vol. 1901, pp. 18–29. Springer, Heidelberg (2000). doi: 10.1007/10722620_2 · doi:10.1007/10722620_2
[4] Suzuki, I., Murata, T.: A method for stepwise refinement and abstraction of Petri nets. J. Comput. Syst. Sci. 27(1), 51–76 (1983) · Zbl 0515.68051 · doi:10.1016/0022-0000(83)90029-6
[5] van der Aalst, W.M., van Hee, K.M., ter Hofstede, A.H., Sidorova, N., Verbeek, H., Voorhoeve, M., Wynn, M.T.: Soundness of workflow nets: classification, decidability, and analysis. J. Formal Aspects Comput. 23(3), 333–363 (2011) · Zbl 1225.68129 · doi:10.1007/s00165-010-0161-4
[6] Lipton, R.: The reachability problem requires exponential space. Research report (Yale University. Department of Computer Science). Department of Computer Science, Yale University (1976)
[7] Murata, T.: Petri nets: Properties, analysis and applications. IEEE 77(4), 541–580 (1989) · doi:10.1109/5.24143
[8] Valmari, A.: The state explosion problem. In: Reisig, W., Rozenberg, G. (eds.) ACPN 1996. LNCS, vol. 1491, pp. 429–528. Springer, Berlin (1998). doi: 10.1007/3-540-65306-6_21 · doi:10.1007/3-540-65306-6_21
[9] Mendling, J., Moser, M., Neumann, G., Verbeek, H.M.W., van Dongen, B.F., van der Aalst, W.M.P.: Faulty EPCs in the SAP reference model. In: Dustdar, S., Fiadeiro, J.L., Sheth, A.P. (eds.) BPM 2006. LNCS, vol. 4102, pp. 451–457. Springer, Berlin (2006). doi: 10.1007/11841760_38 · doi:10.1007/11841760_38
[10] van Dongen, B.F., Jansen-Vullers, M.H., Verbeek, H.M.W., van der Aalst, W.M.: Verification of the SAP reference models using EPC reduction, state-space analysis, and invariants. Comput. Ind. 58(6), 578–601 (2007) · doi:10.1016/j.compind.2007.01.001
[11] Mendling, J., Verbeek, H.M.W., van Dongen, B.F., van der Aalst, W.M., Neumann, G.: Detection and prediction of errors in EPCs of the SAP reference model. Data Knowl. Eng. 64(1), 312–329 (2008) · doi:10.1016/j.datak.2007.06.019
[12] Fahland, D., Favre, C., Jobstmann, B., Koehler, J., Lohmann, N., Völzer, H., Wolf, K.: 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, Berlin (2009). doi: 10.1007/978-3-642-03848-8_19 · Zbl 05606611 · doi:10.1007/978-3-642-03848-8_19
[13] Esparza, J., Hoffmann, P.: Reduction rules for colored workflow nets. In: Stevens, P., Wąsowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 342–358. Springer, Heidelberg (2016). doi: 10.1007/978-3-662-49665-7_20 · Zbl 06571887 · doi:10.1007/978-3-662-49665-7_20
[14] Favre, C., Völzer, H., Müller, P.: Diagnostic information for control-flow analysis of workflow graphs (a.k.a. Free-Choice Workflow Nets). In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 463–479. Springer, Berlin (2016). doi: 10.1007/978-3-662-49674-9_27 · doi:10.1007/978-3-662-49674-9_27
[15] Van Hee, K., Sidorova, N., Voorhoeve, M.: Generalised soundness of workflow nets is decidable. In: Cortadella, J., Reisig, W. (eds.) ICATPN 2004. LNCS, vol. 3099, pp. 197–215. Springer, Berlin (2004). doi: 10.1007/978-3-540-27793-4_12 · Zbl 1094.68070 · doi:10.1007/978-3-540-27793-4_12
[16] Hee, K., Oanea, O., Sidorova, N., Voorhoeve, M.: Verifying generalized soundness of workflow nets. In: Virbitskaite, I., Voronkov, A. (eds.) PSI 2006. LNCS, vol. 4378, pp. 235–247. Springer, Berlin (2007). doi: 10.1007/978-3-540-70881-0_21 · Zbl 1185.68452 · doi:10.1007/978-3-540-70881-0_21
[17] Ping, L., Hao, H., Jian, L.: On 1-soundness and soundness of workflow nets. In: Proceedings of the Third Workshop on Modelling of Objects, Components, and Agents Aarhus, Denmark, pp. 21–36 (2004)
[18] Verbeek, H.M.W., Basten, T., van der Aalst, W.M.: Diagnosing workflow processes using woflan. Comput. J. 44(4), 246–279 (2001) · Zbl 0993.68141 · doi:10.1093/comjnl/44.4.246
[19] Yamaguchi, M., Yamaguchi, S., Tanaka, M.: A model checking method of soundness for workflow nets. IEICE Trans. Fundam. Electron. Commun. Comput. Sci. 92(11), 2723–2731 (2009) · doi:10.1587/transfun.E92.A.2723
[20] Holzmann, G.J.: The SPIN Model Checker Primer and Reference Manual, vol. 1003. Addison-Wesley, Reading (2004)
[21] Barkaoui, K., Ben Ayed, R., Sbai, Z.: Workflow soundness verification based on structure theory of Petri nets. J. Comput. Inf. Sci. 5(1), 51–61 (2007)
[22] Desel, J., Esparza, J.: Free Choice Petri Nets, vol. 40. Cambridge University Press, New York (2005) · Zbl 0836.68074
[23] Lin, H., Zhao, Z., Li, H., Chen, Z.: A novel graph reduction algorithm to identify structural conflicts. In: Proceedings of the 35th Annual Hawaii International Conference on System Sciences HICSS 2002, 10 p. IEEE (2002) · doi:10.1109/HICSS.2002.994506
[24] Hichami, O.E., Al Achhab, M., Berrada, I., Oucheikh, R., El Mohajir, B.E.: An approach of optimisation and formal verification of workflow Petri nets. J. Theoret. Appl. Inf. Technol. 61(3), 486–495 (2014)
[25] Berthelot, G.: Transformations and decompositions of nets. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) ACPN 1986. LNCS, vol. 254, pp. 359–376. Springer, Berlin (1987). doi: 10.1007/978-3-540-47919-2_13 · Zbl 0634.68061 · doi:10.1007/978-3-540-47919-2_13
[26] Voorhoeve, M., Van der Aalst, W.: Ad-hoc workflow: problems and solutions. In: 1997 Proceedings of the Eighth International Workshop on Database and Expert Systems Applications, pp. 36–40. IEEE (1997) · doi:10.1109/DEXA.1997.617230
[27] Sadiq, W., Orlowska, M.E.: Analyzing process models using graph reduction techniques. Inf. Syst. 25(2), 117–134 (2000) · Zbl 02177947 · doi:10.1016/S0306-4379(00)00012-0
[28] Wynn, M.T., Verbeek, H., van der Aalst, W.M., ter Hofstede, A.H., Edmond, D.: Soundness-preserving reduction rules for reset workflow nets. Inf. Sci. 179(6), 769–790 (2009) · Zbl 1162.68488 · doi:10.1016/j.ins.2008.10.033
[29] Sloan, R.H., Buy, U.: Reduction rules for time petri nets. Acta Informatica 33(7), 687–706 (1996) · Zbl 0858.68060 · doi:10.1007/s002360050066
[30] Petri, C.A.: Kommunikation mit Automaten. Ph.D. thesis, Darmstadt University of Technology, Germany (1962)
[31] van der Aalst, W.M.: The application of Petri nets to workflow management. J. Circuits Syst. Comput. 8(1), 21–66 (1998) · doi:10.1142/S0218126698000043
[32] Weber, M., Kindler, E.: The petri net markup language. In: Ehrig, H., Reisig, W., Rozenberg, G., Weber, H. (eds.) Petri Net Technology for Communication-Based Systems. LNCS, vol. 2472, pp. 124–144. Springer, Berlin (2003). doi: 10.1007/978-3-540-40022-6_7 · Zbl 1283.68260 · doi:10.1007/978-3-540-40022-6_7
[33] Desel, J., Juhás, G., Lorenz, R., Neumair, C.: Modelling and validation with viptool. In: Aalst, W.M.P., Weske, M. (eds.) BPM 2003. LNCS, vol. 2678, pp. 380–389. Springer, Berlin (2003). doi: 10.1007/3-540-44895-0_26 · doi:10.1007/3-540-44895-0_26
[34] Freytag, T.: Woped-workflow petri net designer. University of Cooperative Education (2005)
[35] Van Hee, K., Oanea, O., Post, R., Somers, L., Van der Werf, J.M.: Yasper: a tool for workflow modeling and analysis. In: 2006 Sixth International Conference on Application of Concurrency to System Design ACSD 2006, pp. 279–282. IEEE (2006) · doi:10.1109/ACSD.2006.37
[36] Bonet, P., Lladó, C.M., Puijaner, R., Knottenbelt, W.J.: PIPE v2.5: a Petri net tool for performance modelling. In: Proceedings of the 23rd Latin American Conference on Informatics (CLEI 2007), San Jose, Costa Rica, October 2007
[37] Dumas, M., Hofstede, A.H.M.: UML activity diagrams as a workflow specification language. In: Gogolla, M., Kobryn, C. (eds.) UML 2001. LNCS, vol. 2185, pp. 76–90. Springer, Berlin (2001). doi: 10.1007/3-540-45441-1_7 · Zbl 1024.68701 · doi:10.1007/3-540-45441-1_7
[38] Fahland, D.: Translating UML2 activity diagrams to Petri nets (2008)
[39] Kiepuszewski, B., ter Hofstede, A.H.M., van der Aalst, W.M.: Fundamentals of control flow in workflows. Acta Informatica 39(3), 143–209 (2003) · Zbl 1060.68079 · doi:10.1007/s00236-002-0105-4
[40] Kordon, F., Garavel, H., Hillah, L.M., Hulin-Hubard, F., Chiardo, G., Hamez, A., Jezequel, L., Miner, A., Meijer, J., Paviot-Adet, E., Racordon, D., Rodriguez, C., Rohr, C., Srba, J., Thierry-Mieg, Y., Trinh, G., Wolf, K.: Models of the 2016 Edition of the Model Checking Contest, June 2016. http://mcc.lip6.fr/models.php
[41] Lohmann, N., Verbeek, E., Dijkman, R.: Petri net transformations for business processes–a survey. In: Jensen, K., Aalst, W.M.P. (eds.) Transactions on Petri Nets and Other Models of Concurrency II. LNCS, vol. 5460, pp. 46–63. Springer, Berlin (2009). doi: 10.1007/978-3-642-00899-3_3 · Zbl 05546906 · doi:10.1007/978-3-642-00899-3_3
[42] Verbeek, E., Van Der Aalst, W.M.P.: Woflan 2.0 A petri-net-based workflow diagnosis tool. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 475–484. Springer, Heidelberg (2000). doi: 10.1007/3-540-44988-4_28 · Zbl 0986.68781 · doi:10.1007/3-540-44988-4_28
[43] Bride, H., Kouchnarenko, O., Peureux, F.: Verifying modal workflow specifications using constraint solving. In: Albert, E., Sekerinski, E. (eds.) IFM 2014. LNCS, vol. 8739, pp. 171–186. Springer, Heidelberg (2014). doi: 10.1007/978-3-319-10181-1_11 · Zbl 06535515 · doi:10.1007/978-3-319-10181-1_11
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.