| Web Service composition has solved the problems of the integration and collaboration of the heterogeneous application on internet. Modeling of Web Service intergration is a complex and error-prone process. If a mistake is found after a service was brought into operation, it would take high cost to recify this mistake. More over, the efficiency of business is directly associated with the correctness of process structure. Therefore, the verification of BPEL process structure is an important issue in the research field of Web Service. So far, research in this area is limited on the theoretical level and there is lack of practical tools.In this paper, a BPEL process debugging tool based on an improved model of Petri-net, which is defined as PNBP(Petri-Net for BPEL Process), is proposed to achieve the verification and simulation of BPEL process. The details are as follows:(1) Based on the analysises of Petri-net theory, PNBP is put forward to modeling BPEL process. According to the definition, the modelings of process normal sequence, simultaneousness, branch and cycle are implemented.(2) After modeling, the BPEL process is validated by three methods for each time. They are Coverability Tree, Incidence Matrix and State Equation, Transfer Matrix. All of them validated the security, reachability and deadlocks.(3) Further more, the debugging tool is designed and finally implemented. From the angle of implementation, the demostration of this paper mainly focuses on some specific parts. They are transformation from BPEL files to PNML (Petri Net Markup Language) files, the analysis of PNML files and the valification procedure. Based on the debugging process of a case of loan approval, the modeling, verification and simulation of BPEL are showed.The tool has been verified in the research called "Business Process-oriented software product line", which is the sub-topic of the national high-tech development project—"high confidence software product line". |