Reach-ability Analysis of a Cooperative Work Flow Model
Annappa B, K Chandrasekaran, K C Shet
Journal of E-Technology, Vol. 1, No. 1, 2010.
DOI: 
Link: http://www.dline.info/jet/fulltext/v1i1/4.pdf
Abstract:
Use of Petri nets to verify the reach-ability and soundness of a cooperative workflow model is presented in this paper. First, we outline a cooperative workflow model, which is a modified version of Bonita workflow model. Bonita is open source cooperative workflow management software which is an ongoing project from object web consortium. Then we describe the cooperative workflow model using a special kind of Petri net called Wf-net. Next we employ WF-net for verification of the model for reachability and soundness properties. The Petri net based verification shows that the model is reachable and sound.