Formal specification and validation of refinement from WS-CDL to BPEL
Khadidja Salah-Mansour, Youcef Hammal, Lynda Mokdad · 2019
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.