An Automatic Model Checking Approach To Composite Web Services

Today, Web services are widely distributed over the Internet, the tasks of composite Web services are solved through the interactions between these Web services involved. However, in the interaction process, it is possible that some unexpected or "not normal" information interactions will occur, which may cause some incorrect result generated and seriously lower the quality and robustness of a system. Therefore, to ensure Web services can provide correct function, it is necessary to apply formal verification techniques, such as model checking, to the verification of the temporal and epistemic specifications of Web service composition, which has become a hot area of research on formal verification domain. To the best of our knowledge, such formal verification techniques for Web service composition are in the initial research stage, and the entire verification process is not automatic, there are a lot of manual operations in during the process, especially in the modeling stage. Therefore, in order to make the Web services verification process more automatic, we propose a series of algorithms for translating the BPEL flow of Web service composition into the input code of MCTK, a symbolic model checker for temporal epistemic logic. Finally, by these algorithms, we model and verify VTA and STS protocols via MCTK, the state transition diagram of Loan Approval Service is automatically constructed. Some research achivements of this dissertation are as follows:(1) We introduce the concept of transition seven-tuples to represent the state transition relation. Based on the semantics of BPEL activities, we establish the mapping from BPEL activities to transition seven-tuples. It is the foundation for the automatic verification of BPEL flow.(2) We propose the algorithm B2T and F2T for translating the control flow,data flow of BPEL into transition seven-tuples. These algorithms will automatically convert BPEL process into a set of transition seven-tuples, such that we can convert the composite work flow into a multi-branch state transition diagram.(3) We also propose the algorithm T2M to automatically generate the MCTK input code according to the set of transition seven-tuples. In order to detect the control flow automatically, we design T2M algorithm to automatically generate the code according to the relation of transition seven-tuples in a set. It also considers the characteristics of MCTK. This algorithm avoids many tedious manual operations and implement automatic detection of control flow;(4) We apply MCTK to the verification of the temporal and epistemic specifications in VTA and feature interactions in STS. The experiments results show the correctness and effectiveness of the proposed approach. Meanwhile, a state transition diagram of loan service agreement is automatically built by algorithm F2T, which is useful for the next step of verification.