Formal specification and validation of refinement from WS-CDL to BPEL

Service composition is a primary task in the development of service-oriented systems. The Web Service Process Execution Language (WS-BPEL) and the Web Service Choreography Descriptor Language (WS-CDL) are two major languages for Web services modeling and implementation. Although these two composition models are of a different nature, they are complementary. WS-CDL serves as a behavioral modeling language for collaboration between multiple participants (web services) within the same business process from a global point of view. However, WS-BPEL allows a service composition process to be described at different levels of abstraction. At a high level, the description follows a global point of view and deals only with the exchange of messages between participating abstract services (represented abstractly by roles). WS-CDL descriptions are thus considered as a specification of the abstract service composition from which more concrete WS-BPEL processes are extracted. In this article, we present a formal modeling and analysis approach based on sequential communication process (CSP) in order to verify the behavioral consistency between abstract choreographic descriptions and executable BPEL processes, thereby proving the correctness of the translation process.

I. Introduction

Web services have become a key technique for building loosely coupled distributed systems. Web services are software components that enable the interoperability of heterogeneous computing applications in distributed environments. The web service exposes its functionality through an interface described in a computer-readable XML format (WSDL language). The other systems interact, without human intervention, with the web service according to a prescribed procedure using the SOAP protocol messages [1]. However, a web service can only offer task-specific functionality, and most of the time can not meet the complex demands of users.