BPEL Oriented Web Service Composition Modeling And Quantitative Verification

With the continuous development of Web service technology,resulting in a rapid growth in the number of services on the Internet.In general,an atomic service with a single function often fails to respond flexibly to complex requirements,and it becomes more and more important to combine two or more services together.However,in a complex and dynamic network environment,it is difficult to ensure the correctness of the Web service composition process.In addition,the Web service composition process will have some other non-functional property requirements.At the same time,there are probabilistic time information in the Web service composition,so it is extremely important for quantitative verification of Web service composition.In order to achieve quantitative verification of the Web service composition,The main tasks of this paper are as follows:(1)analyzes the basic activities and structured activities as the basic components in the BPEL(business process execution language),and proposes the formalized modeling of the basic activities and structured activities in the BPEL process by WSC-XTS(web service composition-extended transition system).And the algorithm and migration diagram of the BPEL into the WSC-XTS model are given in this paper.The algorithm gives the specific steps of the BPEL to the WSC-XTS model,and the migration graph can represent how to transform the model.(2)The CTMC(Continuous-Time Markov Chain)model in PRISM is used to describe and verify the WSC-XTS.The paper gives some commonly used attribute descriptions.And a correlation analysis is conducted through an example of a service composition that handles purchase orders.(3)When the Web service composition does not meet the demand,it is necessary to reselect the Web service composition according to the counterexample.We compare the two existing counterexample generation algorithms KSP(K-Shortest Path)and XBF(Extended Breadth-First)algorithm,and propose a XSP(Extended Shortest Path)algorithm which combines the advantages of both of them.XSP algorithm uses the KSP algorithm to generate a diagnostic path,and uses the graph in the XBF algorithm to store the diagnostic path.This algorithm avoids the shortcomings of the KSP algorithm to enumerate the path and to produce the suboptimal path in the XBF algorithm.