Paper Info
Title
Verification of behavioral soundness for artifact-centric business process model with synchronizations
Abstract
A correct business process model is the key to achieving a business goal through business process management. In recent years, artifacts have been proposed as a paradigm to capture dynamic and inter-organizational processes in a more natural way. In artifact-centric modeling approach, a business process is modeled as interaction of the involved artifact lifecycles, in which the control flows are implicit in business rules. The interaction significantly complicates the process execution due to synchronizations, which poses great challenges for the verification of one fundamental correctness criteria: behavioral soundness. This paper aims to address this problem, i.e., the verification of behavioral soundness for an artifact-centric process model with synchronizations. First, each artifact lifecycle involved is mapped to a Petri net representation. Then we propose the rules to integrate the Petri nets into a workflow net based on the synchronization constraints. With the workflow net, a reachability graph is calculated to derive all the implicitly specified service execution sequences. Finally, the behavioral soundness (i.e., proper completion) is checked by verifying whether every specified service execution sequence can complete properly or not from its control flow and data flow respectively. A case study is presented to demonstrate the effectiveness of our approach.
Year
DOI
Venue
2019
10.1016/j.future.2019.03.012
Future Generation Computer Systems
Keywords
Field
DocType
00-01,99-00
Artifact-centric business process model,Business process management,Petri net,Business process,Software engineering,Computer science,Business process modeling,Soundness,Business rule,Distributed computing,Data flow diagram
Journal
Volume
ISSN
Citations 
98
0167-739X
0
PageRank 
References 
Authors
0.34
0
3
Name
Order
Citations
PageRank
Kang, G.1295.56
Liqin Yang221.07
Liang Zhang346492.08