Modeling And Verification Of Web Service Composition Based On The ¦Ð-calculus

Web service composition is a technology which is based on service-oriented architecture. It realized the reuse and enhancements of services through composing the single function and individual Web services which can solve some problems about integration and collaboration of the heterogeneous application on internet.Web service composition is a very complex process which involves communication collaboration of multiple Web services. So verirying the Web service composition is very difficult. But it's necessary to verify the Web services composition. The most widely used language to describe the Web service composition are WSFL, XLANG, WS-CDL, BPEL, and so on. They have a common drawback that is there isn't formal tool to support their verification. So how to formal modeling and verify of the Web service composition is an important issue.This paper presents a Web service composition based onπ-calculus modeling through a lot of research about formalization modeling,results include the following three aspects:.(1) BPEL business process modeling based onπ-calculusThis paper presents a number of modeling methods about a series of key elements of BPEL,and achieves the automationπ-calculus modeling about BPEL.(2) BPEL business process model verification based onπ-calculus.This paper presents correctness verification algorithm which includes deadlock,livelock, reachability verification.(3) Design and Implementation of WMVTool.Design and implemented an automatedπ-calculus modeling and verification tool about Web services composition-WMV Tool.