Research On Termination Verification For Exception Handling In BPEL Process

The adoption of event and interruption mechanism and possible behavior of exception re-thrown in exception handling of BPEL processes often lead to inappro-priate termination of exception handling and failure of proper execution of BPEL pro-cesses. As a result, the termination verification for exception handling is of critical importance, which ensures the correctness of systems consisting of BPEL processes. Comparing to conventional termination verification, more factors should be consider-ed in termination verification for exception handling. However, the current research rarely focuses on whether expected goal can be achieved through exception handling, so a systematical study on termination verification for exception handling in BPEL pr oce-sses is carried on in this thesis.The main research in this paper can be concluded in four aspects.(1) A formal modeling method is proposed for exception handling in BPEL process. Based on the theory of colored petri nets, the behavior relating to termination verification for except ion handling in BPEL processes, such as exception throwing, capturing, handling, re-turning and propagating, is investigated in this method. With the method, a formal model suitable for termination verification can be established, which describes the hierarchy of exception handling in BPEL processes and thus lays a solid foundation for the termination verification.(2) A data reduction technique is presented for variab-les in input messages of BPEL processes. On the basis of the theory of abstract inter-pretation, the technique extends the classical concept of interval abstract domain, ana-lyzes the range of variables with the exception control flow graph on a unified con-cept of interval abstract domain, and finally obtains the reduced value range of variab-les in the input messages. With the data reduction technique, a reduced initial configu-ration is provided to the termination verification for exception handling, and thus re-lieves the explosion of state space.(3) A model checking approach is proposed for ter-mination verification of exception handling. A serial of rules based on ASK-CTL, which is a kind of sequential logic, to determine if exceptions terminate properly are given according to the state space generated by the formal model for exception handl-ing. With the rules, an algorithm and a processing procedure for termination verifica-tion are devised, which provide an effective practical approach for termination verifi-cation.(4) A prototype system is designed for termination verification of exception handling. Based on our previous work, a feature of termination verification for excep-tion handling is integrated to the development platform for exception handling, which includes tools for generation of exception control flow graph, modeling for exception handling, data reduction, and termination verification for exception handling, to pro-vide practical and engineering support for termination verification.