Toward a Pi-Calculus Based Verification Tool for Web Services Orchestrations

Abstract. Web services constitute a dynamic field of research about technologies of the Internet. WS-BPEL 2.0, is in the way for becoming a standard for defining Web services orchestration. To check the good behaviour of the produced compositions, but also to check equivalence between services, formalization is necessary. In this paper a contribution to the field of Formal Verification of Web services composition is presented using a calculus-based approach for the verification of composite Web services by applying model checking methods. We adopt the possibility of exploiting benefits from existing works by translating a Business Process Language such as BPEL to a system model of the -calculus for which analysis and verification techniques have already been well established and there are existing tools for model checking systems. We therefore present the basis of a framework aimed to specification and verification, related to some temporal logic, of Web services composition. ...

• Type: Conference
• Year: 2006
• Where: CSAC
• Authors: Faisal Abouzaid
• Keywords: CSAC 2006, Model Checking, Software Engineering, Web Services, Web Services Composition