Title: Interface theory-based formalisation and verification of orchestration in BPEL4WS
Authors: Zhenbang Chen, Ji Wang, Wei Dong, Zhichang Qi
Addresses: National Laboratory for Parallel and Distributed Processing, Changsha, China. ' National Laboratory for Parallel and Distributed Processing, Changsha, China. ' National Laboratory for Parallel and Distributed Processing, Changsha, China. ' National Laboratory for Parallel and Distributed Processing, Changsha, China
Abstract: BPEL4WS (BPEL) is a web service composition language for service-oriented computing. Service orchestration can be specified by executable processes in BPEL. However, it lacks of a formal foundation for specification and verification of service-oriented systems. This paper presents an improved protocol interface for web services. Compared to the existing interface theory, the presented interface can describe some more advanced features of long running transaction such as nested transaction. An interface theory-based formalisation is presented for service orchestration in BPEL. The transformational approach is proposed for translating BPEL processes to protocol interfaces. With the formalisation, a formal technique is presented for model checking of BPEL program with respect to the protocol properties. A set of case studies are demonstrated to illustrate our approach.
Keywords: service composition; web services; transaction; BPEL4WS; interface theory; verification; service-oriented computing; protocol interface; BPEL.
DOI: 10.1504/IJBPIM.2007.017752
International Journal of Business Process Integration and Management, 2007 Vol.2 No.4, pp.262 - 281
Published online: 01 Apr 2008 *
Full-text access for editors Access for subscribers Purchase this article Comment on this article