Verification of Web Services Compositions: Applying Model Checking to BPEL4WS

A composite Web service is a service implemented by combining the functionality of other Web services. There are some applications, like B2B E-commerce, in which an error in the specification of the composite service is critical, because of the high economic looses that it could cause. In this work we propose a framework for the verification of Web services compositions, called VERBUS. Its aim is to help the designer to find errors in the specifications at design time, thus increasing their reliability. Contrary to verification frameworks previously proposed for Web services compositions, VERBUS is a modular an extensible framework. It does not use a specific compositions definition language or a specific verification tool, like them. Instead, VERBUS is an open framework in which new definition languages and verification tools can be easily added. In order to show the feasibility of this environment we have implemented a prototype that can verify BPEL4WS compositions using the model checker Spin.