An analytical method for well-formed workflow/Petri net verification of classical soundness

Julio Clempner

International Journal of Applied Mathematics and Computer Science, Tome 24 (2014), p. 931-939 / Harvested from The Polish Digital Mathematics Library

Résumé

In this paper we consider workflow nets as dynamical systems governed by ordinary difference equations described by a particular class of Petri nets. Workflow nets are a formal model of business processes. Well-formed business processes correspond to sound workflow nets. Even if it seems necessary to require the soundness of workflow nets, there exist business processes with conditional behavior that will not necessarily satisfy the soundness property. In this sense, we propose an analytical method for showing that a workflow net satisfies the classical soundness property using a Petri net. To present our statement, we use Lyapunov stability theory to tackle the classical soundness verification problem for a class of dynamical systems described by Petri nets. This class of Petri nets allows a dynamical model representation that can be expressed in terms of difference equations. As a result, by applying Lyapunov theory, the classical soundness property for workflow nets is solved proving that the Petri net representation is stable. We show that a finite and non-blocking workflow net satisfies the sound property if and only if its corresponding PN is stable, i.e., given the incidence matrix A of the corresponding PN, there exists a Φ strictly positive m vector such that AΦ ≤ 0. The key contribution of the paper is the analytical method itself that satisfies part of the definition of the classical soundness requirements. The method is designed for practical applications, guarantees that anomalies can be detected without domain knowledge, and can be easily implemented into existing commercial systems that do not support the verification of workflows. The validity of the proposed method is successfully demonstrated by application examples.

Détail

Publié le : 2014-01-01

Zbl 1309.93099

EUDML-ID : urn:eudml:doc:271874

Bibliographie

[000] Barkaoui, K. and Ben Ayed, R. (2011). Uniform verification of workflow soundness, Transactions of the Institute of Measurement and Control 33(1): 133-148.

[001] Barkaoui, K. and Petrucci, L. (1998). Structural analysis of workflow nets with shared resources, Proceedings of Workflow Management: Net-based Concepts, Models, Techniques and Tools (WFM'98), Lisbon, Portugal, pp. 82-95.

[002] Basu, A. and Blanning, R.W. (2000). A formal approach to workflow analysis, Information Systems Research 11(1): 17-36.

[003] Basu, A. and Blanning, R.W. (2002). Research commentary: Workflow management issues in e-business, Information Systems Research 13(1): 17-36.

[004] Bi, H.H. and Zhao, J.L. (2004). Applying propositional logic to workflow verification, Information Systems Research 5(3-4): 293-318.

[005] Brams, G.W. (1983). Réseaux de Petri: Théorie et Pratique, Théorie et Analyse (Petri Nets: Theory and Practice), Vol. 1, Masson, Paris. | Zbl 0501.68027

[006] Clempner, J. (2005). Colored decision process Petri nets: Modeling, analysis and stability, International Journal of Applied Mathematics and Computer Science 15(3): 405-420. | Zbl 1169.93371

[007] Clempner, J. (2014). Verifying soundness of business processes: A decision process Petri nets approach, Expert Systems with Applications 41(11): 5030-5040.

[008] Clempner, J. and Retchkiman, Z. (2005). Business process modeling using decision process Petri nets, WSEAS Transactions on Business and Economics 2(2): 36-44. | Zbl 1089.68070

[009] Dehnert, J. and Rittgen, P. (2001). Relaxed soundness of business processes, in K.R. Dittrich, A. Geppert and M.C. Norrie (Eds.), Proceedings of the 13th International Conference on Advanced Information Systems Engineering (CAiSE'01), Lecture Notes in Computer Science, Vol. 2068, Springer-Verlag, Berlin, pp. 157-170. | Zbl 0980.68816

[010] Desel, J. and Erwin, T. (2000). Modeling, simulation and analysis of business processes, in W.M.P. van der Aalst, J. Desel and A. Oberweis (Eds.), Business Process Management: Models, Techniques and Empirical Studies, Lecture Notes in Computer Science, Vol. 1806, Springer-Verlag, London, pp. 129-141.

[011] Ellis, C.A. and Nutt, G.I. (1993). Modelling and enactment of workflow systems, in M. Ajmone Marsan (Ed.), 14th International Conference on Application and Theory of Petri Nets (ICATPN 1993), Lecture Notes in Computer Science, Vol. 691, Springer-Verlag, Berlin, pp. 1-16.

[012] Fu, X., Bultan, T. and Su, J. (2002). Formal verification of e-services and workflows, in C. Bussler, R. Hull, S. McIlraith, M. Orlowska, B. Pernici, and J. Yang (Eds.), Web Services, E-Business, and the Semantic Web, CAiSE 2002 International Workshop (WES 2002), Lecture Notes in Computer Science, Vol. 2512, Springer-Verlag, Berlin, pp. 188-202. | Zbl 1022.68656

[013] Fu, X., Bultan, T. and Su, J. (2004). Analysis of interacting BPEL web services, 13th International World Wide Web Conference, New York, NY, USA, pp. 621-630.

[014] Karamanolis, C., Giannakopoulou, D., Magee, J. and Wheater, S.M. (2000). Model checking of workflow schemas, Proceedings of the 4th International Enterprise Distributed Object Computing Conference (EDOC'00), Los Alamitos, CA, USA, pp. 170-181.

[015] Kindler, E., Martens, A. and Reisig, W. (2000). Inter-operability of workflow applications: Local criteria for global soundness, in W.M.P. van der Aalst, J. Desel and A. Oberweis (Eds.), Business Process Management: Models, Techniques, and Empirical Studies, Lecture Notes in Computer Science, Vol. 1806, Springer-Verlag, Berlin, pp. 235-253.

[016] Lakshmikantham, V., Leela, S. and Martynyuk, A.A. (1990). Practical Stability of Nonlinear Systems, World Scientific, Singapore. | Zbl 0753.34037

[017] Lakshmikantham, V., Matrosov, V.M. and Sivasundaram, S. (1991). Vector Lyapunov Functions and Stability Analysis of Nonlinear Systems, Kluwer Academic Publishers, Dordrecht. | Zbl 0721.34054

[018] Lin, H., Zhao, Z., Li, H. and Chen, Z. (2002). A novel graph reduction algorithm to identify structural conflicts, Proceedings of the 34th Annual Hawaii International Conference on System Science (HICSS-35), Maui, HI, USA, pp. 1-10.

[019] Lohmann, N., Massuthe, P., Stahl, C. and Weinberg, D. (2006). Analyzing interacting BPEL processes, in S. Dustdar, J.L. Fiadeiro and A. Sheth (Eds.), International Conference on Business Process Management (BPM 2006), Lecture Notes in Computer Science, Vol. 4102, Springer-Verlag, Berlin, pp. 17-32.

[020] Mann, Z.A. (2010). Numbering action vertices in workflow graphs, International Journal of Applied Mathematics and Computer Science 20(3): 591-600, DOI: 10.2478/v10006-010-0044-0. | Zbl 1205.68266

[021] Martens, A. (2005a). Analyzing web service based business processes, in M. Cerioli (Ed.), Proceedings of the 8th International Conference on Fundamental Approaches to Software Engineering (FASE 2005), Lecture Notes in Computer Science, Vol. 3442, Springer-Verlag, Berlin, pp. 19-33. | Zbl 1119.68305

[022] Martens, A. (2005b). Consistency between executable and abstract processes, Proceedings of the International IEEE Conference on e-Technology, e-Commerce, and e-Services (EEE'05), Kitakyushu, Japan, pp. 60-67.

[023] Mendling, J., Neumann, G. and van der Aalst, W.M.P. (2007). Understanding the occurrence of errors in process models based on metrics, in M. Cerioli (Ed.), Proceedings of the OTM Conference on Cooperative information Systems (CoopIS 2007), Lecture Notes in Computer Science, Vol. 4803, Springer-Verlag, Berlin, pp. 113-130.

[024] Murata, T. (1989). Petri nets: Properties, analysis and applications, Automatica 77(4): 541-580.

[025] Passino, K.M., Burguess, K.L. and Michel, A.N. (1995). Lagrange stability and boundedness of discrete event systems, Theory and Applications 5: 383-403. | Zbl 0849.93051

[026] Sadiq, W. and Orlowska, M.E. (1997). On correctness issues in conceptual modeling of workflows, Proceedings of the 5th European Conference on Information Systems (ECIS '97), Cork, Ireland, pp. 19-21.

[027] Sadiq, W. and Orlowska, M.E. (2000). Analyzing process models using graph reduction techniques, Information Systems 25(2): 117-134.

[028] Salimifard, K. and Wright, M. (2001). Petri net-based modelling of workflow systems: An overview, European Journal of Operational Research 134(3): 664-676. | Zbl 0984.90005

[029] van der Aalst, W.M.P. (1997). Verification of workflow nets, in P. Azéma and G. Balbo (Eds.), Application and Theory of Petri Nets 1997, Springer-Verlag, Berlin, pp. 407-426.

[030] van der Aalst, W.M.P. (1998). The application of Petri nets to workflow management, The Journal of Circuits, Systems and Computers 8(1): 21-66.

[031] van der Aalst, W.M.P. (2007). Workflow verification: Finding control-flow errors using Petri-net-based techniques, in W.M.P. van der Aalst, J. Desel and A. Oberweis (Eds.), Business Process Management: Models, Techniques, and Empirical Studies, Springer-Verlag, Berlin, pp. 161-183.

[032] van der Aalst, W.M.P. (2011). Soundness of workflow nets: Classification, decidability, and analysis, Formal Aspects of Computing 23(3): 333-363. | Zbl 1225.68129

[033] van Dongen, B.F., van der Aalst, W.M.P. and Verbeek, H.M.W. (2005). Verification of EPCs: Using reduction rules and Petri nets, in O. Pastor and J. Falco e Cunha (Eds.), Proceedings of the 17th Conference on Advanced Information Systems Engineering (CAiSE'05), Lecture Notes in Computer Science, Vol. 3520, Springer-Verlag, Berlin, pp. 372-386.

[034] van Hee, K.M., Serebrenik, A., Sidorova N. and Voorhoeve, M. (2005). Soundness of resource-constrained workflow nets, in G. Ciardo and P. Darondeau (Eds.), Applications and Theory of Petri Nets 2005, Lecture Notes in Computer Science, Vol. 3536, Springer-Verlag, Berlin, pp. 250-267. | Zbl 1128.68391

[035] van Hee, K.M., Sidorova, N. and Voorhoeve, M. (2004). Generalised soundness of workflow nets is decidable, in J. Cortadella and W. Reisig (Eds.), Application and Theory of Petri Nets 2004, Lecture Notes in Computer Science, Vol. 3099, Springer-Verlag, Berlin, pp. 197-215. | Zbl 1094.68070

[036] Vanhatalo, J., Volzer, H. and Leymann, F. (2007). Faster and more focused control-flow analysis for business process models through SESE decomposition, in B. Kramer, K. Lin and P. Narasimhan (Eds.), Proceedings of Service-Oriented Computing (ICSOC 2007), Lecture Notes in Computer Science, Vol. 4749, Springer-Verlag, Berlin, pp. 43-55.

[037] Verbeek, H.M.W., Basten, T. and van der Aalst, W.M.P. (2001). Diagnosing workflow processes using Woflan, The Computer Journal 44(4): 246-279. | Zbl 0993.68141

[038] Verbeek, H.M.W., van der Aalst W.M.P. and ter Hofstede, A.H.M. (2001). Verifying workflows with cancellation regions and or-joins: An approach based on relaxed soundness and invariants, The Computer Journal 50(3): 294-314.

[039] Weske, M. (2007). Business Process Management: Concepts, Languages, Architectures, Springer-Verlag, Berlin.

[040] Wombacher, A. (2006). Decentralized consistency checking in cross-organizational workflows, Proceedings of the International Conference on e-Technology, e-Commerce and e-Service (CEC/EEE 2006), Washington, DC, USA, pp. 39-46.

[041] Wynn, M.T., Edmond, D., van der Aalst W.M.P. and ter Hofstede, A.H.M. (2005). Achieving a general, formal and decidable approach to the or-join in workflow using reset nets, in G. Ciardo and P. Darondeau (Eds.), Applications and Theory of Petri Nets 2005, Lecture Notes in Computer Science, Vol. 3536, Springer-Verlag, Berlin, pp. 423-443. | Zbl 1128.68389

[042] Wynn, M.T., van der Aalst, W.M.P., ter Hofstede, A.H.M. and Edmond, D. (2006). Verifying workflows with cancellation regions and or-joins: An approach based on reset nets and reachability analysis, in S. Dustdar, J.L. Fiadeiro and A. Sheth (Eds.), International Conference on Business Process Management (BPM 2006), Lecture Notes in Computer Science, Vol. 4102, Springer-Verlag, Berlin, pp. 389-394.

[043] zur Muehlen, M. (2004). Workflow-based Process Controlling: Foundation, Design and Application of Workflow-driven Process Information Systems, Logos, Berlin.