This work is based on three fundamental observations:
Within this general framework, this paper focuses on classes of messages, e.g., in an e-commerce application, the message classes might include, ``invoice'', ``receipt'', ``acknowledgment'', etc. We study the case where the peers are represented by Mealy machines (finite state machines with input and output). The sets of conversations exhibit unexpected behaviors. For example, there exists a composite e-service based on Mealy peers whose set of conversations is not regular nor context free. The set of conversations is shown to be context sensitive. One cause for this is the queuing of messages; we first introduce an operator ``prepone'' in an attempt to simulate queue delays. Although the set of conversations of each composite e-service with Mealy peers is closed under prepone, we illustrate that prepone does not completely capture the queue delay effects. We refine the prepone operator to a ``local'' version which applies to conversations by individual peers. Another aspect of the composite e-service is that decisions are only made by individual e-services possibly with communications with each other. This means that each e-service sees only a ``local'' view of the global conversation. Consequently, Mealy implementations in the composite e-service will also include conversations that whose ``projections'' to individual e-services are consistent with the local e-services. We use projection-join closure to capture such situations. This is reminiscent of the decomposition and join in the relational databases. However, there are still Mealy peers whose set of conversations is not prepone and projection-join closure of any regular language. Therefore we propose conversation specifications as a formalism to define the conversations allowed by an e-service composition.
In this paper we present two technical results concerning the interplay between the local behaviors of Mealy peers and the global behaviors of their compositions. One result shows that for each regular language its local prepone and projection-join closure corresponds to the set of conversations by some Mealy peers effectively constructed from . The second result gives a condition on the shape of a composition which guarantees that the set of conversations that can be realized is the local prepone and projection-join closure of a regular language.
The paper is organized as follows. Section 2 presents a formal framework
for studying composite e-services. Sections 3, 4, and 5 present some preliminary
results that focus on an abstract view of the formal framework based on
the classes of messages passed between e-services and finite state automata;
results here illustrate the unexpected nature of the interplay between
local and global in composite e-services. Section 6 concludes the paper.
A fundamental observation is that an e-service (1) provides services through ``service sessions'' and (2) reacts to ``events'' during a session, although the implementation of an e-service may be very complex. Fig.1 illustrates an abstraction of an e-service (called here a peer) as a program that processes the input events from an input queue and determines the response if any (in the form of outgoing events) and termination. For the present we make no assumptions about the computational power of a peer, nor how much storage it has.
Events form the enabling mechanism in composing e-services. In this paper, we focus on an important kind of event--``messages'' between the individual e-services. Messages are organized into a finite collection of ``message classes'' (each message is in exactly one class). Message classes can be used to simplify and organize the specification of actions. A message class consists of a name and a finite set of attributes. A message of a class consists of an identifier of an e-service enactment (session), an identifier for the message itself, the sender, the receiver, and a function mapping each attribute of to a value (of appropriate type).
``11-1-2002'', ``$2,500'', 43-56483, .
Roughly, a peer implementation can be viewed as a ``program'' that decides, based on the received messages and the messages already sent, if a new message should be sent, and/or if the session should terminate. AZTEC [17] classifies e-services into two types: (1) Discrete e-services that do not allow interactions during the service, and (2) Interactive e-services that allow arbitrarily many interactions during the service, such as VCR type of controls during a session. A discrete e-service can be viewed as a service whose output depends only on the original input, while in an interactive e-service inputs can be unpredictable and the e-service reacts to input as they occur. AZTEC [17] emphasizes the importance of interactive e-services in the context of telecommunications applications, but they are also relevant in the context of e-commerce. A single occurrence of ordering a book can be modeled using discrete e-services. But in many cases a vendor wants to track the entire relationship with a customer, and perhaps modify customer treatment accordingly (e.g., frequent flier programs). In this case, some of the e-services used are fundamentally long-running and interactive.
We now start to lay the foundation for a formal study of global behavior of composite e-services. The first step is to formalize the notion of a ``schema'' for a composite e-service.
DEFINITION. An e-composition schema (ec-schema) is a triple , where is a finite set of message classes, a finite set of (abstract) peers (e-services), and is a finite set of one-way communication channels, ^{1} i.e., is a finite set of triples such that, , , and for each pair of channels and in, if and , then ; otherwise, .
Let
be an ec-schema. In a channel ,
is the sender and
the receiver of the channel, and only messages in classes in
are allowed to be sent on the channel. We fix the following notations in
the remainder of the paper. For each peer,
denote the sets of (classes whose) messages may be put in the input queue
of
and in the output by,
resp. i.e.,
and
. Finally, let
.
DEFINITION. Let
be an ec-schema and .
A (peer) implementation of
is a computable function which maps a sequence of incoming and outgoing
messages (a word over)
to .
An
ec-implementation of
is a mapping
such that for each,
is an implementation of .
The e-service implementation described above is very general. In the following sections, we introduce a specific type of implementations based on Mealy machines and study the global behavior of a composition and the local behaviors of individual e-services.
In the technical discussions, we consider a special family of implementations called ``Mealy implementations'' (or ``Mealy peers'') based on Mealy machines [22]. There are two primary reasons. First, Mealy machines are a variant of finite state machines and seem suitable for modeling e-services. Second, Mealy implementations make it possible to analyze some aspects of the global behavior. As we shall see, our preliminary results suggest a ``top-down'' approach to e-service compositions and raise many interesting questions.
Let
denote the empty string. If
is an alphabet, we define
(the extended alphabet with the empty string).
DEFINITION. Let
be an ec-schema and .
A Mealy implementation of
is a (nondeterministic) Mealy machine
where
is a finite set of states,
the starting state,
a set of final states,
and
are derived from
as before, and
is a transition function such that it either consumes a nonempty input
or produces a nonempty output but not both (empty moves are allowed). An
ec-implementation is Mealy if its peer implementations are all Mealy.
A Mealy implementation of a peer reacts to messages according to their
classes while ignoring the contents. Although Mealy implementations are
finite state machines, they can model e-services in many applications nicely.
This is illustrated by Example 2.1, where the message
classes effectively dictate the actions to be taken by each server and
consequently the responses.
Example 3.1Fig. 4 shows a family of Mealy peer implementations for the warehouse example of Example 2.1. (The implementation for Warehouse2 is analogous to the implementation for Warehouse1.) In these diagrams, we use ``'' (``'') to denote sending (receiving) a message from class . It can be verified that the ec-language generated by this Mealy implementation
We now define the notion to capture the computation of ec-implementations.
Let be an ec-schema where . Suppose that is a Mealy ec-implementation for . An ec-configuration of is a -tuple of the form
For ec-configurations and , we say that if one of the following three conditions holds:
DEFINITION. Let be an ec-schema where and a Mealy ec-implementation of. A word over is a (halting) conversation for if
While Mealy peers resemble I/O automata [23] and interface automata [6,5], the communication model is different. In our composition model, Mealy peers communicate asynchronously. Specifically, a queue is used for each peer to buffer messages that were received but not processed so far. In approaches such as CSP [21], and I/O and interface automata, the communicating processes execute a send and a corresponding receive action synchronously. This makes Mealy implementations significantly different from the communication model used in approaches such as CSP, I/O and interface automata. Our model of Mealy peers is similar to Communicating Finite State Machines defined in [12]. However, in our model messages are exchanged through a common medium and then stored in the queues of the peers, whereas in [12] each pair of communicating machines use isolated communication channels. Our goal is to investigate the global behavior of the protocol by investigating the possible configurations of the watcher which models the behavior of this common medium. Finally, [10] studies ``quasi-realtime'' automata with queues. These are single automata with one or more queues, where an automaton can write a bounded number of letters on the queue(s) for each input letter read. In [10] the input and queue alphabets maybe different; in our framework the alphabets are identical.
Example 4.1Figure 5 shows a Mealy implementation with two peers. Peer sends requests while responds with a message for each message. Since messages can be temporarily stored in the queue of , the ec-language consists of words with the same number of 's as's and each has a corresponding that occurs somewhere beforehand. Note that . Therefore is not regular (but it is context free).
Using an idea similar to that in Example 4.1,
one can easily construct a Mealy ec-implementation whose ec-language is
not regular nor context free but context sensitive. However,
THEOREM 4.2Let be an arbitrary Mealy ec-implementation of any ec-schema.
We now return to the phenomenon exposed by Example 4.1. A close examination indicates that the primary reason for this behavior is that the message queue of a peer serves as a ``buffer'' for the input: while conversations monitor the arrival of messages at the queues the messages may not be read right away. To understand this effect, we introduce the operator PREPONE on the alphabet of an ec-schema as follows.
Let be a word in, where is in the set of messages on the channel from to and in the set of messages on the channel from to. If either (1) and are disjoint, or (2) and , then includes the word . Intuitively, the operator PREPONE allows two messages in a conversation to be swapped if the senders and receivers are completely disjoint, or a later message to a peer can arrive in the queue earlier than an outgoing message from the peer since the outgoing message cannot depend on a later arrived message.
It is important to note that PREPONE applies to the global sequence of messages observed by the watcher. We will exhibit later in the section that is not strong enough to characterize the behaviors of Mealy ec-implementations.
If is a language over, we define to be the smallest language that contains and is closed under . The following interesting property holds for .
LEMMA 4.3For each Mealy ec-implementation of an ec-schema, (closure under PREPONE).
Since the set of context-sensitive languages does not have the closure property, the following holds.
COROLLARY 4.4 There is a context-sensitive language such that for any Mealy ec-implementation .
The second property of ec-languages concerns with combining ``local views'' of conversations into global conversations, this is reminiscent of the join operator in the relational database model.
Example 4.5 Consider an ec-schema that has four peers , and three channels , , and . Is there any Mealy ec-implementation that generates the regular language ? Note that the peer groups and are in fact independent; there is no communication possible between them. It can be shown that any Mealy ec-implementation that generates also generates each of , and.
The above example suggests that if two global behaviors have exactly the same local views, they are indistinguishable. We formalize this concept below.
The definition of given for Mealy ec-implementations has the effect of generating words. We now define a kind of converse for individual Mealy peer implementations, which has the effect of consuming words. Let be a Mealy implementation for a peer . Let . A local (l-)configuration of is is a triple . In an l-configuration , is the current state of the peer , is the sequence of messages in the input queue of , is a sequence of ``future messages'' including the incoming messages not yet in the queue of and the messages to be sent out by (i.e., represents the remaining portion of a conversation projected to the messages visible to ).
We define for a pair of l-configurations and if one of the following holds for some and some :
Let . A local (l-)run of is a (finite) sequence of l-configurations () such that for . A word in the language is a (halting) execution of if for some (final) state .
For word and peer, let denote the restriction of to the set ().
LEMMA 4.6Let be a Mealy ec-implementation of an ec-schema . Let. If for each peer, is a (halting) execution of , then is a (halting) conversation for . The converse is also true.
PROOF (Sketch) Let be a word over . We outline a proof for the direction ``if projection of to each peer is a (halting) execution, then is a (halting) conversation''. The converse is trivial.
Without loss of generality, we assume that the ec-schema has peers . Since for each peer , the projection is a local execution, there exists a corresponding l-run for . We show that is a (halting) conversation by constructing an ec-run that simulates each . The construction has phases. Phase 0 is the initialization phase where we simulate in the global ec-run the initial-moves of each until it advances to an l-configuration that is ready to do a send-message action or an enqueue-message action. Then in each phase , we simulate the transmission of message, where only the sender and receiver of are involved. We start with the sender of . We execute the send- action, and its follow-up actions such as-moves and consume-message actions, until we encounter an enqueue-message or send-message action on a message where . Then we turn to the receiver of , execute the enqueue- action and the follow-up actions until an action related to a later message is reached.
We can prove the correctness of the above process by an induction on the number of phases. Specifically, it can be shown that (1) after the completion of phase , the l-run of each peer has been simulated right before the last l-configuration which contains the future messages , and (2) the simulation can always proceed. It follows that the last global ec-configuration is consistent with the last l-configuration for every .
Now we define the join operator which takes as input a sequence of languages where each is a set of words for peer , and is the number of peers in the ec-schema. It returns a language over .
LEMMA 4.7For each Mealy ec-implementation of an ec-schema with peers, .
Given a language over , let denote the minimal superset of that is closed under and. From Lemmas 4.3 and 4.7, we can infer that for each Mealy ec-implementation , the following holds:
Essentially, this states that any Mealy ec-implementation that generates the behavior set must also generate its closure. One interesting question is given, is it always possible to synthesize a Mealy ec-implementation such that ?
The answer unfortunately is negative. Consider the following example.
Example 4.8Shown in Figure 6 is an ec-schema that consists of three peers and three channels. The language , and it is obvious that .
If is recognized by, consider the scenario that takes the local execution path and takes the path . It is not hard to see that is a conversation since sends while having in its input queue. Thus .
One reason that the cannot be the set of conversations by some Mealy ec-implementation is that applying to (global) conversations is too weak. Consider the projection of the conversation on in Example 4.8. If it is not accepted by , it must be the result of applying one or more ``prepone'' like swaps on an accepted word. For example, swap the sequence of output message and input message, we get from . Note that this type of swap differs from since the former is applied locally instead of globally. Secondly, we allow the receiver of the first message and the sender of the second message to be the same, which is forbidden in . We call this type of swap a local prepone defined below. For each peer , if
Using local prepone operators and , we define for each language over the ec-closure of as follows.
Now let us consider the inverse of the synthesis problem. Given a Mealy ec-implementation , can we find a regular language as its core? The following example provides a negative answer.
Example 4.9Consider an ec-schema shown in Figure 7 consisting of 3 Mealy peers, and 3 channels. Intuitively, sends, say messages of class , to, a message to , and then halt; responds to each message by send a message to ; expects at the beginning and then consumes all messages. It is not hard to see that the only way for to halt is for to keep all messages in its queue till after sends to . Thus is its ec-language. It can be shown that each subset of satisfies the following property
PROPOSITION 4.10There exists a Mealy ec-implementation such that for each regular language .
DEFINITION. Let be an ec-schema. A conversation specification for is a specification (e.g., by regular expression, finite state automaton, intertask dependencies, etc.) of a language over . The language specified by is denoted. Let be a conversation specification. An ec-implementation of conforms to if is contained in the ec-closure of, and realizes if the ec-closure of.
We are interested in the following question: For a conversation specification ,
can we construct a (Mealy) ec-implementation
that realizes ?
The main result of the section is to show that the answer is positive.
THEOREM 5.1For every regular language , one can effectively construct a Mealy ec-implementation that realizes.
We now discuss the proof of the above theorem. The proof consists of the following main steps. First, we construct a finite state automaton that accepts. From , we construct, for each peer , a Mealy implementation . This construction is essentially a projection: replace all edges in that are irrelevant to channels connected to by moves, change edges of messages sent to as input, and finally edges of messages sent by as output. To prove that the composition of the implementation generates exactly, we have to show that
By Lemma 4.6, a word is contained in if and only if for each peer , is a halting execution. Combined with the fact that , we can infer that to prove Equation (1), it suffices to show the following property (Lemma 5.2).LEMMA 5.2Let be a Mealy implementation for peer . A word is a halting execution if and only if .
PROOF (Sketch) We prove by induction that is a sufficient condition for being a local execution. In the induction proof it suffices to show the claim that if a word is contained in for some local execution , is also a local execution. The proof of the claim is straightforward, because we can always construct an l-run for by modifying the l-run of.
Next we show that is a necessary condition. We show that for any halting execution, we can always find such that , by applying ``reverse prepone'' procedure finitely many times. We briefly describe the procedure below. Consider the l-run of the local execution . Let be the first send-message action such that input queue is not empty, i.e., . It is not hard to show that can be written as , where includes those eagerly processed messages before the arrival of any message in. Now let , we can show that and is also a halting execution. Repeat the above procedure, until we cannot find a send-message action with a non-empty queue, then we get a list where, , and for each , . The last word is the we are looking for.
Lemma 5.2 implies the following corollary.
COROLLARY 5.3Given a Mealy ec-implementation for an ec-schema . The conversation set generated by is the following:
DEFINITION. Let be an ec-schema. Let be the non-directed graph where
PROPOSITION 5.4 Let be a tree-based ec-schema and a Mealy implementation for . Then for some regular language .
PROOF (Sketch) First we extend the notion of conversation to indicate when messages are read from an input queue, in addition to when messages are written onto the input queue. Let . A read-augmented conversation of implementation is a word over the alphabet that corresponds to a computation over , where each occurrence of a letter corresponds to a time when letter was read from a peer's input queue. Given such a , denotes the projection of onto the alphabet.
Now let and be as in the statement of the proposition. A key lemma is to show that if is a read-augmented conversation of corresponding to a halting computation, then there is a read-augmented conversation of such that and has the immediate read property, that is, for each occurrence of occurring in there is an occurrence of immediately following in . The key idea of the proof is that since is tree-based, entire blocks of a computation occurring in one ``part'' of the tree (if partitioned by removing ) can be ``delayed'' or ``accelerated'' so that a message is not put onto the queue of peer until is ready to read that message.
From the above key lemma, we learn that each halting conversation is contained in for some word , where satisfies the following condition: for each peer, the projection is accepted by. Let , it is not hard to show that is a regular language, and . Let be the Mealy ec-implementation generated from the projection of to each peer. It is easy to infer that . Combined with the known fact that
Acknowledgment: Bultan was supported in part by NSF grant CCR-9970976 and NSF Career award CCR-9984822; Fu was partially supported by NSF grant IIS-0101134 and NSF Career award CCR-9984822; Su was also supported in part by NSF grants IIS-0101134 and IIS-9817432.
[2] The 3rd generation partnership project 2. http://www.3gpp2.org.
[3] A dynamic warehouse for XML data of the Web.IEEE Data Engineering Bulletin, 2001.
[4] Relational transducers for electronic commerce. In Proc. ACM Symp. on Principles of Database Systems, 1998.
[5] Interface automata. In Proceedings of the Ninth Annual Symposium on Foundations of Software Engineering (FSE'01), pages 109-120, 2001.
[6] Interface theories for component-based design. In Proceedings of the First International Workshop on Embedded Software (EMSOFT '01), Lecture Notes in Computer Science 2211. Springer-Verlag, 2001.
[7] The scala home page. http://lamp.epfl.ch/scala/.
[8] DAML-S: Web service description for the semantic web. In Proc. Intl. Semantic Web Conf. (ISWC), July 2002.
[9] Self-coordinated and self-traced composite services with dynamic provider selection. Technical report, University of New South Wales, March 2001. (Available at http://sky.fit.qut.edu.au/ dumas/selfserv.ps.gz).
[10] Quasi-realtime languages.Mathematical Systems Theory, 4(2):97-111, 1970.
[11]Business process execution language for web services (version 1.0).http://www.ibm.com/developerworks/library/ws-bpel, 2002.
[12] On communicating finite-state machines.Journal of the ACM, 30(2):323-342, 1983.
[13] C-commerce virtuality - will it work in the Internet? In Proc. of International Conf. on Advances in Infrastructure for Electronic Business, Science, and Education on the Internet (SSGRR 2000), 2000. (http://www.ssgrr.it/en/ssgrr2000/proceedings.htm).
[14]Proceedings of Workshop on Web Services, E-Business, and the Semantic Web (WES). Springer-Verlag Lecture Notes in Computer Science, number 2512, Toronto, 2002.
[15] Developing e-services for composing e-services. In Proceedings of CAISE 2001, Interlaken, Switzerland, June 2001.
[16] Dynamic and adaptive composition of e-services.Information Systems, 26(3):143-163, 2001.
[17] Beyond discrete e-services: Composing session-oriented services in telecommunications. In Proc. of Workshop on Technologies for E-Services (TES), Rome, Italy, September 2001.
[18] Detecting changes in xml documents. In Proc. Int. Conf. on Data Engineering, 2002.
[19] XL: An XML programming language for web service specification and composition. In Intl. World Wide Web Conf. (WWW2002), 2002.
[20] Types for correct communication in client-server systems. Technical Report CSD-TR-00-07, Department of Computer Science, Royal Holloway, University of London, December 18 2000.
[21] Communicating sequential processes.Communications of the ACM, 21(8):666-677, 1978.
22Introduction to Automata Theory, Languages, and Computation. Addison Wesley, 1979.
[23] Hierarchical correctness proofs for distributed algorithms. In Proc. 6th ACM Symp. Principles of Distributed Computing, pages 137-151, 1987.
[24] Semantic web services. In IEEE Intelligent Systems, March/April 2001.
[25] Simulation, verification and automated composition of web services. In Intl. World Wide Web Conf. (WWW2002), 2002.
[26]Simple object access protocol (soap) 1.1. W3C Note 08, May 2000. (http://www.w3.org/TR/SOAP/).
[27] Session initiation protocol. http://www.sipforum.org.
This document was generated using the LaTeX2HTML translator Version 2002 (1.62)
Copyright © 1993, 1994, 1995, 1996,
Nikos
Drakos, Computer Based Learning Unit, University of Leeds.
Copyright © 1997, 1998, 1999,
Ross
Moore, Mathematics Department, Macquarie University, Sydney.