A Refinement Checking Method of Web Services Composition

As a new kind of distributed computing paradigm, web services have been paid more and more attention in recent years. The idea of software as a service is accepted by more and more people. Regarding the web services composition process as a software development process, in this paper we consider web services composition from the view of software architecture, which can control the layout of the whole system. In order to analyze web services composition from the global perspective, we use a software architecture description language based on temporal logic to specify web services composition behavior and property. This also cover the shortage of semantic representations of BPEL, then we transform the temporal logic description to timed-automata, and apply refinement checking to verify the correctness of web service composition, meanwhile the feasibility is illustrated by a ticket booking system.