Formal methods are effective ways to model and verify software system. To Describe and verify Web services by formal method is considered as an important research field. Guaranteeing the correctness of Web services composition is indispensable for enhancing the value of services. Pi-calculus is a kind of process algebra which can be used to model asynchronous concurrent communication network. A Picalculus based context aware model for Web service composition is presented. Web services behavior are described and modeled based on Pi-calculus in this paper. Finally, a case study is presented and the validity of composition model is verified.