Describing and Verifying Web Service Using Type Theory

A Web service is a basic software component that can be accessed by standard Internet protocols. It provides a new approach to cooperative and federated computing among different organizational units. There are many specifications which can describe the elements of Web services and make the end-users interact with each other. However, they are remaining at the descriptive level, without supporting any kind of mechanisms or tools for the verifying the specified attributes of the Web services. In the paper, we provide a mathematical scheme, type theory, to describe the basic elements of Web services and the specified attributes. We also present the mechanism to deduce the automated programs in other languages (for example ML) from the type theory. Thus we can verify the behavioral properties of a Web service as well as analyzing and verifying Web services composition