Research on Web Service Composition Using Probabilistic Abstraction Refinement

The Web service composition (WSC) has been widely used in Service-Oriented Architecture (SOA), which is an effective integration of the distributed and heterogeneous business applications. In contrast to the component-based software, dynamic reconfiguration occurs more frequently in Web services-based software for self-adapting and self-managing their computing capabilities due to the uncertainty of dynamic Internet environment. Verifying these stochastic and nondeterministic behaviors is becoming a hot topic in model checking of Web services (WSs) application engineering. Abstraction refinement technique as an effective approach to alleviating the state explosion problem is particularly suitable for verifying the complex WSC. In this paper, we extend the classical abstraction refinement technique CEGAR (Counterexample-guided abstraction refinement) to make quantitative verification of WSC applicable and efficient. To model WSC, a probabilistic service behavior model (p-SBM) is proposed in form of Markov Decision Process (MDP). To verify WSC, the abstraction is defined by means of a quotient on states with respect to some probabilistic equivalence relation. Once counterexample is produced in the abstract model, verifying whether the counterexample is real or spurious is carried out. Based on the counterexample-guided technique, an iterative abstraction refinement process is performed to progressively refine the abstract model until either there is no abstract counterexample or a valid counterexample is verified. The case studies which are discussed throughout the paper demonstrate that our approach takes advantages than the traditional approaches.