Abstract: In order to excute Web composite service and implement automatic composition of Web service, this paper discussed the correctness of the translation between WSDL and Pi calculus based model for Web services composition. Web services and their composition were described and modeled by process algebra, PICM2WSDL (Pi-calculus model to WSDL) model was proposed in this paper. Formal methods verify that correct WSDL would be generated automaticall by Web service modeling based on Pi calculus translated by PICM2WSDL.