Verification of workflow nets with transition conditions

Zhao-xia WANG; Jian-min WANG; Xiao-chen ZHU; Li-jie WEN

doi:10.1631/jzus.C1100364

Your Location：

Home >

Browse articles >

Verification of workflow nets with transition conditions

Computer & Automation | Updated：2022-12-09

- Verification of workflow nets with transition conditions
- Verification of workflow nets with transition conditions
- Frontiers of Information Technology & Electronic Engineering Vol. 13, Issue 7, Pages: 483-509(2012)
- Affiliations：
  
  1.School of Software, Tsinghua University, Beijing 100084, China
  2.Department of Computer Science and Technology, Tsinghua University, Beijing 100084, China
  3.MOE Key Laboratory for Information System Security, Tsinghua University, Beijing 100084, China
  4.National Laboratory for Information Science and Technology, Tsinghua University, Beijing 100084, China
  5.Department of Logistical Information & Engineering, Logistical Engineering University, Chongqing 400016, China
- Author bio：
  
  [ "Zhao-xia WANG, E-mail: wang-cx06@mails.thu.edu.cn" ]
  Jian-min WANG, E-mail: jimwang@thu.edu.cn
- Funds：
- DOI：10.1631/jzus.C1100364
  CLC： TP311
- Received：08 December 2011，
  
  Revised：2012-;5-31，
  
  Published：2012-07
- Accepted：
Scan QR Code
Zhao-xia WANG, Jian-min WANG, Xiao-chen ZHU, et al. Verification of workflow nets with transition conditions[J]. Frontiers of Information Technology & Electronic Engineering, 2012, 13(7): 483-509.
DOI：

Zhao-xia WANG, Jian-min WANG, Xiao-chen ZHU, et al. Verification of workflow nets with transition conditions[J]. Frontiers of Information Technology & Electronic Engineering, 2012, 13(7): 483-509. DOI： 10.1631/jzus.C1100364.

摘要

Abstract

Workflow management is concerned with automated support for business processes. Workflow management systems are driven by process models specifying the tasks that need to be executed

the order in which they can be executed

which resources are authorised to perform which tasks

and data that is required for

and produced by

these tasks. As workflow instances may run over a sustained period of time

it is important that workflow specifications be checked before they are deployed. Workflow verification is usually concerned with control-flow dependencies only; however

transition conditions based on data may further restrict possible choices between tasks. In this paper we extend workflow nets where transitions have concrete conditions associated with them

called WTC-nets. We then demonstrate that we can determine which execution paths of a WTC-net that are possible according to the control-flow dependencies

are actually possible when considering the conditions based on data. Thus

we are able to more accurately determine at design time whether a workflow net with transition conditions is sound.

关键词

Keywords

references

L.A. Clarke . . A system to generate test data and symbolically execute programs . . IEEE Trans. Software Eng. , , 1976 . . 2 ( ( 3 ): ): 215 - - 222 . . DOI: 10.1109/TSE.1976.233817 http://doi.org/10.1109/TSE.1976.233817 . .

T. Curran , , , G. Keller . . SAP R/3 Business Blueprint: Understanding the Business Process Reference Model . . Prentice Hall PTR, Upper Saddle River, NJ, USA , , 1998 . . .

R. Cytron , , , J. Ferrante , , , B.K. Rosen , , , M.N. Wegman , , , F.K. Zadeck . . Efficiently computing static single assignment form and the control dependence graph . . ACM Trans. Program. Lang. Syst. , , 1991 . . 13 ( ( 4 ): ): 451 - - 490 . . DOI: 10.1145/115372.115320 http://doi.org/10.1145/115372.115320 . .

J. Dehnert , , , W.M.P. van der Aalst . . Bridging the gap between business models and workflow specifications . . Int. J. Cooper. Inf. Syst. , , 2004 . . 13 ( ( 3 ): ): 289 - - 332 . . DOI: 10.1142/S0218843004000973 http://doi.org/10.1142/S0218843004000973 . .

B. Dutertre , , , L.M. de Moura . . A Fast Linear-Arithmetic Solver for DPLL(T) . . 18th Int. Conf. on Computer Aided Verification , , 2006a . . p.81 - - 94 . . DOI: 10.1007/11817963_11 http://doi.org/10.1007/11817963_11 . .

B. Dutertre , , , L. de Moura . . The Yices SMT Solver . . Available from , , http://yices.csl.sri.com/tool-paper.pdf http://yices.csl.sri.com/tool-paper.pdf , , 2006b . . .

S. Fan , , , W. Dou , , , J. Chen . . Dual Workflow Nets: Mixed Control/Data-Flow Representation for Workflow Modeling and Verification . . Advances in Web and Network Technologies and Information Management , , 2007 . . p.433 - - 444 . . DOI: 10.1007/978-3-540-72909-9_46 http://doi.org/10.1007/978-3-540-72909-9_46 . .

J.V. Franco . . Typical case complexity of satisfiability algorithms and the threshold phenomenon . . Discr. Appl. Math. , , 2005 . . 153 ( ( 1-3 ): ): 89 - - 123 . . DOI: 10.1016/j.dam.2005.05.008]MathSciNetzbMATH http://doi.org/10.1016/j.dam.2005.05.008]MathSciNetzbMATH . .

H. Ganzinger , , , G. Hagen , , , R. Nieuwenhuis , , , A. Oliveras , , , C. Tinelli . . DPLL(T): Fast Decision Procedures . . 16th Int. Conf. on Computer Aided Verification , , 2004 . . p.175 - - 188 . . DOI: 10.1007/978-3-540-27813-9_14 http://doi.org/10.1007/978-3-540-27813-9_14 . .

S. Graf , , , H. Saïdi . . Construction of Abstract State Graphs with PVS . . 9th Int. Conf. on Computer Aided Verification , , 1997 . . p.72 - - 83 . . DOI: 10.1007/3-540-63166-6_10 http://doi.org/10.1007/3-540-63166-6_10 . .

T.S. Heinze , , , W. Amme , , , S. Moser . . A Restructuring Method for WS-BPEL Business Processes Based on Extended Workflow Graphs . . 7th Int. Conf. on Business Process Management , , 2009 . . p.211 - - 228 . . . .

T.S. Heinze , , , W. Amme , , , S. Moser . . Process Restructuring in the Presence of Message-Dependent Variables . . Service-Oriented Computing j ICSOC 2010 Int. Workshops, PAASC, WESOA, SEE, and SOC-LOG , , 2011 . . p.121 - - 132 . . . .

R.M. Karp , , , R.E. Miller . . Parallel program schemata . . J. Comput. Syst. Sci. , , 1969 . . 3 ( ( 2 ): ): 147 - - 195 . . DOI: 10.1016/S0022-0000(69)80011-5]MathSciNetzbMATH http://doi.org/10.1016/S0022-0000(69)80011-5]MathSciNetzbMATH . .

S. Khurshid , , , C.S. Pasareanu , , , W. Visser . . Generalized Symbolic Execution for Model Checking and Testing . . 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems , , 2003 . . p.553 - - 568 . . DOI: 10.1007/3-540-36577-X_40 http://doi.org/10.1007/3-540-36577-X_40 . .

J.C. King . . Symbolic execution and program testing . . Commun. ACM , , 1976 . . 19 ( ( 7 ): ): 385 - - 394 . . DOI: 10.1145/360248.360252]zbMATH http://doi.org/10.1145/360248.360252]zbMATH . .

D. Knuplesch , , , L.T. Ly , , , S. Rinderle-Ma , , , H. Pfeifer , , , P. Dadam . . On Enabling Data-Aware Compliance Checking of Business Process Models . . 29th Int. Conf. on Conceptual Modeling , , 2010 . . p.332 - - 346 . . . .

V. Kumar . . Algorithms for constraint-satisfaction problems: a survey . . AI Mag. , , 1992 . . 13 ( ( 1 ): ): 32 - - 44 . . . .

J. Lee , , , S.P. Midkiff , , , D.A. Padua . . Concurrent Static Single Assignment Form and Constant Propagation for Explicitly Parallel Programs . . 10th Int. Workshop on Languages and Compilers for Parallel Computing , , 1998 . . p.114 - - 130 . . DOI: 10.1007/BFb0032687 http://doi.org/10.1007/BFb0032687 . .

A. Martens . . On compatibility of Web services . . Petri Net Newslett. , , 2003 . . 65 12 - - 20 . . . .

A. Martens . . Analyzing Web Service Based Business Processes . . 8th Int. Conf. on Fundamental Approaches to Software Engineering , , 2005 . . p.19 - - 33 . . DOI: 10.1007/978-3-540-31984-9_3 http://doi.org/10.1007/978-3-540-31984-9_3 . .

H.S. Meda , , , A.K. Sen , , , A. Bagchi . . Detecting Data Flow Errors in Workflows: a Systematic Graph Traversal Approach . . Proc. 17th Workshop on Information Technologies and Systems , , 2007 . . p.133 - - 138 . . . .

H.S. Meda , , , A.K. Sen , , , A. Bagchi . . On detecting data flow errors in workflows . . J. Data Inf. Qual. , , 2010 . . 2 ( ( 1 ): ): 1 - - 31 . . DOI: 10.1145/1805286.1805290 http://doi.org/10.1145/1805286.1805290 . .

B. Meyer . . ntroduction to the Theory of Programming Languages . . Prentice-Hall, Upper Saddle River, NJ, USA , , 1990 . . .

S. Moser , , , A. Martens , , , K. Görlach , , , W. Amme , , , A. Godlinski . . Advanced Verification of Distributed WSBPEL Business Processes Incorporating CSSA-Based Data Flow Analysis . . IEEE Int. Conf. on Services Computing , , 2007 . . p.98 - - 105 . . DOI: 10.1109/SCC.2007.22 http://doi.org/10.1109/SCC.2007.22 . .

T. Murata . . Petri nets: properties, analysis and applications . . Proc. IEEE , , 1989 . . 77 ( ( 4 ): ): 541 - - 580 . . DOI: 10.1109/5.24143 http://doi.org/10.1109/5.24143 . .

F. Puhlmann , , , M. Weske . . Interaction Soundness for Service Orchestrations . . 4th Int. Conf. on Service-Oriented Computing , , 2006 . . p.302 - - 313 . . . .

J. Rushby . . Threatened by a Great Opportunity: Disruptive Innovation in Formal Verification . . Federated Logic Conf , , 2006 . . .

K. Schmidt . . Using Petri Net Invariants in State Space Construction . . 9th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems , , 2003 . . p.473 - - 488 . . DOI: 10.1007/3-540-36577-X_35 http://doi.org/10.1007/3-540-36577-X_35 . .

N. Sidorova , , , C. Stahl , , , N. Trčka . . Workflow Soundness Revisited: Checking Correctness in the Presence of Data while Staying Conceptual . . 22nd Int. Conf. on Advanced Information Systems Engineering , , 2010 . . p.530 - - 544 . . . .

N. Sidorova , , , C. Stahl , , , N. Trčka . . Soundness verification for conceptual workflow nets with data: early detection of errors with the most precision possible . . Inf. Syst. , , 2011 . . 36 ( ( 7 ): ): 1026 - - 1043 . . DOI: 10.1016/j.is.2011.04.004 http://doi.org/10.1016/j.is.2011.04.004 . .

S.X. Sun , , , J.L. Zhao , , , J.F. Nunamaker . . Formulating the data-flow perspective for business process management . . Inf. Syst. Res. , , 2006 . . 17 ( ( 4 ): ): 374 - - 391 . . DOI: 10.1287/isre.1060.0105 http://doi.org/10.1287/isre.1060.0105 . .

N. Trčka . . Workflow Soundness and Data Abstraction: Some Negative Results and Some Open Issues . . Int. Workshop on Abstractions for Petri Nets and Other Models of Concurrency , , 2009 . . p.19 - - 25 . . . .

N. Trčka , , , W.M.P. van der Aalst , , , N. Sidorova . . Data-Flow Anti-patterns: Discovering Data-Flow Errors in Workflows . . 21st Int. Conf. on Advanced Information Systems Engineering , , 2009 . . p.425 - - 439 . . . .

E.P.K. Tsang . . Foundations of Constraint Satisfaction , , : : London, UK Academic Press , , 1993 . . .

W.M.P. van der Aalst . . Verification of Workflow Nets . . 18th Int. Conf. on Application and Theory of Petri Nets , , 1997 . . p.407 - - 426 . . . .

W.M.P. van der Aalst . . The application of Petri nets to workflow management . . J. Circ. Syst. Comput. , , 1998a . . 8 ( ( 1 ): ): 21 - - 66 . . DOI: 10.1142/S0218126698000043 http://doi.org/10.1142/S0218126698000043 . .

W.M.P. van der Aalst . . Information and Process Integration in Enterprises: Rethinking Documents . . Kluwer Academic Publishers, Norwell , , 1998b . . p.161 - - 182 . . DOI: 10.1007/978-1-4615-5499-8_10 http://doi.org/10.1007/978-1-4615-5499-8_10 . .

W.M.P. van der Aalst , , , B.F. van Dongen , , , C. W. Günther , , , A. Rozinat , , , H.M.W. Verbeek , , , A.J.M.M. Weijters . . ProM: the Process Mining Toolkit . . Proc. Business Process Management Demonstration Track , , 2009 . . p.9 - - 12 . . . .

W.M.P. van der Aalst , , , K.M. van Hee . . Workflow Management: Models, Methods, and Systems , , : : London, UK MIT Press , , 2002 . . .

K.M. van Hee , , , N. Sidorova , , , M. Voorhoeve . . Soundness and Separability of Workflow Nets in the Stepwise Refinement Approach . . 24th Int. Conf. on Applications and Theory of Petri Nets , , 2003 . . p.337 - - 356 . . . .

K.M. van Hee , , , N. Sidorova , , , M. Voorhoeve . . Generalised Soundness of Workflow Nets is Decidable . . 2nd Int. Conf. on Business Process Management , , 2004 . . p.197 - - 215 . . . .

H.M.W. Verbeek . . Verification of WF-Nets . . PhD Thesis, Eindhoven University of Technology, Eindhoven, the Netherlands , , 2004 . . .

H.M.W. Verbeek , , , T. Basten , , , W.M.P. van der Aalst . . Diagnosing workflow processes using Woflan . . Comput. J. , , 2001 . . 44 ( ( 4 ): ): 246 - - 279 . . DOI: 10.1093/comjnl/44.4.246]zbMATH http://doi.org/10.1093/comjnl/44.4.246]zbMATH . .

Z. Wang , , , J. Wang , , , L. Wen , , , Y. Liu . . Deriving Canonical Business Object Operation Nets from Process Models . . Proc. 11th Int. Conf. on Enterprise Information Systems , , 2009 . . p.182 - - 187 . . . .

M.T. Wynn , , , W.M.P. van der Aalst , , , A.H.M. ter Hofstede , , , D. Edmond . . Verifying Workflows with Cancellation Regions and OR-Joins: an Approach Based on Reset Nets and Reachability Analysis . . 4th Int. Conf. on Business Process Management , , 2006 . . p.389 - - 394 . . . .

H. Zha , , , W.M.P. van der Aalst , , , J. Wang , , , L. Wen , , , J. Sun . . Verifying workflow processes: a transformationbased approach . . Software Syst. Model. , , 2011 . . 10 ( ( 2 ): ): 253 - - 264 . . DOI: 10.1007/s10270-010-0149-9 http://doi.org/10.1007/s10270-010-0149-9 . .

Views

Downloads

CSCD

Alert me when the article has been cited

Submit

Tools

Publicity Resources

No data

Related Author

No data

Related Institution

No data

Chat

Address：Zhejiang University Press, 148 Tianmushan Road, Hangzhou, China Postal code：310028
Tel：+86-571-88273162 Email：fitee@zju.edu.cn
It is recommended to read the content of this site in Chrome&IE9+. Please switch to extreme mode in browser 360.
Cookies We use cookies to help provide and enhance our service and tailor content. By continuing, you agree to the use of cookies.

⁰