Compliance verification using a joint model of open workflow net and global calculus

In a collaborative workflow environment, interaction protocol is adopted as a contract, which every peer process must comply with. In order to verify the compliance, we develop a joint model of Open Workflow Net (oWFN) and Global Calculus by establishing a connection between their grammars, and denote the joint model Dynamic oWFN (DoWFN). We construct the Reachability Graph (RG) of DoWFN, and we prove that by analyzing RG of DoWFN, we can verify the compliance of peer process and interaction protocol. We adopt 13 oWFN reduction rules to shrink the size of Reachability Graph, thus reducing the time complexity of the compliance verification. In order to validate our method, we implement a tool tValidator and test it on practical scenarios.