Improving correctness of BPEL program with Petri net
应用Petri网改进BPEL程序的正确性*

To solve the problem of correctness of composite Web service defined by the BPEL, this paper presented an integrated method for improving the correctness of composite Web service defined by BPEL against Petri net. The rules were firstly presented for translating the composite Web service defined by BPEL into a Petri net described by PNML. Then, the algorithms for deriving Petri net presented by PNML from BPEL program and generating transition fired sequences from Petri net were presented. With an open source tool PIPE2, the correctness, liveness and other properties of BPEL program could be ve-rified and analyzed. Generated the test sequence for testing BPEL program from the fired sequences. The case study shows that the presented method is feasible to improve the correctness of BPEL program.