Describing And Verifying Web Service Using Type Theory

With the development of the specifications and platforms for Web service, more and more web services can be accessed easily as well as the applications based on web service. However the current protocol for Web services are almost describable without the support from the basic theory and the tools for the verification. With the deep research about Web services, disadvantage limits the development of Web service, for example, the area of automate composition of web services.In recent years several formalisms for program construction have been introduced. One such formalism is the type theory developed by Per Martin-L"of. It is well suited as a theory for program construction since it is possible to express both specifications and programs within the same formalism. Furthermore, the proof rules can be used to derive a correct program from a specification as well as to verify that a given program has a certain property. Then It is a suitable theory for the research of web services, especially for the area of automate composition of web services.In the paper, our contributions for the web services are described below:Firstly, we will define all the basic elements in web service using Martin-Lof's type theory. In the meanwhile, we will show the definition of the matching of web services and the calculation of the matching.Secondly, we will describe the verification of matching for web service. According to the definition, we will give the process of compute from the description.Lastly, we will give the details about a platform which will implement the matching and verifying for web services using Martin-Lof type theory. It is the basic project for the automated composition for Web services.