| One of an important question in web service composition researching area is how todescribe Web service composition formally and verify the correctness of Web servicecomposition. Using Pi-calculus model Web services composition can be used to check and verifyWeb service composition in order to ensure the correctness of Web service composition. Becausethe composition of Web services involves communication and collaboration of several Webservice, this feature makes the verification of the composition of Web service more difficult.Besides, the Business Process Execution Language for Web services (BPEL4WS) as to be aservice composition method, which is based on business process, is weak in modeling, and theassurance of the validity is also weak. So the validity of the process and the property ofnon-deadlocks must be simulated and proved before being implemented formally.Using formal method is an effective way for modeling and verifying software system.Describing and verifying Web Services by formal method is an important research. Guaranteeingthe validity of Web services is very important for enhancing the value of services. Web servicesand their composition are described and modeled based on Pi-calculus in this paper. Rules aboutapplying Pi-calculus to Web services are explained and the method of working out agents andchannels is proposed. Relationship between Pi-calculus and Web services protocol stack isillustrated too. Finally, a demo is constructed and the validity of composition model is verified.Compared with process algebra method based on CCS, the Pi-calculus can be used for describingand reasoning dynamic system and appropriate for modeling Web services composition. Besides,using the mutual simulation theory of the Pi-calculus, we also verify the compatibility andbehavior equivalence about the Web service composition. |
PDF Full Text Request