The conversation model captures interactions among the components of a composite web service. A conversation is the global sequence of messages exchanged among the components. We discuss the impact of asynchronous communication on the conversation behavior. It turns out that the conversation behavior is signi cantly different for synchronous and asynchronous communication and demands new techniques for static analysis of composite web services. We outline strategies of model checking service composition for both bottom-up and top-down design approaches.
The success of business-to-consumer applications (e.g. in electronic commerce) over the Internet and the web has already lead to the need of the development of business-to-business applications. Integrating business processes of different organizations through network accessible software components faces several hurdles: (1) Different organizations could use different, incompatible implementation platforms. (2) Organizations may not want to share the internal details of their applications which can hinder integration. (3) No organization would want their application to get stuck due to pauses in availability of a software component residing in another organization.
Web services standards and technologies provide a framework for integration and interoperability of web accessible software applications by addressing these challenges as follows:
Standardized data transmission via XML enables interaction among software components that are implemented using different platforms. Loose coupling of interacting services through standardized interfaces such as Web Service De nition Language (WSDL) provides a clear separation between the internals of an application and its interface visible to outside organizations.
Use of asynchronous communication to lessen the effects of pauses in availability of other services and slow data transmission through the Internet.
In this short paper, we focus on asynchronous communication and its
effects on the interaction behavior of composite web services. In asynchronous
communication when a message is sent, it is inserted into a FIFO message
queue, and the receiver consumes the message when it reaches to the front of
the queue. This type of asynchronous communication is supported by
message delivery platforms such as Java Message Service (JMS) [
We focus on the behavior of composite web services that usually consist of many interacting component services. We consider two design approaches: bottom-up that starts from developing (identifying through discovery) component services, and top-down that derives the individual services from the speci cation for the composite service. A main goal is to analyze composite web services (obtained either through bottom-up or top-down) against properties speci ed in some logic language.
A composite web service consists of a set of peers (or component services)
which communicate with each other using asynchronous messages. The
messages exchanged among the peers are XML documents. This model ts nicely
with the existing web service standards such as WSDL, BPEL (Business
Process Execution Language for Web Services), and WSCL (Web Service
Conversation Language [
A promising component of the web services framework that facilitates
integration and interoperability is the conversation model [
There are two fundamentally distinguished approaches to composite web service design:
In the bottom-up approach each peer participating in the web service composition is speci ed separately (as a state machine) and then the composed system can be studied by analyzing the combined behaviors of these individual peer speci cations.
In the top-down approach the desired global behavior is speci ed rst and the detailed peer implementations are left blank initially. Any peer implementation that conforms to the desired global behavior is an acceptable implementation of a peer.
Conversation protocols are a top-down speci cation for composite web services. A conversation protocol is a nite state machine that speci es the desired set of conversations for a composite web service. A composite web service realizes a conversation protocol if the conversations accepted by the conversation protocol are exactly those generated by the composite web service. In other words, if the conversation sets of a conversation protocol and a composite web service are equal then we say that the composite web service realizes the conversation protocol.
A conversation protocol is realizable if there exists a composite web service
that realizes it. It is known that not every conversation protocol is realizable;
however, if a conversation protocol is realizable then it is realizable by its
projections to each peer [
On the other hand, if we start from the peer implementation as in the
bottomup approach, the set of all possible conversations may not be identical to any
conversation protocols. The reason is that the conversation sets of some
composite web services may not be regular nor even context-free [
Given a composite web service where each peer is speci ed as a state
machine, an interesting problem is to verify if the conversations generated by the
composite web service satisfy certain properties. For example, it would be
very useful to verify properties such as a payment message is always
eventually followed by a receipt message. Such properties can be speci ed in Linear
Temporal Logic (LTL) [
Model checking [
Known results indicate that automated veri cation of conversation behavior
is not always possible in the presence of asynchronous communication with
unbounded queues [
The synchronizability and realizability results lead to following veri cation strategies. For example, in the case of bottom-up speci cations (design), the analysis strategy consists of the following steps: 1 We rst check the synchronizability of the composite web service. 2 If the web service is synchronizable we verify the LTL properties on its conversations. (In this case the results we obtain hold for all conversations generated by the composite web service even in the presence of unbounded message queues.) 3 If the web service is not synchronizable we verify the LTL properties on its conversations by bounding the sizes of FIFO queues. In this case the veri cation results we obtain are guaranteed as long as the message queues remain within the speci ed bound. However if we nd that a property is violated, then a counter-example generated using the model checking techniques provide a concrete counter-example demonstrating the error.
A slightly different 3-step strategy is developed for top-down speci cation.
The synchronizability and realizability analysis have been implemented as
a part of the Web Service Analysis Tool (WSAT) [
Conversation model provides a promising framework for analyzing interactions among web services. Asynchronous communication can effect the conversation behavior and if unbounded queues are used to model asynchronous communication then the veri cation of temporal logic properties of conversations becomes undecidable. We outlined two approaches to overcome the dif culties that arise in veri cation due to asynchronous communication. Synchronizability analysis identi es web service compositions for which the conversation behavior does not change when synchronous communication is replaced with asynchronous communication. This enables us to verify properties of conversations using the simpler synchronous communication semantics without giving up the bene ts of asynchronous communication. On the other hand realizability analysis helps us to make sure that for top-down web service speci cations asynchronous communication does not create unintended behaviors. This enables us to verify the conversation properties at a higher level of abstraction without considering the asynchronous communication semantics.