Model checking is a popular formal technique facilitating automatic verification of finite-state transition systems, and it has been applied to almost all of the Web service verification aspects, such as control-flow, data-flow, interaction, time requirements, quality of service, security requirements, etc. However, no systematic literature review focused on model checking of Web services is available. Motivated by this fact, in this paper, we systematically review existing research works on model checking based Web service verification appeared during the period of 2002-2017. We present a verification goal based classification of the collected articles, and for each paper, we identify the verification technique, target Web service standard, flavor of the employed model checking technique and tool, and other supplementary techniques, if any. Further, we highlight some of the issues, gaps, key challenges in this area and propose some future directions.

The design principle of composability among Web services is one of the most crucial reasons for the success and popularity of Web services. However, achieving error-free automatic Web service composition is still a challenge. In this paper, we propose a recursive composition based modeling and verification technique for Web service interaction. The application of recursive composition over a Web service with respect to a given set of Web services yields a recursive composition interaction graph (RCIG). In order to capture the requirement specifications of a Web service interaction scenario, we propose recursive composition specification language (RCSL) as a requirement specification language. Further, we employ the proposed RCIG as an interpretation model to interpret the semantics of a RCSL formula. Our verification technique is based on the generation and analysis of all possible interaction patterns. Performance evaluation results, provided in this paper, show that our proposition is implementable for the real world applications. The key advantages of the proposed approach are: (i) it does not require explicit system modeling as in model checking based approaches, (ii) it captures primitive characteristics of Web service interaction patterns, such as recursive composition, sequential and parallel flow, etc, and (iii) it supports automatic composition of services.

Summary Given a composition request, the formation of possible Web Service Composition Graphs (WSCGs) depends on the set of available services. Since the availability of Web services is dynamic, at any time, a new service can join or an existing service can leave the set of available services. A change in the set may bring the structural change in a previously formed WSCG. However, it is not always the case that a structural change in the WSCG brings the semantic change. In this paper, our aim is to verify the compositional equivalence between two WSCGs formed before and after the structural change caused by the change in the set of available services. Our proposed solution is based on an algebraic formalism, and by using the formalism, directed acyclic WSCGs are formed for a given composition request. Then, by using WSCGs, we propose the concept of composition expression and canonical composition expression. On the basis of the proposed concept of canonical composition expression, we verify compositional equivalence between two WSCGs. The advantage of our approach is that it reduces the equivalence verification to the subsumption checking between two algebraic expressions instead of directly using the WSCGs and solving a subgraph matching problem. The proposed mechanism is implemented and evaluated for the exhaustive possibilities in a travel agency case study with respect to a given composition request.