Verifying the Correctness of Workflow Systems Based on Workflow Net With Data Constraints
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 s...
| Main Authors: | , , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
IEEE
2018-01-01
|
| Series: | IEEE Access |
| Subjects: | |
| Online Access: | https://ieeexplore.ieee.org/document/8293772/ |
| _version_ | 1818853910607036416 |
|---|---|
| author | Yaqiong He Guanjun Liu Dongming Xiang Jiaquan Sun Chungang Yan Changjun Jiang |
| author_facet | Yaqiong He Guanjun Liu Dongming Xiang Jiaquan Sun Chungang Yan Changjun Jiang |
| author_sort | Yaqiong He |
| collection | DOAJ |
| description | 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 (WFDC-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. |
| first_indexed | 2024-12-19T07:44:19Z |
| format | Article |
| id | doaj.art-f767c22360ef4f91913f4c516b3159ea |
| institution | Directory Open Access Journal |
| issn | 2169-3536 |
| language | English |
| last_indexed | 2024-12-19T07:44:19Z |
| publishDate | 2018-01-01 |
| publisher | IEEE |
| record_format | Article |
| series | IEEE Access |
| spelling | doaj.art-f767c22360ef4f91913f4c516b3159ea2022-12-21T20:30:24ZengIEEEIEEE Access2169-35362018-01-016114121142310.1109/ACCESS.2018.28068848293772Verifying the Correctness of Workflow Systems Based on Workflow Net With Data ConstraintsYaqiong He0https://orcid.org/0000-0002-4452-5787Guanjun Liu1https://orcid.org/0000-0002-7523-4827Dongming Xiang2Jiaquan Sun3Chungang Yan4Changjun Jiang5Key Laboratory of Embedded System and Service Computing, Ministry of Education, Tongji University, Shanghai, ChinaKey Laboratory of Embedded System and Service Computing, Ministry of Education, Tongji University, Shanghai, ChinaKey Laboratory of Embedded System and Service Computing, Ministry of Education, Tongji University, Shanghai, ChinaKey Laboratory of Embedded System and Service Computing, Ministry of Education, Tongji University, Shanghai, ChinaKey Laboratory of Embedded System and Service Computing, Ministry of Education, Tongji University, Shanghai, ChinaKey Laboratory of Embedded System and Service Computing, Ministry of Education, Tongji University, Shanghai, ChinaThe 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 (WFDC-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.https://ieeexplore.ieee.org/document/8293772/Workflow systemsdata constraintsPetri netssoundness |
| spellingShingle | Yaqiong He Guanjun Liu Dongming Xiang Jiaquan Sun Chungang Yan Changjun Jiang Verifying the Correctness of Workflow Systems Based on Workflow Net With Data Constraints IEEE Access Workflow systems data constraints Petri nets soundness |
| title | Verifying the Correctness of Workflow Systems Based on Workflow Net With Data Constraints |
| title_full | Verifying the Correctness of Workflow Systems Based on Workflow Net With Data Constraints |
| title_fullStr | Verifying the Correctness of Workflow Systems Based on Workflow Net With Data Constraints |
| title_full_unstemmed | Verifying the Correctness of Workflow Systems Based on Workflow Net With Data Constraints |
| title_short | Verifying the Correctness of Workflow Systems Based on Workflow Net With Data Constraints |
| title_sort | verifying the correctness of workflow systems based on workflow net with data constraints |
| topic | Workflow systems data constraints Petri nets soundness |
| url | https://ieeexplore.ieee.org/document/8293772/ |
| work_keys_str_mv | AT yaqionghe verifyingthecorrectnessofworkflowsystemsbasedonworkflownetwithdataconstraints AT guanjunliu verifyingthecorrectnessofworkflowsystemsbasedonworkflownetwithdataconstraints AT dongmingxiang verifyingthecorrectnessofworkflowsystemsbasedonworkflownetwithdataconstraints AT jiaquansun verifyingthecorrectnessofworkflowsystemsbasedonworkflownetwithdataconstraints AT chungangyan verifyingthecorrectnessofworkflowsystemsbasedonworkflownetwithdataconstraints AT changjunjiang verifyingthecorrectnessofworkflowsystemsbasedonworkflownetwithdataconstraints |