Most of existing formal models for BPEL based Web Services composition are without description of deadpath-elimination semantics. There are Petri net based models describing the dead-path-elimination semantics, while the models are too big to handle large scale processes. In this paper, a new model called DPE net is advanced to describe the WS-BPEl process under the dead-path-elimination semantics. We give the DPE net models describing the basic control flow, relatively complete links semantics and deadpath-elimination semantics, and introduce how to analyze properties of the WS-BPEL process based on DPE Reachability Graph. The features of DPE net make the DPE net model for the WS-BPEL process smaller than the model based on P/T net. Moreover, the DPe Reachability Graph allows several transitions to be fired in one step, which reduces the reachability graph's size dramatically.
展开▼
