Analysis of Web Service Substitutability Based on Typed Pi-Calculus

Web service substitutability refers to identify a suitable service to replace the failed service in Web service composition (WSC) and make sure the new WSC can still run correctly. Because of lack of data types, pi-calculus canpsilat verify the consistency of data types during the substitution processes. In this paper, we extend pi-calculus with a type system and present its syntactic descriptions, subtyping relationships and judgment rules of well typeness. We also propose the definitions of Web service behavioral substitutability and type weak simulation based on behavioral equivalence theory. After that, a substitutability judgment algorithm is given. Finally, a case study is used to demonstrate how to use our typed pi-calculus to formally descript WSC and discuss Web services substitutability from the aspects of data types consistency and behavioral equivalence, as well as the evolvement of system structure due to substitution.