In recent years, Web services had been widely used on the Internet. Thanks to the convenient communication technologies and their inexpensive cost, communications between organizations is much easier, and Web services have become a de-facto standard for organizations to provide information and services. There are two different perspectives to describe Web service composition: orchestration and choreography. Works that verify a choreography model so as to alleviating some correctness problem such as deadlock have also been proposed. However the verification of implementations based on a choreography model has not be addressed. In this thesis, we propose an approach to verify the conformance of a set of Web services to a given choreography model and prune some candidate Web services which do not comply with the choreography model to avoid discordance with the choreography model and run-time errors. The proposed approach is evaluated by simulating 10,000 execution sequences of composite Web services. The experimental results show that our proposed method improves the performance of success rate and space usage by pruning the unsuitable candidate Web services.

Nowadays, Web Services technology has become a standard to integrate business processes across organizations. In general, there are two approaches for web service composition: Orchestration and Choreography. Orchestration is used to develop a single process that integrates services within or across an organization to achieve a business goal. On the other hand, Choreography is often used for cross-organizational communication and serves as a specification for communication. In a choreographed environment, each Web service is an independent entity, and each service selects the partner services using its own selection policy without knowing all the other services in the choreography. In this thesis, we use £k-calculus for modeling the Web Services. Afterwards, we propose an approach for each constituent process to choose and invoke other processes using the limited information provided by its partners. In our method, each service proclaims the requirments of its potential service providers (or consumers) and itself and provides to its partners. Subsequently each service will generate a local view using the information provided by its service consumers and providers to guide the selection. We evaluate our method by simulating 100,000 executions with different degrees of service availability. The experimental results indicate that our proposed method can indeed improve the success rate of the entire choreography.