Property Checking Of BPEL4WS Based On π-calculus

Along with the prosperity and acceptance of the Web services, the technique of dynamic service composition based on Web Services has been regarded as one of the hot research topics. 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.Based on the research of formal method, the method of checking the property of BPEL4WS, which make use of π -calculus and μ -calculus, has been put forward in this paper.In the aspect of modeling, in addition to put forward a method of modeling, in consideration of the complications of modeling by user, we have carried out the automatic conversion algorithm for modeling the BPEL4WS by π--calculus. Using the tool mentioned in this paper, the BPEL4WS file specified by user can create the π-calculus model automatically.In the aspect of describing property, we have analyzed someerrors which appear probably in BPEL4WS, and given the description example in u -calculus.In the aspect of tool, we have developed a new tool which carried out the automatic modeling mentioned in preceding context.This new tool, embedding the being tool ---- MWB and improvingthe algorithm, can return the erring snippet when the model can' t fulfill some given properties, and first try to remark the error path in the BPEL4WS source file, implementing the automatically check on the properties of BPEL4WS.It is almost transparent from modeling to checking for user. So, the user who doesn' t understand the formal method thoroughly can do the check using the tool and do the improvement aiming at the tagged place. The result of this paper has explained that it is feasible to check the property of BPEL4WS and tag the erring path automatically.