The Nature Of The Inspection Of Web Service Composition And Realization

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 a service composition method based on business process, is weak in modeling and compositing. So the validity of the process and the property of non-deadlocks must be simulated and proved before the service composition is being implemented formally.According to the requirement mentioned above, using Pi-calculus and mu-calculus, a method for checking the property of BPEL4WS has been put forward in this thesis, as well as a tool for checking reachable and deadlocks.People could check BPEL4WS files roughly automatic on, when it finds error, it will tag error on BPEL4WS files.It is almost transparent, from modeling to checking, to user, the user who doesn't understand the formal method thoroughly, can do the check using the tool and do the improvement at the tagged place. The simulation result shows that it is feasible to check the property of BPEL4WS and tag the error path automatically.