×

Connectivity of workflow nets: The foundations of stepwise verification. (English) Zbl 1234.68305

Summary: Behavioral models capture operational principles of real-world or designed systems. Formally, each behavioral model defines the state space of a system, i.e., its states and the principles of state transitions. Such a model is the basis for analysis of the system’s properties. In practice, state spaces of systems are immense, which results in huge computational complexity for their analysis. Behavioral models are typically described as executable graphs, whose execution semantics encodes a state space. The structure theory of behavioral models studies the relations between the structure of a model and the properties of its state space. In this article, we use the connectivity property of graphs to achieve an efficient and extensive discovery of the compositional structure of behavioral models; behavioral models get stepwise decomposed into components with clear structural characteristics and inter-component relations. At each decomposition step, the discovered compositional structure of a model is used for reasoning on properties of the whole state space of the system. The approach is exemplified by means of a concrete behavioral model and verification criterion. That is, we analyze workflow nets, a well-established tool for modeling behavior of distributed systems, with respect to the soundness property, a basic correctness property of workflow nets. Stepwise verification allows the detection of violations of the soundness property by inspecting small portions of a model, thereby considerably reducing the amount of work to be done to perform soundness checks. Besides formal results, we also report on findings from applying our approach to an industry model collection.

MSC:

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68R10 Graph theory (including graph drawing) in computer science
05C40 Connectivity
PDFBibTeX XMLCite
Full Text: DOI Link

References:

[1] Berthelot, G.: Checking properties of nets using transformation. In: ATPN. Volume 222 of Lecture Notes in Computer Science. Springer, Berlin, pp. 19–40 (1986) · Zbl 0606.68055
[2] Berthelot, G.: Transformations and decompositions of nets. In: Advances in Petri Nets. Volume 254 of Lecture Notes in Computer Science. Springer, Berlin, pp. 359–376 (1987) · Zbl 0634.68061
[3] Battista, G.D., Tamassia, R.: On-line graph algorithms with SPQR-trees. In: ICALP. Volume 443 of Lecture Notes in Computer Science. Springer, Berlin, pp. 598–611 (1990) · Zbl 0765.68024
[4] Desel J., Esparza J.: Free Choice Petri Nets. Cambridge University Press, Cambridge (1995) · Zbl 0836.68074
[5] Diestel R.: Graph Theory. Springer, Berlin (2005) · Zbl 1074.05001
[6] Eshuis R., Wieringa R.: Tool support for verifying UML activity diagrams. IEEE Trans. Softw. Eng. (TSE) 30(7), 437–447 (2004) · Zbl 05114059 · doi:10.1109/TSE.2004.33
[7] Esparza, J., Silva, M.: Circuits, handles, bridges and nets. In: ATPN. Volume 483 of Lecture Notes in Computer Science. Springer, Berlin, pp. 210–242 (1991)
[8] Fahland, D., Favre, C., Jobstmann, B., Koehler, J., Lohmann, N., Völzer H., Wolf K.: Instantaneous soundness checking of industrial business process models. In: BPM. Volume 5701 of Lecture Notes in Computer Science. Springer, Berlin, pp. 278–293 (2009)
[9] Gutwenger, C., Mutzel, P.: A linear time implementation of SPQR-trees. In: Graph Drawing. Volume 1984 of Lecture Notes in Computer Science. Springer, Berlin, pp. 77–90 (2001) · Zbl 1043.68621
[10] Hopcroft J., Tarjan R.E.: Dividing a graph into triconnected components. SIAM J. Comput. (SIAMCOMP) 2(3), 135–158 (1973) · Zbl 0281.05111 · doi:10.1137/0202012
[11] Hopcroft J., Tarjan R.E.: Algorithm 447: efficient algorithms for graph manipulation. Commun. ACM (CACM) 16(6), 372–378 (1973) · doi:10.1145/362248.362272
[12] Johnson, R.C.: Efficient Program Analysis Using Dependence Flow Graphs. PhD thesis, Cornell University, Ithaca, NY, USA (1995)
[13] Kemper, P.: Linear time algorithm to find a minimal deadlock in a strongly connected free-choice net. In: ATPN. Volume 691 of Lecture Notes in Computer Science. Springer, Berlin, pp. 319–338 (1993)
[14] Keller, G., Nüttgens, M., Scheer, A.W.: Semantische Prozeßmodellierung auf der Grundlage ’Ereignisgesteuerter Prozeßketten (EPK)’. Veröffentlichungen des Instituts für schaftsinformatik (IWi), Universität des Saarlandes (January 1992) In German
[15] Kiepuszewski B., ter Hofstede A.H.M., van der Aalst W.M.P.: Fundamentals of control flow in workflows. Acta Informatica 39(3), 143–209 (2003) · Zbl 1060.68079 · doi:10.1007/s00236-002-0105-4
[16] Kindler, E.: On the semantics of EPCs: A framework for resolving the vicious circle. In: BPM. Volume 3080 of Lecture Notes in Computer Science. Springer, Berlin, pp. 82–97 (2004)
[17] Lohmann, N.: A feature-complete Petri net semantics for WS-BPEL 2.0. In: WS-FM. Volume 4937 of Lecture Notes in Computer Science. Springer, Berlin, pp. 77–91 (2008)
[18] Lohmann N., Verbeek E., Dijkman R.M.: Petri net transformations for business processes–a survey. Trans. Petri Nets Other Models Concurr. (TOPNOC) 2, 46–63 (2009) · Zbl 05546906 · doi:10.1007/978-3-642-00899-3_3
[19] Menger K.: Zur allgemeinen Kurventheorie. Fund. Math. 10, 96–115 (1927) · JFM 53.0561.01
[20] Murata T.: Petri nets: properties, analysis and applications. Proc. IEEE (PIEEE) 77(4), 541–580 (1989) · doi:10.1109/5.24143
[21] Object Management Group: Unified Modeling Language: Superstructure (UML) version 2.1.1(February 2007)
[22] Object Management Group: Business Process Model and Notation (BPMN) version 2.0 beta 2 (June 2010)
[23] Polyvyanyy, A., Smirnov, S., Weske, M.: The triconnected abstraction of process models. In: BPM. Volume 5701 of Lecture Notes in Computer Science. Springer, Berlin, pp. 229–244 (2009)
[24] Polyvyanyy, A.: Structural abstraction of process specifications. In: ZEUS. Volume 563 of CEUR Workshop Proceedings. CEUR-WS.org, pp. 73–79 (2010)
[25] Polyvyanyy, A., Weidlich, M., Weske, M.: The biconnected verification of workflow nets. In: OTM Conferences (1). Volume 6426 of Lecture Notes in Computer Science. Springer, Berlin, pp. 410–418 (2010) · Zbl 1234.68305
[26] Polyvyanyy, A., Vanhatalo, J., Völzer, H.: Simplified computation and generalization of the refined process structure tree. In: WS-FM. Volume 6551 of Lecture Notes in Computer Science. Springer, Berlin, pp. 25–41 (2011)
[27] Reisig, W.: Petri Nets: An Introduction. Volume 4 of Monographs in Theoretical Computer Science. An EATCS Series. Springer, Berlin (1985) · Zbl 0555.68033
[28] Skiena S.S.: Implementing Discrete Mathematics: Combinatorics and Graph Theory with Mathematica. Addison-Wesley, Reading (1990) · Zbl 0786.05004
[29] Tarjan R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput. (SIAMCOMP) 1(2), 146–160 (1972) · Zbl 0251.05107 · doi:10.1137/0201010
[30] Valette R.: Analysis of petri nets by stepwise refinements. J. Comput. Syst. Sci. (JCSS) 18(1), 35–46 (1979) · Zbl 0401.68038 · doi:10.1016/0022-0000(79)90050-3
[31] Tarjan, R.E., Valdes, J.: Prime subprogram parsing of a program. In: POPL, pp. 95–105 (1980)
[32] van der Aalst, W.M.P.: Verification of workflow nets. In: ICATPN. Volume 1248 of Lecture Notes in Computer Science. Springer, Berlin, pp. 407–426 (1997)
[33] van der Aalst W.M.P.: The application of Petri nets to workflow management. J. Circuits Syst. Comput. (JCSC) 8(1), 21–66 (1998) · doi:10.1142/S0218126698000043
[34] van der Aalst, W.M.P.: Workflow verification: finding control-flow errors using Petri-net-based techniques. In: BPM. Volume 1806 of Lecture Notes in Computer Science. Springer, Berlin, pp 161–183 (2000)
[35] Vanhatalo, J., Völzer, H., Leymann, F.: Faster and more focused control-flow analysis for business process models through SESE decomposition. In: ICSOC. Volume 4749 of Lecture Notes in Computer Science. Springer, Berlin, pp. 43–55 (2007)
[36] Vanhatalo, J., Völzer, H., Koehler, J.: The refined process structure tree. In: BPM. Volume 5240 of Lecture Notes in Computer Science. Springer, Berlin, pp. 100–115 (2008)
[37] Vanhatalo J., Völzer H., Koehler J.: The refined process structure tree. Data Knowl. Eng. (DKE) 68(9), 793–818 (2009) · Zbl 05841529 · doi:10.1016/j.datak.2009.02.015
[38] Verbeek E., Basten T., van der Aalst W.M.P.: Diagnosing workflow processes using woflan. Comput. J. (CJ) 44(4), 246–279 (2001) · Zbl 0993.68141 · doi:10.1093/comjnl/44.4.246
[39] Verbeek E., Wynn M.T., van der Aalst W.M.P., ter Hofstede A.H.M.: Reduction rules for reset/inhibitor nets. J. Comput. Syst. Sci. (JCSS) 76(2), 125–143 (2010) · Zbl 1187.68330 · doi:10.1016/j.jcss.2009.06.003
[40] van der Aalst W.M.P., Basten T.: Inheritance of workflows: an approach to tackling problems related to change. Theor. Comput. Sci. (TCS) 270(1–2), 125–203 (2002) · Zbl 0984.68113 · doi:10.1016/S0304-3975(00)00321-2
[41] Weidlich, M., Polyvyanyy, A., Mendling J., Weske M.: Efficient computation of causal behavioural profiles using structural decomposition. In: Petri Nets. Volume 6128 of Lecture Notes in Computer Science. Springer, Berlin, pp. 63–83 (2010) · Zbl 1233.68174
[42] Weske M.: Business Process Management: Concepts Languages Architectures. Springer, Berlin (2007)
[43] Wolf, K.: Generating Petri net state spaces. In: ICATPN. Volume 4546 of Lecture Notes in Computer Science. Springer, Berlin, pp. 29–42 (2007)
[44] Wynn M.T., Verbeek E., van der Aalst W.M.P., ter Hofstede A.H.M., Edmond D.: Soundness-preserving reduction rules for reset workflow nets. Inf. Sci. (ISCI) 179(6), 769–790 (2009) · Zbl 1162.68488 · doi:10.1016/j.ins.2008.10.033
[45] Wynn M.T., Verbeek E., van der Aalst W.M.P., ter Hofstede A.H.M., Edmond D.: Reduction rules for YAWL workflows with cancellation regions and OR-joins. Inf. Softw. Technol. (INFSOF) 51(6), 1010–1020 (2009) · Zbl 05854350 · doi:10.1016/j.infsof.2008.12.002
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.