Research on Reachability Verification of Web Service Composition

By Web service composition, the reuse of services is implemented, the quality and the efficiency are increased, and the dynamic evolvement of the user´s requirement is satisfied. Because Web services are autonomous, heterogeneous and dynamic, at the same time, the user´s requirements are becoming more complex gradually, and it is difficult for the user to control them, the error will be introduced inescapably during composing Web services. It is necessary to verify the correctness of Web service composition and to avoid the great economic loss, before the composite service is carried out. In this paper, in order to avoid the shortage of the incidence matrix and the state equation of Petri nets, the relevant algorithms of the reachable marking graph based on Petri nets were presented to verify the reachability of Web service composition, the reachable paths can be given as well. Then, the algorithms were applied to a case. Finally, the conclusion was drawn, and the future work was pointed out.