A Way to Model Flow Construct and Its Three Properties Verification for BPEL Specification

A kind of concurrent-based model of control flow is proposed for the analysis and verification of interactions of composite web services which are specified in BPEL. First, a verification framework of concurrent construct is presented, then we convert the choice flow into concurrent flow with link semantics to simplify the description and verification methods of formal model. Furthermore, deadlock-free, meaning-full and non-conflict, three properties of this model are defined. Meanwhile, the meaning and verification methods for the three properties are discussed. Finally, an example of composite service is given to prove the usability of the model and verification methods.