TY - GEN
T1 - Petri net modeling and verification of transactional workflows
AU - Klai, Kais
AU - Gaaloul, Walid
PY - 2011/9/15
Y1 - 2011/9/15
N2 - The increasing use of Workflow Management Systems (WfMS) in companies expresses their undeniable importance to improve the efficiency of their processes and their execution costs. However, with the technological improvements and the continuous increasing market pressures and requirements, collaborative information systems are becoming more and more complex, involving numerous interacting business objects. Consequently, in spite of their obvious potential, WfMS show some limitations to ensure a correct and reliable execution. Therefore, there is a growing interest for verification techniques which help to provide reliable transactional workflow behavior and thereafter prevent workflow execution failures. In this paper, we propose a Petri net driven approach to validate workflow transactional behavior to subsequently improve and correct related recovery mechanisms. The transactional behavior verification is done at design time to validate the transactional behavior consistency and help designers to provide correct recovery mechanisms. By using Petri nets and Temporal Logic formalisms to specify and check the transactional behavior consistency, the approach we present in this paper provides a logical foundation to ensure workflow execution reliability.
AB - The increasing use of Workflow Management Systems (WfMS) in companies expresses their undeniable importance to improve the efficiency of their processes and their execution costs. However, with the technological improvements and the continuous increasing market pressures and requirements, collaborative information systems are becoming more and more complex, involving numerous interacting business objects. Consequently, in spite of their obvious potential, WfMS show some limitations to ensure a correct and reliable execution. Therefore, there is a growing interest for verification techniques which help to provide reliable transactional workflow behavior and thereafter prevent workflow execution failures. In this paper, we propose a Petri net driven approach to validate workflow transactional behavior to subsequently improve and correct related recovery mechanisms. The transactional behavior verification is done at design time to validate the transactional behavior consistency and help designers to provide correct recovery mechanisms. By using Petri nets and Temporal Logic formalisms to specify and check the transactional behavior consistency, the approach we present in this paper provides a logical foundation to ensure workflow execution reliability.
U2 - 10.1109/WETICE.2011.72
DO - 10.1109/WETICE.2011.72
M3 - Conference contribution
AN - SCOPUS:80052613018
SN - 9780769544106
T3 - Proceedings of the 2011 20th IEEE International Workshops on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE 2011
SP - 176
EP - 184
BT - Proceedings of the 2011 20th IEEE International Workshops on Enabling Technologies
T2 - 2011 20th IEEE International Workshops on Enabling Technologies: Infrastructure for Collaborative Enterprises, WETICE 2011
Y2 - 27 June 2011 through 29 June 2011
ER -