Description of Web service composition model based on Z notation

In this paper, we propose an approach that gives a formal description of Web service composition. With the number of Web service increasing dramatically, the user has a large choice of services. Since a single Web service cannot meet the user´s complex requirements, it is necessary to integrate the existing single Web service to generate more complex functionality. In our approach, we model Web service composition using Z notation through an example. Firstly we formally describe the behavior of a single Web service, and then describe the communications among services. In this way, we offer the formal description of web service composition, which has precise composition semantics and help guarantee the correctness of service composition.