Title :
Verifying the Concurrent Properties in BPEL Based Web Service Composition Process
Author :
Bixin Li ; Shunhui Ji ; Dong Qiu ; Leung, Henry ; Gongyuan Zhang
Author_Institution :
Sch. of Comput. Sci. & Eng., Southeast Univ., Nanjing, China
Abstract :
The relatively new web service software paradigm involves services which are loosely coupled, highly reusable and flexible. By specifying the workflow of individual services, Web service composition enhances the ability to handle more complex business processes and provides many value-added services. In this article, we propose an extended control flow graph (XCFG) to formally model the workflow of Web service composition specified in BPEL, and corresponding techniques to verify concurrent properties, such as deadlock-free, non-conflict, and link non-redundant. XCFG can model not only the workflow of BPEL but also the synchronization control dependencies among concurrent activities. Meanwhile, each element of XCFG keeps record of related information of corresponding activity in BPEL so as to support further analysis and verification. Experimental study validates the effectiveness and efficiency of the proposed XCFG-based technique.
Keywords :
Web services; business data processing; concurrency control; flow graphs; formal verification; BPEL; Web service composition; Web service software paradigm; XCFG; complex business processes; concurrent activities; concurrent properties; deadlock-free techniques; extended control flow graph; formal verification; link nonredundant techniques; nonconflict techniques; service workflow; synchronization control dependencies; value-added services; Analytical models; Bills of materials; Concurrent computing; DSL; Process control; Synchronization; Web services; BPEL; Formal verification; Web service composition; XCFG;
Journal_Title :
Network and Service Management, IEEE Transactions on
DOI :
10.1109/TNSM.2013.111113.120379