Research On Formal Modeling And Verification Of Data And Time Aware Web Service Compositions

In recent years, with the popularization of internet and the development of electroniccommerce technology, Service-Oriented Computing(SOC) and Service-Oriented Archi-tecture(SOA) are becoming one trend of the next generation software, and are becominga focus in academic and industry. As a new computing model, SOC solves the distributedapplication integration problems effectively in the dynamic and heterogeneousenvironment, and as a new software development model, SOA supports and realizes theintegration and reuse of software assets through the loose coupling method. At present,because of its mature and development, Web service becomes the main way to realizeSOA, and provides the best technical support for SOC.Web service is a self-described and self-contained software component which isbased on network, and it has the characteristics of loose coupling and strongindependence. To standard protocol such as SOAP, WSDL and UDDI as the core, it takesthe service-oriented architecture, besides it realizes the dynamic and openinginteroperability and cross-platform application in the distributed environment. Asindividual Web service has its limitations, through the static or dynamic way tocomposite service components to meet enterprise’s requirements has become aninevitable trend in dynamic electronic commerce area and has affected the way of productdevelopment in service industry.However, network environment has the dynamic, heterogeneous and distributedcharacteristics. How to ensure that the compositions of the Web services can realize theenterprise’s requirements of the functions of business, and at the same times that it won’tappear the situations which are not expected in the process of runtime has become theroot of setting up and running the service oriented architecture system and realizing theenterprise application integration.As an important method to ensure the quality of software, formal technologytechnology provides an effective way to solve the above problems. In this paper, we use the formal technology to research three key scientific problems in area of verification ofweb service compositions which includes web service compositions’ modeling, staticverification and dynamic verification. The main contents as follows: first, we willestablish a formal model for Web service compositions which can depict data-related andtime-related information effectively based on automata theory; In the second, we willpresent a theoretical approach to verify behavior property, data-related property, andtime-related property of Web service compositions. At last, we will establish a faultdiagnosis mechanism to treat the exceptions in the process of runtime of Web servicecompositions based on idea of a general method for monitoring Web servicecompositions. The in-depth research of modeling and verification of service compositionscan improve the credibility of Web service compositions, and promote the developmentof the concepts of service-oriented.