Research On Verification Of Web Service Composition Based On XYZ/ADL

With the development of Internet and electronic commerce, Web service received great attention because of its ability solving interactivity and reusability problems of services in Internet heterogeneous platforms. Compare to traditional distributed computing model, Web service is more abstract and independent, also it has larger granularity. Though function of single Web service is limited, it is difficult to meet the ever-changing business requirements; therefore, it is necessary to composite Web services to provide more powerful functions. Due to web service is often used to describe high level business logics of cross-platform and interorganizations, so it is much more important to guarantee its correctness.Web service composition is the hotspot research in the field of Web services. Many methods are proposed to verify its correctness; however, verification starting from architecture is a new perspective. Refinement checking and model checking are two important formal verification methods, we apply these two methods to verify the correctness of Web service composition in this thesis.Ground on the above ideas and the work have been done of our research group, we study the verification of Web service composition based on the software architecture description language - XYZ/ADL, which based on the temporal logic language XYZ/E. For systems with time constraints, we can express it using XYZ/RE, which is the real time extension of XYZ/E. Considering most Web service with real time characteristics, this thesis analyzes the similarity of the elements of XYZ/RE and timed automata, also corresponding existed mapping rules are improved. For Web service composition systems, using XYZ/ADL to describe behaviors and properties should be satisfied of the Web service composition, then transform both to behavior timed automata and property timed automata, and applying refinement checking to judge if the behavior description satisfied the property. On the other side, map a single Web service XYZ/ADL description to a single timed automata, multi-descriptions of Web services composition to network of timed automata,using CTL expression to represent properties the composite system should satisfy, take the above two as the input of the model checking tool ? UPPAAL, then realize the correctness verification of Web service composition; Last we illustrate the idea above by analyzing an Internet ticketbooking service system and a stock analysis service system.