Petri Net Modeling and Verification of Transactional Workflows

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.