Keywords

1 Introduction

Web services are self contained, self-describing modular applications that can be published, located, and invoked across the web [1]. Since Web services interact with each other through messages (synchronous and asynchronous), concurrency related bugs and/or inconsistency problems are possible in the interaction patterns (communication patterns). In order to overcome the problem, Web service interaction verification is required.

Classical testing techniques are inadequate to verify the interaction among services [2, 3]. A Web service interaction scenario resembles with reactive and concurrent systems, with component-based systems [4, 5], and with multi-agent systems [6] up to a certain extent. Therefore, various Web service interaction modeling and verification techniques are proposed on the basis of these approaches [6, 7]. However, composition among services tangles the task of verification as it poses unique primitive verification requirements that are not covered by either classical tests or other verification approaches.

Many efficient and industry wide accepted formal verification tools are available that could verify Web service interaction. However, transformation of a service interaction scenario into an input model for any existing verification tool may loose the architectural originality and significant native primitive notions, thus, restricting the verifiable properties (requirements). In this article, we characterize the model of Web service interaction for verification, a novel effort towards establishing Web service interaction verification model.

The rest of the article is structured as follows. Section 2 investigates fundamental characteristics of a Web service interaction model. We study the appropriateness and effectiveness of model checking and module checking in Sect. 3. Section 4 provides conclusion and future directions.

2 Primitive Characteristics of Web Service Interaction Model

In this section, primitive characteristics of the Web service interaction model are discussed as follows.

2.1 Modular and Hierarchical Architecture

All Web services basically fall into two categories: either basic or composite. A basic Web service does not take help of other Web services to accomplish the job whereas a composite Web service does.

Modular architecture of Web services interaction model refers to the design of a system composed of independent Web services that could interact with each other. The advantage of the modular architecture is that a module could be added or substituted with another suitable module without affecting the rest of the system.

Hierarchical architecture of Web services interaction model comes in the existence only when a composite service comes in the existence. A composite service depends on the other basic or composite services. A composite service is a higher level abstraction and basic Web services are lowest level abstraction. Web service interaction possess hierarchical architecture but nesting of Web services are not allowed. Indeed, nesting of Web services does not make any sense as basic Web services work as independent modules.

Therefore, Web service interaction model has both shades of hierarchical and modular architectural archetype. It requires modeling a Web service in such a way that it preserves its identity and supports composite services at a time. Consequently, a Web service can serve as an independent module and can serve as an building block of a composite service.

2.2 Open System

Each basic Web service works as an independent module that fundamentally yields an open system from a verification perspective. An open system is one which is designed to interact with an environment [8]. A web service cannot anticipate all behaviors of its interacting partner in advance, thus enabling the open system phenomenon. In order to be able to model the open system, environment modeling is inevitable. Classical modeling approaches and many other new verification techniques does not support environment modeling. They typically apply to closed systems whose behavior is fully specified.

2.3 Trace Modeling

Informally, a trace (in the context of Web services) is a linear, unidirectional Web service composition workflow path in which each node represents a Web service and the directed edges indicate the flow from one service to another. Trace modeling and computation are among the most primitive modeling requirements for Web service interaction as the computation of trace related phenomenons (such as trace inclusion, trace crossing, and trace merging) reduce the time and space complexity for verification.

Formal definition of a Web service trace is given as follows.

Definition 1

(Trace) A trace is a tuple \(\mathcal{T} = (\mathcal{W},I,w_{i} ,w_{n} )\), where \(\mathcal{W} = \{ w_{1} , \cdots ,w_{m} \}\) is a finite set of the Web services, \(I:\mathcal{W} \to \mathcal{W}\) is an invocation function such that w i Iw j if and only if w i invokes w j , \(w_{i} \in \mathcal{W}\) is a service from which trace generation begin and \(\nexists w_{j} \in \mathcal{W}:w_{j} Iw_{i}\), and \(w_{n} \in \mathcal{W}\) is a service on which trace ends up and \(\nexists w_{j} \in \mathcal{W}:w_{n} Iw_{j}\).

Let w i be a Web service then \(\mathcal{T}_{{w_{i} }}\) represents a set which contains all the traces generated by the service w i . The concept of trace is utilized mainly while studying behavioral equivalence of services.

2.4 Asynchronous Messaging

A Web service consists ports and a port consists sets of input and output messages. Messages consisting activities are unit of interaction. There are two principal messaging models used in Web services namely synchronous and asynchronous model. The two Web service messaging models are distinguished by their way of request-response operation handling mechanism.

Synchronous messaging and asynchronous messaging among less number of services can be handled in a fair manner without much complexity. If involved number of services are high, asynchronous messaging complicates the verification process.

2.5 Recursive Composition

Composition and recursive composition are fundamental characteristics of Web service interaction model. Composition of services is aggregation of facilities provided by services. Recursive composition refers recursive aggregation of services. The difference between recursive composition and non-recursive composition is explained as follows.

Let 〈A, B〉 represents the knowledge that a Web service A is composed of a Web service B. Let {〈A, B〉, 〈B, C〉, 〈C, D〉} represents a composition scenario. If a composition dependency holds among tuples such as 〈A, B〉 depends upon 〈B, C〉 and 〈B, C〉 depends upon 〈C, D〉 then it forms a recursive composition scenario otherwise non-recursive composition.

2.6 Dynamic Reconfiguration

There are two crucial factors that make consideration of dynamic reconfiguration in the case of Web service inevitable. First, a Web service resembles a module (a basic Web service resembles an independent module whereas a composite Web service resembles a dependent module). Second, dynamic availability of services. Web services are accessible through the Web and a Web service could become unavailable/removed at any time or a new Web service could be introduced at any time. Ethically, a composition designer or verifier must be ready for substitution, replacement, and introduction of services. Introduction or unavailability of a service could make complete chaos if not handled properly. Automatic dynamic service composition is a rapidly emerging paradigm and research topic that is based on dynamic reconfiguration phenomenon.

2.7 Hierarchical Concurrency

Classical model-based verification approaches do not consider hierarchy among Web services while verifying the interaction. They keep transmitting all variables that are being considered for verification through every state in their state transition diagram. All variables need not be considered at a time. A hierarchy must be found among services and must be considered in verification process. We explain a hierarchical concurrency scenario among Web services as follows.

Let 〈A, B〉 represents the knowledge that A is composed of B and 〈A, B〉 → 〈B, C〉 represents the knowledge that 〈A, B〉 depends upon 〈B, C〉. Let us consider the following scenario

$$\begin{array}{*{20}c} {\langle A,B\rangle } & {} & {} & {} & {\langle I,J\rangle } \\ \downarrow & {} & {} & {} & \downarrow \\ {\langle B,C\rangle } & \leftarrow & { (B,J) } & \to & {\langle J,K\rangle } \\ \downarrow & {} & {} & {} & \downarrow \\ {\langle C,D\rangle } & {} & {} & {} & {\langle K,L\rangle } \\ \end{array}$$

Consider that concurrency has to be resolved between services B and J for a given specification. If 〈B, C〉 and 〈J, K〉 do not affect 〈B, J〉 regarding concurrency then concurrency will be resolved between B and J only (B and J are first level services). No need to involve the services C and K (C and K are second level services). If the concurrency is not resolved at first level then only second level services will be considered. Again, if second level services are also not sufficient to resolve the concurrency, third level services (D and L are third level services) will be considered.

We introduce a conceptual term sphere of influence to ease the process of hierarchical concurrency verification in the context of Web service interaction. Sphere of influence is a set of Web services computed for an Web service such that either each member of the set is directly invokable by the center service or invokes the center service. Figure 1 is a pictorial representation of the sphere of influence for a Web service namely WS1. This diagram infers that services WS2, WS3, WS4, and WS5 constitutes the sphere of influence set for the service WS1. Figure 2 is an evolved version of sphere of influence depicted in Fig. 1. Sphere of influence serves as a basic model to verify hierarchical concurrency.

Fig. 1
figure 1

Sphere of influence for a Web service WS1

Full size image
Fig. 2
figure 2

Evolved version of sphere of influence depicted in Fig. 1

Full size image

2.8 Verification of Adversarial Specification

Classical temporal logics such as linear temporal logic (LTL) and computation tree logic (CTL) are unable to specify collaborative as well as adversarial interactions among different Web services. Alternating Temporal Logic (ATL) [8] is designed to write requirements of open system [8] and is able to express collaborative as well as adversarial interaction specifications. ATL models each Web service as an agent. Let Σ be a set of agents corresponding to different Web services, one of which may correspond to the external environment. Then, the logic ATL admits formulas of the form \(\left\langle {\left\langle A \right\rangle } \right\rangle \diamondsuit p\), where p is a state predicate and A is a subset of agents. The formula \(\left\langle {\left\langle A \right\rangle } \right\rangle \diamondsuit p\) means that the agents in the set A can cooperate to reach a p-state no matter how the remaining agents resolve their choices.

3 Web Service Interaction Verification

In this section, we study and compare two different model-based formal verification approaches that are suitable for service interaction verification: model checking and module checking. Further, we study the working mechanisms of their representative tools and its input languages whether there are native language constructs or not to support the desired characteristics discussed earlier in this paper.

Model Checking

Model checking has been widely used as one of the formal techniques for Web service composition and interaction verification [7, 9–12]. In order to be able to model check a Web service interaction scenario, the scenario has to be modeled as an input model of model checking. The transformation of service interaction into an input model of model checking yields a monolithic structure. This transformed structure collapses several significant characteristics such as modular cum hierarchical architecture. Further, monolithic structure increases computation overhead and is not adequate for reasoning. The biggest drawback one faces with model checking is that it does not support open system modeling that is primary requirement for modeling of Web service interaction. Model checking does not have any provision for interface and private variable types. Consequently, a chaos develops among variables in verification.

SPIN [13] and NuSMV [14] are representative tools of model checking. SPIN supports only linear-time temporal logic whereas NuSMV supports both linear-time temporal logic as well as branching-time temporal logic. We study NuSMV (NuSMV 5.0) as a representative tool for model checking.

Module Checking

Module checking is also an model-based formal verification technique. It could be considered as an alternative of model checking. Module checking differs from model checking in various means as follows. From modeling point of view, module checking supports the heterogeneous modeling framework of reactive modules whereas model checking supports unstructured state transition graphs. From specification writing point of view, module checking employs ATL to write specification about the system whereas model checking verifies the specifications written in LTL/CTL. From architecture point of view, module checking facilitates with hierarchical design and verification along with modular design whereas model checking provides only modular designing and verification.

We study MOCHA [15] (jMOCHA 2.0) as a representative tool for module checking. MOCHA is an interactive verification environment that supports a range of compositional and hierarchical verification methodologies.

A comparative analysis between NuSMV 5.0 and jMOCHA 2.0 with respect to investigated characteristics is shown in Table 1.

Table 1 Verification requirements versus verification approaches
Full size table

4 Related Work

To the best of our knowledge, a paper merely focusing on architectural characterization of Web service interaction is not available in literature. However, some of the studied characteristics are discussed individually in articles. Hierarchical architecture of Web services is discussed in [16]. Hnetynka et al. [4] discusses dynamic reconfiguration of Web services and collaboration among them. Roglinger [17] presents a requirements framework for verification. However, the proposed requirements in [17] corresponds to model checking and not characterizing the Web service interaction. Pistore et al. [18] present a requirement model for verification of Web services. However, the authors focus on business requirements not architectural characterization in the paper [18].

We do not find any evidence of Web service interaction verification using module checking tool (jMOCHA) in literature. However, ATL is used for Web service verification along with Petri net in [19].

5 Conclusion and Future Work

On the basis of our study, we conclude that Web service interaction is a modular cum hierarchical architecture. Each Web service works as an open system. Recursive composition is a fundamental characteristic of Web service interaction. And a verification approach for Web services must support hierarchical concurrency verification with adversarial specification facility.

Though module checking is an efficient verification technique for reactive, concurrent, and open systems, it is not widely accepted among industry and academia. Reasons might be lack of popularity and complex specification writing scheme. However, on the basis of our study, we advocate use of module checking rather than model checking for verification of Web services interaction.

There are many improvement suggestions that could be considered as parts of future work. First, we want to investigate hierarchical structure of Web service interaction in more depth. Both verification approaches model checking and module checking do not support recursive composition and dynamic introduction or removal of a service. Therefore, realization of a verification approach based on investigated characteristics and sphere of influence will be our second future work. Discovering all fundamental and advanced verification requirements for Web service interaction is also a part of our future work.