Verificación de Composiciones de Servicios Web: Aplicación de Model Checking a BPEL4WS (Verification of Web Services Compositions: Applying Model Checking to BPEL4WS)

Jesús Arias Fisteus (jaf@it.uc3m.es), Carlos Delgado Kloos (cdk@it.uc3m.es), Luis Sánchez Fernández (luis.sanchez@uc3m.es)


Departamento de Ingeniería Telemática, Universidad Carlos III de Madrid, Spain
This paper appears in: Revista IEEE América Latina

Publication Date: March 2005
Volume: 3,   Issue: 1 
ISSN: 1548-0992


Abstract:
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.

Index Terms:
Service oriented architectures, Software verification and validation, Web services, Web services composition.   


Documents that cite this document
This function is not implemented yet.


[PDF Full-Text (213)]