Verification for the concurrent properties of evolving BPEL composite service

BPEL composite service inevitably evolves to meet various requirements. Most researchers only consider the verification of single versions. However, applying the original costly verification method to subsequent versions during evolution is very expensive, especially for large systems. To address this challenge, we proposed a new approach to incrementally verify the concurrent properties of the evolved version, including deadlock-free, non-conflict and link non-redundant. With XCFG, which can formally model the BPEL process, it is convenient to identify the changes between the consecutive versions of composite service by comparing their XCFGs. Then it concentrates on the changes to incrementally analyze whether violations exist for the three concurrent properties. Finally, a case study is illustrated to show the effectiveness and efficiency of the incremental method.