A Modeling And Verification Method For Web Services Based On VerICS

The emergence and rapid development of service-oriented architecture makes the Web service becoming a very important role in the process of software development.A single Web service can’t satisfy increasingly complex requirements of users because of it’s limited functions. In most situations, we need to combine the existing single Web services to achieve our target requirements. However, the credibility of Web service composition which includes correctness, security, reliability and so on, is threatened easily because of the characteristics of the service itself, open and volatile operating development of the Internet or different development model of services. It is necessary to verify the credibility of the Web service composition in order to ensure the Web service composition to run correctly. Model checking technique, a formal method, is always used to model the operation process of a Web service composition and verify the credibility of a Web service composition.Aiming at the limitation that the traditional model checking method can’t verify the relevant properties of Web service composition with time constraints, we propose a modeling and verification method for Web service composition based on Ver ICS.This method can verify the timeliness of a Web service composition with time constrains. It can also verify the temporal epistemic logic specification of a Web service composition.Our work is mainly reflected in the following aspects:(1)We propose a method in which Web services business process execution language BPEL is extended with time constraint attributes, so that we can use VerICS to verify the relevant properties of Web service composition with time constraints.(2)BPEL I/O state transition system BIOSTS is proposed. BIOSTS is described as a “middle bridge” between BPEL and input language IL of VerICS. We also establish BIOSTS model for BPEL basic activities and structured activities which are foundation of realizing the automation of the BPEL process.(3)We put forward a series of algorithms BP2 BS and others for translating the BPEL process or it’s structured activities into BIOSTS formal model. Thesealgorithms realize the formal modeling of BPEL process automatically, and they Also improve the degree of automation of Web services.(4)We also propose the algorithm BS2 IL for translating the BIOSTS into VerICS input language IL.The algorithm takes both the characteristics of formal model BIOSTS and the characteristics of IL grammar into consideration, and it makes every element of BIOSTS map to each component of IL language. The algorithm realizes the transformation from BIOSTS to IL automatically. This algorithm avoid many tedious manual operations and implement model checking of BPEL process automatically;(5)We apply VerICS to the verification of the temporal and epistemic specification in Virtual Travel Agency(VTA for short).We can judge the Web service composition satisfy the target needs or not according to the results of VerICS. The results of this experiment show that the modeling and verification method for Web service composition we proposed is feasible and effective.