中文摘要：

为顺利地执行Web复合服务，实现服务的自动组合，对基于Pi演算的Web服务组合模型与WSDL语言程序段转换的正确性进行了论证．运用进程代数对Web服务及其组合进行建模，提出并建立了PICM2WSDL模型．通过形式化的方法验证，基于Pi演算的Web服务建模经过PIC2WSDL模型转换可自动生成正确的．wsdl文件。

英文摘要：

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.