Soundness of workflow nets: classification, decidability, and analysis

Formal Aspects of Computing - Tập 23 - Trang 333-363 - 2010
W. M. P. van der Aalst1,2, K. M. van Hee1, A. H. M. ter Hofstede1,2, N. Sidorova1, H. M. W. Verbeek1, M. Voorhoeve1, M. T. Wynn2
1Eindhoven University of Technology, Eindhoven, The Netherlands
2Queensland University of Technology, Brisbane, Australia

Tóm tắt

Workflow nets, a particular class of Petri nets, have become one of the standard ways to model and analyze workflows. Typically, they are used as an abstraction of the workflow that is used to check the so-called soundness property. This property guarantees the absence of livelocks, deadlocks, and other anomalies that can be detected without domain knowledge. Several authors have proposed alternative notions of soundness and have suggested to use more expressive languages, e.g., models with cancellations or priorities. This paper provides an overview of the different notions of soundness and investigates these in the presence of different extensions of workflow nets. We will show that the eight soundness notions described in the literature are decidable for workflow nets. However, most extensions will make all of these notions undecidable. These new results show the theoretical limits of workflow verification. Moreover, we discuss some of the analysis approaches described in the literature.

Tài liệu tham khảo

van der Aalst WMP (1997) Verification of workflow nets. In: Azéma P, Balbo G (eds) Application and theory of Petri nets 1997. Lecture notes in computer science, vol 1248. Springer-Verlag, Berlin, pp 407–426 van der Aalst WMP (1998) The application of Petri nets to workflow management. J Circ Syst Comput 8(1): 21–66 van der Aalst WMP (2000) Workflow verification: finding control-flow errors using Petri-net-based techniques. In: Aalst WMP, Desel J, Oberweis A (eds) Business process management: models, techniques, and empirical studies. Lecture notes in computer science, vol 1806. Springer-Verlag, Berlin, pp 161–183 van der Aalst WMP, van Hee KM (2004) Workflow management: models, methods, and systems. MIT press, Cambridge van der Aalst WMP, ter Hofstede AHM (2005) YAWL: yet another workflow language. Inf Syst 30(4): 245–275 van der Aalst WMP, van Hee KM, ter Hofstede AHM, Sidorova N, Verbeek HMW, Voorhoeve M, Wynn MT (2008) Soundness of workflow nets: classification, decidability, and analysis. Computer Science report no. 08-13. Technische Universiteit Eindhoven, The Netherlands van der Aalst WMP, van Hee KM, ter Hofstede AHM, Sidorova N, Verbeek HMW, Voorhoeve M, Wynn MT (2009) Soundness of workflow nets with reset arcs. In: Jensen K, Billington J, Koutny M (eds) Transactions on Petri nets and other models of Concurrency III. Lecture notes in computer science, vol 5800. Springer-Verlag, Berlin, pp 50–70 van der Aalst WMP, ter Hofstede AHM, Kiepuszewski B, Barros AP (2003) Workflow patterns. Distrib Parallel Databases 14(1): 5–51 van der Aalst WMP, Hirnschall A, Verbeek HMW (2002) An alternative way to analyze workflow graphs. In: Banks-Pidduck A, Mylopoulos J, Woo CC, Ozsu MT (eds) Proceedings of the 14th international conference on advanced information systems engineering (CAiSE’02). Lecture notes in computer science, vol 2348. Springer-Verlag, Berlin, pp 535–552 van der Aalst WMP, Lohmann N, Massuthe P, Stahl C, Wolf K (2008) From public views to private views: correctness-by-design for services. In: Dumas M, Heckel H (eds) Proceedings of the 4th international workshop on Web services and formal methods (WS-FM 2007). Lecture notes in computer science, vol 4937. Springer-Verlag, Berlin, pp 139–153 van der Aalst WMP, Mooij AJ, Stahl C, Wolf K (2009) Service interaction: patterns, formalization, and analysis. In: Bernardo M, Padovani L, Zavattaro G (eds) Formal methods for Web services. Lecture notes in computer science, vol 5569. Springer-Verlag, Berlin, pp 42–88 Basu A, Blanning RW (2000) A formal approach to workflow analysis. Inf Syst Res 11(1): 17–36 Berthelot G (1987) Transformations and decompositions of nets. In: Brauer W, Reisig W, Rozenberg G (eds) Advances in Petri nets 1986. Part I: Petri nets, central models and their properties. Lecture notes in computer science, vol 254. Springer-Verlag, Berlin, pp 360–376 Basu A, Kumar A (2002) Research commentary: workflow management issues in e-business. Inf Syst Res 13(1): 1–14 Barkaoui K, Petrucci L (1998) Structural analysis of workflow nets with shared resources. In: van der Aalst WMP, De Michelis G, Ellis CA (eds) Proceedings of workflow management: net-based concepts, models, techniques and tools (WFM’98), vol 98/7 of Computing science reports, Lisbon, Portugal. Eindhoven University of Technology, Eindhoven, pp 82–95 Bi HH, Zhao JL (2004) Applying propositional logic to workflow verification. Inf Technol Manag 5(3–4): 293–318 Chrzastowski-Wachtel P (1999) Testing undecidability of the reachability in Petri nets with the help of 10th Hilbert problem. In: Donatelli S, Kleijn J (eds) Application and theory of Petri nets. Lecture notes in computer science, vol 1639. Springer-Verlag, Berlin, pp 268–281 Dehnert J, van der Aalst WMP (2004) Bridging the gap between business models and workflow specifications. Int J Coop Inf Syst 13(3): 289–332 Dwyer MB, Avrunin GS, Corbett JC (1999) Patterns in property specifications for finite-state verification. In: ICSE ’99: proceedings of the 21st international conference on software engineering, Los Alamitos, CA, USA. IEEE Computer Society Press, pp 411–420 Dumas M, van der Aalst WMP, ter Hofstede AHM (2005) Process-aware information systems: bridging people and software through process technology. Wiley, Hoboken, New Jersey van Dongen BF, van der Aalst WMP, Verbeek HMW (2005) Verification of EPCs: using reduction rules and Petri nets. In: Pastor O, Falcão e Cunha J (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 Desel J, Esparza J (1995) Free choice Petri nets. In: Cambridge tracts in theoretical computer science, vol 40. Cambridge University Press, Cambridge Dufourd C, Finkel A, Schnoebelen Ph (1998) Reset nets between decidability and undecidability. In: Larsen K, Skyum S, Winskel G (eds) Proceedings of the 25th international colloquium on automata, languages and programming. Lecture notes in computer science, vol 1443. Springer-Verlag, Berlin, pp 103–115 Dufourd C, Jančar P, Schnoebelen Ph (1999) Boundedness of reset P/T nets. In: Wiedermann J, Emde Boas P, Nielsen M (eds) Lectures on concurrency and Petri nets Lecture notes. in computer science, vol 1644. Springer-Verlag, Berlin, pp 301–310 Dehnert J, Rittgen P (2001) Relaxed soundness of business processes. In: Dittrich KR, Geppert A, Norrie MC (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 Esparza J, Nielsen M (1994) Decidability issues for Petri nets: a survey. J Inf Process Cybern 30: 143–160 Esparza J (1998) Decidability and complexity of Petri net problems: an introduction. In: Reisig W, Rozenberg G (eds) Lectures on Petri nets I: basic models. Lecture notes in computer science, vol 1491. Springer-Verlag, Berlin, pp 374–428 Esparza J (1998) Reachability in live and safe free-choice Petri nets is NP-complete. Theor Comput Sci 198(1–2): 211–224 Fu X, Bultan T, Su J (2002) Formal verification of e-Services and workflows. In: Bussler C, Hull R, McIlraith S, Orlowska M, Pernici B, Yang J (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 Fu X, Bultan T, Su J (2004) Analysis of interacting BPEL Web services. In: International World Wide Web conference: proceedings of the 13th international conference on World Wide Web, New York. ACM Press, pp 621–630 Fahland D, Favre C, Jobstmann B, Koehler J, Lohmann N, Voelzer H, Wolf K (2009) Instantaneous soundness checking of industrial business process models. In: Dayal U, Eder J, Koehler J, Reijers H (eds) Business process management (BPM 2009). Lecture notes in computer science, vol 5701. Springer-Verlag, Berlin, pp 278–293 Finkel A, Schnoebelen Ph (2001) Well-structured transition systems everywhere!. Theor Comput Sci 256(1–2): 63–92 Georgakopoulos D, Hornick M, Sheth A (1995) An overview of workflow management: from process modeling to workflow automation infrastructure. Distrib Parallel Databases 3(2): 119–153 van Glabbeek RJ, Weijland WP (1996) Branching time and abstraction in bisimulation semantics. J ACM 43(3): 555–600 Hinz S, Schmidt K, Stahl C (2005) Transforming BPEL to Petri nets. In: Aalst WMP, Benatallah B, Casati F, Curbera F (eds) International conference on business process management (BPM 2005). Lecture notes in computer science, vol 3649. Springer-Verlag, Berlin, pp 220–235 van Hee KM, Serebrenik A, Sidorova N, Voorhoeve M (2005) Soundness of resource-constrained workflow nets. In: Ciardo G, Darondeau P (eds) Applications and theory of Petri nets 2005. Lecture notes in computer science, vol 3536. Springer-Verlag, Berlin, pp 250–267 van Hee KM, Sidorova N, Voorhoeve M (2003) Soundness and separability of workflow nets in the stepwise refinement approach. In: Aalst WMP, Best E (eds) Application and theory of Petri nets 2003. Lecture notes in computer science, vol 2679. Springer-Verlag, Berlin, pp 335–354 van Hee KM, Sidorova N, Voorhoeve M (2004) Generalised soundness of workflow nets is decidable. In: Cortadella J, Reisig W (eds) Application and theory of Petri nets 2004. Lecture notes in computer science, vol 3099. Springer-Verlag, Berlin, pp 197–215 Jablonski S, Bussler C (1996) Workflow management: modeling concepts, architecture, and implementation. International Thomson Computer Press, London Jensen K (1997) Coloured Petri nets. Basic concepts, analysis methods and practical use, vol 1. EATCS monographs on theoretical computer science. Springer-Verlag, Berlin Juhas G, Kazlov I, Juhasova A (2010) Instance deadlock: a mystery behind frozen programs. In: Lilius J, Penczek W (eds) Applications and theory of Petri nets 2010. Lecture notes in computer science, vol 6128. Springer-Verlag, Berlin, pp 1–17 Kindler E, van der Aalst WMP (1999) Liveness, fairness, and recurrence. Inf Process Lett 70(6): 269–274 Karamanolis C, Giannakopoulou D, Magee J, Wheater SM (2000) Model checking of workflow schemas. In: Proceedings of the fourth international enterprise distributed object computing conference (EDOC’00), Los Alamitos, CA, USA, 2000. IEEE Computer Society, pp 170–181 Kindler E (2006) On the semantics of EPCs: a framework for resolving the vicious circle. Data Knowl Eng 56(1): 23–40 Kindler E, Martens A, Reisig W (2000) Inter-operability of workflow applications: local criteria for global soundness. In: Aalst WMP, Desel J, Oberweis A (eds) Business process management: models, techniques, and empirical studies. Lecture notes in computer science, vol 1806. Springer-Verlag, Berlin, pp 235–253 Keller G, Nüttgens M, Scheer AW (1992) Semantische Processmodellierung auf der Grundlage Ereignisgesteuerter Processketten (EPK). Veröffentlichungen des Instituts für Wirtschaftsinformatik, Heft 89 (in German), University of Saarland, Saarbrücken Lohmann N, Massuthe P, Stahl C, Weinberg D (2006) Analyzing interacting BPEL processes. In: Dustdar S, Fiadeiro JL, Sheth A (eds) International conference on business process management (BPM 2006). Lecture notes in computer science, vol 4102. Springer-Verlag, Berlin, pp 17–32 Leymann F, Roller D (1999) Production workflow: concepts and techniques. Prentice-Hall PTR, Upper Saddle River, New Jersey Lohmann N, Weinberg D (2010) Wendy: a tool to synthesize partners for services. In: Lilius J, Penczek W (eds) Applications and theory of Petri nets 2010. Lecture notes in computer science, vol 6128. Springer-Verlag, Berlin, pp 279–307 Lin H, Zhao Z, Li H, Chen Z (2002) A novel graph reduction algorithm to identify structural conflicts. In: Proceedings of the thirty-fourth annual Hawaii international conference on system science (HICSS-35). IEEE Computer Society Press Martens A (2003) On Compatibility of Web services. Petri Net Newsl 65: 12–20 Martens A (2005) Analyzing Web service based business processes. In: Cerioli M (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 Martens A (2005) Consistency between executable and abstract processes. In: Proceedings of international IEEE conference on e-Technology, e-Commerce, and e-Services (EEE’05). IEEE Computer Society Press, pp 60–67 Mendling J, Moser M, Neumann G, Verbeek HMW, van Dongen BF, van der Aalst WMP (2006) Faulty EPCs in the SAP reference model. In: Dustdar S, Fiadeiro JL, Sheth A (eds) International conference on business process management (BPM 2006). Lecture notes in computer science, vol 4102. Springer-Verlag, Berlin, pp 451–457 Mendling J, Neumann G, van der Aalst WMP (2007) Understanding the occurrence of errors in process models based on metrics. In: Curbera F, Leymann F, Weske M (eds) Proceedings of the OTM conference on cooperative information systems (CoopIS 2007). Lecture notes in computer science, vol 4803. Springer-Verlag, Berlin, pp 113–130 Massuthe P, Reisig W, Schmidt K (2005) An operating guideline approach to the SOA. In: Proceedings of the 2nd South-East European workshop on formal methods 2005 (SEEFM05), Ohrid, Republic of Macedonia Massuthe P, Reisig W, Schmidt K (2005) An operating guideline approach to the SOA. Ann Math Comput Teleinformatics 1(3): 35–43 zur Muehlen M (2004) Workflow-based process controlling: foundation, design and application of workflow-driven process information systems. Logos, Berlin Murata T (1989) Petri nets: properties, analysis and applications. Proc IEEE 77(4): 541–580 Mendling J, Verbeek HMW, van Dongen BF, van der Aalst WMP, Neumann G (2008) Detection and prediction of errors in EPCs of the SAP reference model. Data Knowl Eng 64(1): 312–329 Ouyang C, Dumas M, van der Aalst WMP, ter Hofstede AHM, Mendling J (2009) From business process models to process-oriented software systems. ACM Trans Softw Eng Methodol 19(1): 1–37 Puhlmann F, Weske M (2006) Interaction soundness for service orchestrations. In: Dan A, Lamersdorf W (eds) Proceedings of service-oriented computing (ICSOC 2006). Lecture notes in computer science, vol 4294. Springer-Verlag, Berlin, pp 302–313 Puhlmann F, Weske M (2006) Investigations on soundness regarding lazy activities. In: Dustdar S, Fiadeiro JL, Sheth A (eds) International conference on business process management (BPM 2006). Lecture notes in computer science, vol 4102. Springer-Verlag, Berlin, pp 145–160 Puhlmann F, Weske M (2009) A look around the corner: the pi-calculus. In: Jensen K, Aalst WMP (eds) Transactions on Petri nets and other models of concurrency II. Lecture notes in computer science, vol 5460. Springer-Verlag, Berlin, pp 64–78 Rozinat A, van der Aalst WMP (2008) Conformance checking of processes based on monitoring real behavior. Inf Syst 33(1): 64–95 Sadiq W, Orlowska ME (1997) On correctness issues in conceptual modeling of workflows. In: Proceedings of the 5th European conference on information systems (ECIS ’97), Cork, Ireland, pp 19–21 Sadiq W, Orlowska ME (2000) Analyzing process models using graph reduction techniques. Inf Syst 25(2): 117–134 Salimifard K, Wright M (2001) Petri net-based modelling of workflow systems: an overview. Eur J Oper Res 134(3): 664–676 Trcka N, van der Aalst WMP, Sidorova N (2009) Data-flow anti-patterns: discovering data-flow errors in workflows. In: Eck P, Gordijn J, Wieringa R (eds) Advanced information systems engineering, proceedings of the 21st international conference on advanced information systems engineering (CAiSE’09). Lecture notes in computer science, vol 5565. Springer-Verlag, Berlin, pp 425–439 van der Toorn R (2004) Component-based software design with Petri nets: an approach based on inheritance of behavior. PhD thesis, Eindhoven University of Technology, Eindhoven, The Netherlands Verbeek HMW, van der Aalst WMP (2005) Analyzing BPEL processes using Petri nets. In: Marinescu D (ed) Proceedings of the second international workshop on applications of Petri nets to coordination, workflow and business process management. Florida International University, Miami, Florida, pp 59–78 Verbeek HMW, van der Aalst WMP, ter Hofstede AHM (2007) Verifying workflows with cancellation regions and OR-joins: an approach based on relaxed soundness and invariants. Comput J 50(3): 294–314 Verbeek HMW, Basten T, van der Aalst WMP (2001) Diagnosing workflow processes using Woflan. Comput J 44(4): 246–279 Vanhatalo J, Völzer H, Leymann F (2007) Faster and more focused control-flow analysis for business process models through SESE decomposition. In: Krämer B, Lin K, Narasimhan P (eds) Proceedings of service-oriented computing (ICSOC 2007). Lecture notes in computer science, vol 4749. Springer-Verlag, Berlin, pp 43–55 Verbeek HMW, Wynn MT, van der Aalst WMP, ter Hofstede AHM (2010) Reduction rules for reset/inhibitor nets. J Comput Syst Sci 76(2): 125–143 Wynn MT, van der Aalst WMP, ter Hofstede AHM, Edmond D (2006) Verifying workflows with cancellation regions and OR-joins: an approach based on reset nets and reachability analysis. In: Dustdar S, Fiadeiro JL, Sheth A (eds) International conference on business process management (BPM 2006). Lecture notes in computer science, vol 4102. Springer-Verlag, Berlin, pp 389–394 Wynn MT, Edmond D, van der Aalst WMP, ter Hofstede AHM (2005) Achieving a general, formal and decidable approach to the OR-join in workflow using reset nets. In: Ciardo G, Darondeau P (eds) Applications and theory of Petri nets 2005. Lecture notes in computer science, vol 3536. Springer-Verlag, Berlin, pp 423–443 Weske M (2007) Business process management: concepts, languages, architectures. Springer-Verlag, Berlin Wong PYH, Gibbons J (2007) A process-algebraic approach to workflow specification and refinement. In: Lumpe M, Vanderperren W (eds) Software composition. Lecture notes in computer science, vol 4829. Springer-Verlag, Berlin, pp 51–65 Wong PYH, Gibbons J (2008) A process semantics for BPMN. In: Liu S, Maibaum T, Arki K (eds) International conference on formal engineering methods (ICFEM 2008). Lecture notes in computer science, vol 5256. Springer-Verlag, Berlin, pp 27–31 Wong PYH, Gibbons J (2009) Property specifications for workflow modelling. In: Proceedings of 7th international conference on integrated formal methods. Lecture notes in computer science, vol 5423. Springer-Verlag, Berlin White SA et al (2009) Business process modeling notation specification (Version 1.2, OMG Final Adopted Specification) Wolf K (2009) Does my service have partners?. In: Jensen K, Aalst WMP (eds) Transactions on Petri nets and other models of concurrency II. Lecture notes in computer science, vol 5460. Springer-Verlag, Berlin, pp 152–171 Wombacher A (2006) Decentralized consistency checking in cross-organizational workflows. In: Proceedings of international conference on e-Technology, e-Commerce and e-Service (CEC/EEE 2006). IEEE Computer Society, pp 39–46 Wynn MT, Verbeek HMW, van der Aalst WMP, ter Hofstede AHM, Edmond D (2009) Soundness-preserving reduction rules for reset workflow nets. Inf Sci 179(6): 769–790