Interface theory-based formalisation and verification of orchestration in BPEL4WS

Author： Chen Zhenbang Wang Ji Dong Wei Qi Zhichang

ISSN： 1741-8763

Source： International Journal of Business Process Integration and Management, Vol.2, Iss.4, 2008-04, pp. : 262-281

Disclaimer: Any content in publications that violate the sovereignty, the constitution or regulations of the PRC is not accepted or approved by CNPIEC.

Previous Menu Next

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.