Research on Web Service Interface Extending and Composition Compatibility Checking Based on pi Calculus

Service interface description is one of the most important problems in services-oriented software architecture, and formal description methods are considered to be a promising approach for service interface. Presently the typical Web service description language (WSDL) only provided the syntax level information that needed by the service interaction without containing the dynamic behavioral protocol information. So it can not guarantee the correct interaction and usage of the service in the open environment. The paper first defined the signature view and the behavior view of the service then designed the modeling method that transfer the Web service behavior into pi calculus process expression and proposed the algorithm that makes the service view transfer into pi calculus process automatically. At last with the help of operational and transitional semantics and formal deduction we can check whether two services are behavior compatible when their composition.