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

计算机与自动化 | Updated：2022-12-09

- Verification of workflow nets with transition conditions
- Verification of workflow nets with transition conditions
- 信息与电子工程前沿（英文） 2012年13卷第7期页码：483-509
- 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：
  
  Project supported by the National Science and Technology Major Project of China (No. 2010ZX01042-002-002-01), the National Basic Research Program (973) of China (No. 2009CB320700), and the National Natural Science Foundation of China (Nos. 61073005 and 61003099)
- DOI：10.1631/jzus.C1100364
  中图分类号： TP311
- 收稿：2011-12-08，
  
  修回：2012-;5-31，
  
  纸质出版：2012-07
- Accepted：
Scan QR Code
Verification of workflow nets with transition conditions[J]. 信息与电子工程前沿（英文）, 2012,13(7):483-509.

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.
Verification of workflow nets with transition conditions[J]. 信息与电子工程前沿（英文）, 2012,13(7):483-509. DOI： 10.1631/jzus.C1100364.

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

浏览量

Downloads

CSCD

文章被引用时，请邮件提醒。

Submit

工具集

关联资源

暂无数据