Abstract: To enhance the credibility of Web service composition, Pi calculus based formal verification of trust Web service composition is proposed. Trust Web service composition is firstly defined abstractly, and then the powerful behavioral theory of Pi-calculus is used to depict structure and internal interaction of trust Web service composition, and the mapping relation between trust entity and Pi calculus is discussed. Automatic reasoner MWI3 is used to analyze and reason the trust Web service composition system, which is aimed at finding and correcting the faults before the execution of trust authentication of Web service composition and meet the users' demands on trust quality effectively.

Key words: Pi-calculus, Trust Web service composition, Model