Paper Info
Title
Verifying the Correctness of Workflow Systems Based on Workflow Net With Data Constraints.
Abstract
The correctness verification is very important for workflow systems. It is closely related with both control-flows and data-flows. Workflow nets with data (WFD-nets) are a kind of formal model that can reflect some logical structures of workflow systems, e.g., choice and concurrency, and represent some operations on data, e.g., read, write, and delete. However, these data operations are conceptual in WFD-nets and only characterize the logical relation between two operations, e.g., whether a write and a read are concurrently operating on a data. They do not consider the functional requirements about data (i.e., data constraints). Thus, some data errors cannot be found via WFD-nets. In order to solve this problem, we propose Workflow nets with Data Constraints (WI-DC-nets) and define four levels of soundness to describe different correctness requirements. Based on the reachability graphs of WFDC-nets, we verify the soundness. The related algorithms are proposed and a tool is developed to show the effectiveness and usefulness of our method.
Year
DOI
Venue
2018
10.1109/ACCESS.2018.2806884
IEEE ACCESS
Keywords
Field
DocType
Workflow systems,data constraints,Petri nets,soundness
Functional requirement,Data modeling,Petri net,Programming language,Computer science,Concurrency,Correctness,Reachability,Soundness,Workflow,Distributed computing
Journal
Volume
ISSN
Citations 
6
2169-3536
1
PageRank 
References 
Authors
0.36
0
6
Name
Order
Citations
PageRank
Yaqiong He110.69
GuanJun Liu217626.24
Dongming Xiang392.21
Jiaquan Sun410.69
Chun-Gang Yan56215.97
Changjun Jiang61350117.57