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

Julio Clempner

International Journal of Applied Mathematics and Computer Science (2014)

  • Volume: 24, Issue: 4, page 931-939
  • ISSN: 1641-876X

Abstract

top
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.

How to cite

top

Julio Clempner. "An analytical method for well-formed workflow/Petri net verification of classical soundness." International Journal of Applied Mathematics and Computer Science 24.4 (2014): 931-939. <http://eudml.org/doc/271874>.

@article{JulioClempner2014,
abstract = {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.},
author = {Julio Clempner},
journal = {International Journal of Applied Mathematics and Computer Science},
keywords = {Petri nets; decidability; workflow nets; Lyapunov stability; soundness; verification},
language = {eng},
number = {4},
pages = {931-939},
title = {An analytical method for well-formed workflow/Petri net verification of classical soundness},
url = {http://eudml.org/doc/271874},
volume = {24},
year = {2014},
}

TY - JOUR
AU - Julio Clempner
TI - An analytical method for well-formed workflow/Petri net verification of classical soundness
JO - International Journal of Applied Mathematics and Computer Science
PY - 2014
VL - 24
IS - 4
SP - 931
EP - 939
AB - 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.
LA - eng
KW - Petri nets; decidability; workflow nets; Lyapunov stability; soundness; verification
UR - http://eudml.org/doc/271874
ER -

References

top
  1. Barkaoui, K. and Ben Ayed, R. (2011). Uniform verification of workflow soundness, Transactions of the Institute of Measurement and Control 33(1): 133-148. 
  2. 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. 
  3. Basu, A. and Blanning, R.W. (2000). A formal approach to workflow analysis, Information Systems Research 11(1): 17-36. 
  4. Basu, A. and Blanning, R.W. (2002). Research commentary: Workflow management issues in e-business, Information Systems Research 13(1): 17-36. 
  5. Bi, H.H. and Zhao, J.L. (2004). Applying propositional logic to workflow verification, Information Systems Research 5(3-4): 293-318. 
  6. 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. Zbl0501.68027
  7. Clempner, J. (2005). Colored decision process Petri nets: Modeling, analysis and stability, International Journal of Applied Mathematics and Computer Science 15(3): 405-420. Zbl1169.93371
  8. Clempner, J. (2014). Verifying soundness of business processes: A decision process Petri nets approach, Expert Systems with Applications 41(11): 5030-5040. 
  9. Clempner, J. and Retchkiman, Z. (2005). Business process modeling using decision process Petri nets, WSEAS Transactions on Business and Economics 2(2): 36-44. Zbl1089.68070
  10. 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. Zbl0980.68816
  11. 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. 
  12. 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. 
  13. 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. Zbl1022.68656
  14. 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. 
  15. 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. 
  16. 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. 
  17. Lakshmikantham, V., Leela, S. and Martynyuk, A.A. (1990). Practical Stability of Nonlinear Systems, World Scientific, Singapore. Zbl0753.34037
  18. Lakshmikantham, V., Matrosov, V.M. and Sivasundaram, S. (1991). Vector Lyapunov Functions and Stability Analysis of Nonlinear Systems, Kluwer Academic Publishers, Dordrecht. Zbl0721.34054
  19. 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. 
  20. 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. 
  21. 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. Zbl1205.68266
  22. 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. Zbl1119.68305
  23. 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. 
  24. 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. 
  25. Murata, T. (1989). Petri nets: Properties, analysis and applications, Automatica 77(4): 541-580. 
  26. 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. Zbl0849.93051
  27. 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. 
  28. Sadiq, W. and Orlowska, M.E. (2000). Analyzing process models using graph reduction techniques, Information Systems 25(2): 117-134. 
  29. Salimifard, K. and Wright, M. (2001). Petri net-based modelling of workflow systems: An overview, European Journal of Operational Research 134(3): 664-676. Zbl0984.90005
  30. 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. 
  31. 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. 
  32. 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. 
  33. van der Aalst, W.M.P. (2011). Soundness of workflow nets: Classification, decidability, and analysis, Formal Aspects of Computing 23(3): 333-363. Zbl1225.68129
  34. 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. 
  35. 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. Zbl1128.68391
  36. 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. Zbl1094.68070
  37. 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. 
  38. 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. Zbl0993.68141
  39. 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. 
  40. Weske, M. (2007). Business Process Management: Concepts, Languages, Architectures, Springer-Verlag, Berlin. 
  41. 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. 
  42. 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. Zbl1128.68389
  43. 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. 
  44. zur Muehlen, M. (2004). Workflow-based Process Controlling: Foundation, Design and Application of Workflow-driven Process Information Systems, Logos, Berlin. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.