A BPEL Program Verification Method Research Based On Mealy Machine

As one of the description languages in Web service orchestration,BPEL is used to state the activities of business process and the controls to activities.There are some syntax structures like common program languages in BPEL which can demonstrate the controls to business process,e.g.sequence, branch and loop.Specialized structures are designed for business process to meet the requirement both from IT and business domain.However,it brings some puzzles in verifying BPEL programs. BPEL is not an executable language,while with prolix and complicated codes it usually suffers from ambiguity,inconsistency and incompleteness.It is necessary to improve the mechanism of verifying BPEL program in order to reinforce the robustness.This paper deals with the research on the Verification method of BPEL program based on model checking technology,and presents a verifying model based on mealy automata - BVM(BPEL Verification Machine) which is adopted to construct a method aimed at verifying the program properties.By finding out the required BVM model M from the known BPEL source code and pending properties P from user specification,the paper designs and implements an engine in model checker NuSMV to verify whether M satisfy P.The case study shows that the above methods are able to verify the BPEL programs include compensation,filling up a deficiency of current methods.