Abstract: Web service composition validation is very important for improving the efficiency of software development.This paper presented a method based on probabilistic model checking to validate the service composition. We used an extended finite automaton to represent the service composition, and then converted it into a Markov model. A probabilistic model checker PRISM was used to validate the effectiveness of the service composition. Finally, we gave an example to illustrate the feasibility of this method.

Key words: Web service composition, Finite automata, Markov model, Probabilistic model checking