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 Full-text access for subscribers Purchase this article Comment on this article