On formalizing and verifying web services

Web services are becoming an important paradigm for web-based computing. However the mainstream web service description language such as WSDL (Web Service Description Language) is lack of formal basis. In order to verify the behavioral properties of web services, we adopt the π-calculus as a precise language because it provides many useful facilities such as behavioral equivalence, mobility that are lack in other formal language. The basic elements of WSDL are translated into the terms in the π-calculus. By means of the MWB (Mobility Workbench), a concurrency tool, the behavioral property of web services denoted by processes is verified.