Verification Of Web Servies Composition Based On Pi-Calculus

Service-oriented architecture is deemed as the developing direction of the distributed computing and software developing, web service, one method of implementing SOA, whose value is the service reusing. Web service composition technology which based on SOA provides a resolvement for service reusing and increment, moreover, it has the merit of loose coupling, industrial support and high integration.One of important issue in web service composition researching area is how to describe Web service composition formally and verify the correctness of Web service composition. A formal model of Web service composition can be used to check and verify Web service composition so that the correctness of Web service composition can be guaranteed. The composition of Web services involves communication and collaboration of several Web service, this characteristic makes the verification of the composition of Web services more difficult. Further more, the Business Process Execution Language for Web services(BPEL4WS) as to be a service composition method, which is based on business process, is weak in modeling, and the assurance of the validity is also weak. So the validity of the process and the property of non- deadlocks must be simulated and Proved before being implemented formally.Aimed at this problem, a Web service composition modeling method based on Pi-calculus is presented, using concurrent operators Pi-calculus provided, a Web service composition is modeled as a composition of a set of concurrent Web services, on the basis of this specification, the correctness of Web service composition process is verified. The main points of this thesis are as follows:(i) On the basis of studying process algebra theory, Web service composition modeling and the BPEL4WS specification, the mapping from Web service composition Language-BPEL4WS to Pi-Calculus is proposed.(ii) A Pi-Calculus based method is brought forward to formalize and validate the WS-CDL choreography. The correctness of the WS-CDL choreography is guaranteed, and the cost which due to the failure of the Web service execution is decreased.(iii) Web service composition is formalized and modeled using Pi-Calculus and its correctness is verified, and then a feedback result is presented,(iv) A concrete transaction scenario is put forward for verifying the correctness of the WS-CDL choreography. The verification of Web service composition is not on the architecture layer, but on the program code written by Web service composition Language, consequently the feasibility and practicability is even more.