Research On Formal Verification Of Web Services Composition And Method Of Visualization

Web service is used to realize the interoperation of application program on Internet. It has been used as an integration technology of distributed network application with great development potential. The study on service composition not only realizes industry service with effective use, but also facilitates the owners of industry service to expand their business and improve their value. Finally the web service combination aims to develop service combination system with high quality and satisfying user’s demands. Whether the system can satisfy user’s demands, it essentially depends on specific behavior executed practically, namely the preciseness of execution behavior determines whether the system can satisfy user’s demands.This paper explored the formalized modeling of service combination,verification and the visualization technology of model driven theoretically and practically. BDL based modeling method facilitates the abstraction of service behaviors correlated with communications and interaction among different web services in the process, and further verify the related characteristics of the established behavior model. Thus it provides theoretical basis to ensure whether the continuing combination service is executed correctly and user’s established target is successfully achieved. On this basis, the study into the behavior model visualization of model driven can help the users with various knowledge backgrounds to master complex behavior interaction of behavior model more directly and accurately, so that the high efficiency and accurate expression can be guaranteed in subsequent development process. The main work is following:(1) WSBM model was set up formal service portfolio behavior based on BPEL4WS. This study presented a modeling method for converting Business Process Execution Language for Web Services (BPEL4WS) to BDL. The use of behavior description language BDL can establish a behavior model offormal, were analyzed and compared by Web service composition system onBPEL4WS is described with BDL model, service concept and elements can becombined with concepts and elements in the BDL model system in thecorresponding. By the concept of transform semantics, formal service portfolio behavior WSBM model set up in this way inherited the basic syntax and semantics of BDL.(2) Construct the simulation execution process of WSBM service composition model for malization behavior. Labeled movement system was used as operational semantics to describe the state evolution process of BDL model. Besides, an equivalent automata model was constructed to describe the moving track of behavior model for semantic test. In construction, starting from initial state, the changes of compound movement expression were traced to obtain the motion event set of normalized model on each state and their mapping relations, the movement trace of the model was finally acquired. Conversion and modeling method of atomic behavior and structural behavior from BPEL4WS to BDL was put forward.(3) The characteristics for web service combination of the formalized model were analyzed and verified based on the behavior model.Due to the web service with high reusable probability, it will suffer a lot in case of any occurring error if a combination service is sent without verification. So the combination process needs to be verified before sending. The formalized modeling and verification method are adopted to express, establish demand model and execute model by grammar and semantic rules. Consequently, the related characteristics satisfied by the target system are verified through the characteristics analysis. This paper studied verification problems of web service combination and proposed a verification method with compatibility based on BDL. The mismatched uncertainties of potential behaviors on combinational logic can be found out using the method prior to service deployment, thereby the robustness of service combination and user’s satisfaction are improved.The accuracy and validity of the method were verified by a practical case.(4) The visualization method was presented by combination behavior interaction of behavior model driven based on web service combination. Through formalized modeling and verification, the correlated characteristics of the system are ensured. However it is difficult for users to understand the demand model by reading and understanding the grammar of model even its semantic rules. The visualization technology can vividly present the model and help users to know and understand the demand model directly. Thus this paper transformed the formalized model of web service in a specific case into visualized animation form of the corresponding combination based on the verification of service combination. After establishing the behavior model of combination service based on BDL, firstly the behavior model was converted into state machine to act as demand animation model by using model conversion. Then this research selected the entity set described by demand visualization based on demands, their corresponding graphics and pictures to show the entities directly. Finally, the status blocks corresponding with the entities were extracted from the model in the demonstration range using a state selection method based on the selected entity set; and the association between the movement of each status block and movement primitive is regarded as visualization description of behavior. When the state machine executes, the driven animation engine calls the correlated movement primitive to control the graphics movement correlated with objects based on the corresponding movement of status blocks, so that the behavior process described by model is presented distinctly.