=Paper=
{{Paper
|id=Vol-204/paper-24
|storemode=property
|title=Conformance and Interoperability in Open Enviroments
|pdfUrl=https://ceur-ws.org/Vol-204/P11.pdf
|volume=Vol-204
|dblpUrl=https://dblp.org/rec/conf/woa/BaldoniBMP06
}}
==Conformance and Interoperability in Open Enviroments==
https://ceur-ws.org/Vol-204/P11.pdf
Conformance and Interoperability
in Open Enviroments
Matteo Baldoni, Cristina Baroglio,
Alberto Martelli, and Viviana Patti
Dipartimento di Informatica — Università degli Studi di Torino
C.so Svizzera, 185 — I-10149 Torino (Italy)
Email: {baldoni,baroglio,mrt,patti}@di.unito.it
Abstract— An important issue, in open environments like the interface (although it can refuse the answer). This, however,
web, is guaranteeing the interoperability of a set of services. is not the only possible model of execution. In multi-agent
When the interaction scheme that the services should follow is systems, for instance, an agent sending a request message to
given (e.g. as a choreography or as an interaction protocol), it
becomes possible to verify, before the interaction takes place, another agent cannot be certain that it will ever be answered,
if the interactive behavior of a service (e.g. a BPEL process unless the interaction is ruled by a protocol. The protocol
specification) respects it. This verification is known as “confor- plays, in a way, the role of the public interface: an agent
mance test”. Recently some attempts have been done for defining conforming to a protocol must necessarily answer and must be
conformance tests w.r.t. a protocol but these approaches fail able to handle messages sent by other agents in the context of
in capturing the very nature of interoperability, turning out
to be too restrictive. In this work we give a representation of the protocol itself. The difference between the case of objects
protocol, based on message exchange and on finite state automata, and the case of protocols is that the protocol also defines an
and we focus on those properties that are essential to the “execution context” in which using messages. Therefore, the
verification the interoperability of a set of services. In particular, set of messages that it is possible to use varies depending
we define a conformance test that can guarantee, a priori, the on the point at which the execution has arrived. In a way,
interoperability of a set of services by verifying properties of the
single service against the protocol. This is particularly relevant in the protocol is a dynamic interface that defines messages
open environments, where services are identified and composed in the context of the occurring interaction, thus ruling this
on demand and dynamically, and the system as a whole cannot interaction. On the other hand, the user of an object is not
be analyzed. obliged to use all of the methods offered in the public interface
and it can implement more methods. The same holds when
I. I NTRODUCTION protocols are used to norm the interaction. Generally speaking,
In this work we face the problem of verifying the in- only part of the protocol will be used in an entity’s interaction
teroperability of a set of peers by exploiting an abstract with another and they can understand more messages than
description of the desired interaction. On the one hand, we the one forseen by the protocol. Moreover, we will assume
will have an interaction protocol (possibly expressed by a that the initiative is taken from the entity that plays as a
choreography), capturing the global interaction of a desired sender, which will commit to sending a specific message out
system of services; on the other, we will have a set of service of its set of alternatives. The receiver will simply execute
implementations which should be used to assemble the system. the reception of the message. Of course, the senders should
The protocol is a specification of the desired interaction, send a message that its counterpart can understand. For all
as thus, it might be used for defining several systems of these reasons, performing the conformance test is analogous
services [3]. In particular, it contains a characterization of to verifying at compilation time (that is, a priori) if a class
the various roles played by the services [6]. In our view, a implements an interface in a correct way and to execute a
role specification is not the exact specification of a process static typechecking.
of interest, rather it identifies a set of possible processes, all Sticking to a specification, on the other hand, does not
those whose evolutions respect the dictates given by the role. mean that the service must do all that the role specification
In an open environment, the introduction of a new peer in an defines; indeed, a role specification is just a formal definition
execution context will be determined provided that it satisfies of what is lawful to say or to expect at any given moment
the protocol that characterizes such an execution context; as of the interaction. Taking this observation into account we
long as the new entity satisfies the rules, the interoperability need to define some means for verifying that a single service
with the other components of the system is guaranteed. implementation comforms to the specification of the role in the
The computational model to which web services are inspired protocol that it means to play [14]. The idea is that if a service
is that of distributed objects [10]. An object cannot refuse to passes the conformance test it will be able to interact with a
execute a method which is invoked on it and that is contained set of other services, equally proved individually conformant
in its public interface, in the very same way as a service cannot to the other roles in the protocol, in a way that respects the
refuse to execute over an invocation that respects its public rules defined in the protocol itself.
151
A typical approach to the verification that a service im- and on the circumstances, only one conversation at a time
plementation respects a role definition is to verify whether will actually be expressed, in order to verify conformance a
the execution traces of the service belong to the protocol [1], priori we need to consider them all as a set. It is important to
[12], [7]. This test, however, does not consider processes with remark before proceeding that other proposal, e.g. [2], focus
different branching structures. Another approach, that instead on a different kind of conformance: run-time conformance,
takes this case into account, is to apply bisimulation and say in which only the ongoing conversation is checked against a
that the implementation is conformant if it is bisimilar to protocol.
its role or, more generally, that the composition of a set of Let us then introduce a formal representation of policies
policies is bisimilar to the composition of a set of roles [9], and protocols. We will use finite state automata (FSA). This
[18]. Bisimulation [16], however, does not take into account choice, though simple, is the same used by the well-known
the fact that the implementor’s decisions of cutting some verification system SPIN [15], whose notation we adopt.
interaction path not necessarily compromise the interaction. FSA will be used for representing individual processes that
Many services that respect the intuitions given above will not exchange messages with other processes. Therefore, FSA will
be bisimilar to the specification. Nevertheless, it would be very be used both for representing the roles of a protocol, i.e. the
restrictive to say that they are not conformant (see Section III- abstract descriptions of the interacting parties, as well as for
A). Thus, in order to perform the conformance test we need representing the policies of specific entities involved in the
a softer test, a test that accepts all the processes contained in interaction. In this work we do not consider the translation
a space defined by the role. In this work we provide such a process necessary to turn a protocol (e.g. a WS-CDL choreog-
test (Section III). This proposal differs from previous work raphy) or an entity’s policy (e.g. a BPEL process) in a FSA;
that we have done on conformance [7], [8] in various aspects. our focus is, in fact, conformance and interoperability. It is
First of all, we can now tackle protocols that contain an possible to find in the literature some works that do this kind
arbitrary (though finite) number of roles. Second, we account of translations. An example is [12].
also for the case of policies and roles which produce the same Definition 2.1 (Finite State Automaton): A finite state au-
interactions but have different branching structures. This case tomaton is a tuple (S, s0 , L, T, F ), where S is a finite set of
could not be handled in the previous framework due to the states, s0 ∈ S is a distinguished initial state, L is a finite set
fact that we based it exclusively on a trace semantics. of labels, T ⊆ (S × L × S) is a set of transitions, F ∈ S is a
set of final states.
II. P ROTOCOLS , POLICIES , AND CONVERSATIONS
Similarly to [15] we will denote by the “dot” notation the
A conversation policy is a program that defines the com- components of a FSA, for example we use A.s to denote the
municative behavior of an interactive entity, e.g. a service, state s that belongs to the automaton A. The definition of run
implemented in some programming language [3]. A conversa- is taken from [15].
tion protocol specifies the desired communicative behavior of Definition 2.2 (Runs and strings): A run σ of a FSA
a set of interactive entities. More specifically, a conversation (S, s0 , L, T, F ) is an ordered, possibly infinite, set of transi-
protocol specifies the sequences of messages (also called tions (a sequence) (s0 , l0 , s1 ), (s1 , l1 , s2 ), (s2 , l2 , s3 ), . . . such
speech acts) that can possibly be exchanged by the involved that ∀i ≥ 0, (si , li , si+1 ) ∈ T , while the sequence l0 l1 . . . is
parties, and that we consider as lawful. the corresponding string σ.
In languages that account for communication, speech acts
Definition 2.3 (Acceptance): An accepting run of a finite
often have the form m(as , ar , l), where m is the kind of
state automaton (S, s0 , L, T, F ) is a finite run σ in which the
message, or performative, as (sender) and ar (receiver) are
final transition (sn−1 , ln−1 , sn ) has the property that sn ∈ F .
two interactive entities and l is the message content. In the
The corresponding string σ is an accepted string.
following analysis it is important to distinguish the incoming
Given a FSA A, we say that a state A.s1 ∈ A.S is alive if
messages from the outgoing messages w.r.t a role of a protocol
there exists a finite run (s1 , l1 , s2 ), . . . , (sn−1 , ln−1 , sn ) and
or a policy. We will write m? (incoming message) and m!
sn ∈ A.F . Moreover, we will write A1 ⊆ A2 iff every string
(outgoing message) when the receiver or the utterer and the
of A1 is also a string of A2 .
content of the message is clear from the context or they are
not relevant. So, for instance, m(as , ar , l) is written as m? In order to represent compositions of policies or of individ-
from the point of view of ar , and m! from the point of view ual protocol roles we need to introduce the notions of free and
of the sender. By the term conversation we will, then, denote of synchronous product. These definitions are an adaptation
a sequence of speech acts that is a dialogue of a set of parties. to the problem that we are tackling of the analogous ones
presented in [4] for Finite Transition Systems.
Both a protocol and a policy can be seen as sets of
conversations. In the case of the protocol, it is intuitive that Definition 2.4 (Free product): Let Ai , i = 1, . . . , n, be n
it will be the set of all the possible conversations allowed by FSA’s. The free product A1 × · · · × An is the FSA A =
its specification among the partners. In the case of the single (S, s0 , L, T, F ) defined by:
policy, it will be the set of the possible conversations that the • S is the set A1 .S × · · · × An .S;
entity can carry on according to its implementing program. • s0 is the tuple (A1 .s0 , . . . , An .s0 );
Although at execution time, depending on the interlocutor • L is the set A1 .L × · · · × An .L;
152
• T is the set of tuples of interactive entities and its verification is fundamental in
((A1 .s1 , . . . , An .sn ), (l1 , . . . , ln ), (A1 .s01 , . . . , An .s0n )) order to understand whether the system works. Such a test
such that (Ai .si , li , Ai .s0i ) ∈ Ai .T , for i = 1, . . . , n; and passes through the analysis of all the entities involved in the
• F is the set of tuples (A1 .s1 , . . . , An .sn ) ∈ A.S such interaction.
that si ∈ Ai .F , for i = 1, . . . , n.
We will assume, from now on, that every FSA A has an
empty transition (s, ε, s) for every state s ∈ A.S. When the
finite set of labels L used in a FSA is a set of speech acts,
strings will represent conversations.
Definition 2.5 (Synchronous product): Let Ai ,
i = 1, . . . , n, be n FSA’s. The synchronous product of
the Ai ’s, written A1 ⊗ · · · ⊗ An , is the FSA obtained as
the free product of the Ai ’s containing only the transitions
((A1 .s1 , . . . , An .sn ), (l1 , . . . , ln ), (A1 .s01 , . . . , An .s0n )) such
that there exist i and j, 1 ≤ i 6= j ≤ n, li = m!, lj = m?,
and for any k not equal to i and j, lk = ε.
The synchronous product allows a system that exchanges mes-
sages to be represented. It is worth noting that a synchronous
product does not imply that messages will be exchanged in
a synchronous way; it simply represents a message exchange
without any assumption on how the exchange is carried on.
In order to represent a protocol, we use the synchronous
product of the set of such FSA’s associated with each role Fig. 1. Example of the summer school.
(where each FSA represents the communicative behavior of
the role). Moreover, we will assume that the automata that Figure 1 shows an intuitive example, in which a group of
compound the synchronous product have some “good prop- persons wish to attend a summer school. Each of them can
erties”, which meet the commonly shared intuitions behind speak and understand different languages. For instance, Jan
protocols. In particular, we assume that for the set of such can speak English, Dutch, and French. The school registration
automata the following properties hold: form requires the interested attendee to speak and understand
1) any message that can possibly be sent, at any point of English, which is the official language of the school. This
the execution, will be handled by one of its interlocutor; requirement allows a person to decide if it will be in condition
2) whatever point of conversation has been reached, there to interact with the other participants before attending the
is a way to bring it to an end. school. So, for instance, Matteo, who speaks Italian and could
An arbitrary synchronous product of n FSA’s might not meet therefore interact with Guido, will not be in condition to
these requirements, which can, however, be verified by using understand the other participants. Jan and Leon could interact
automated systems, like SPIN [15]. by speaking Ducth, however, since they also know English,
Note that protocol specification languages, like UML se- they will be able to interact with all the other attendees and
quence (activity) diagrams and automata [17], naturally follow so they will be in condition to participate. The fact that they
these requirements: an arrow starts from the lifeline of a role, understand other languages besides the one required by the
ending into the lifeline of another role, and thus corresponds to “school protocol” does not compromise their interoperability
an outgoing or to an incoming message depending on the point with the others. In fact, within the context of the school
of view. Making an analogy with the computational model of everybody will speak English with them. Interoperability is
distributed objects, one could say that the only messages that compromised when one does not understand (part of) the
are sent are those which can be understood. Moreover, usually protocol (e.g. Matteo) or when one decides to speak a language
protocols contain finite conversations. that is not agreed (e.g. Leon when speaking Dutch).
We will say that a conversation is legal w.r.t. a protocol if In an open system, however, it is quite unlikely to have a
it respects the specifications given by the protocol, i.e. if it is global view of the system either because it is not possible
an accepted string of the protocol. to read part of the necessary information (e.g. some services
do not publish their behavior) or because the interactive
III. I NTEROPERABILITY AND CONFORMANCE TEST
entities are identified at different moments, when necessary.
We are now in position to explain, with the help of a few Protocols are adopted to solve such problems, in fact, having
simple examples, the intuition behind the terms “conformance” an interaction schema allows the distribution of the tests in
and “interoperability”, that we will, then, formalize. By in- time, by checking a single entity at a time against the role
teroperability we mean the capability of a set of entities of that it should play. The protocol, by its own nature guarantees
actually producing a conversation when interacting with one the interoperability of the roles that are part of it. One might
another [5]. Interoperability is a desired property of a system argue why we do not simply verify the system obtained by
153
substituting the policy instead of its role within the protocol Policy Protocol role
and, then, check whether any message that can be sent will be m2 ! m2 !
m ?
handled by some of the interlocutor roles, bringing to an end
(a) m1 ? 6≤ 1
the conversations. Actually, this solution presents some flaws,
m3 !
as the following counter-example proves. Let us consider a No!
m2 !
protocol with three roles: A1 sends m1 to A2 , A2 waits m2 !
m1 ?
for m1 and then it waits for m2 , and A3 sends m2 to A2 . (b) m1 ? ≤
Let us know substitute to role A2 the policy which, first, Ok! m4 !
waits for m2 and then it waits for m1 . The three partners m2 ?
m2 ?
will perfectly interoperate and successfully conclude their m1 !
conversations but the conversation that is produced is not legal (c) m1 ! ≤
w.r.t. the protocol. In protocol-based systems, the proof of the m3 ?
interoperability of an entity with others, obtained by checking Ok! m2 ?
m2 ?
the communicative behavior of the entity against the rules of m !
the system (i.e. against an interaction protocol itself), is known (d)
m1 ! 6≤ 1
No! Missing edge m4 ?
as conformance test. Intuitively, this test must guarantee the
following definition of interoperability.
Definition 3.1 (Interoperability w.r.t. an interaction protocol): Fig. 2. A set of cases that exemplifies our expectations about a conformant
Interoperability w.r.t. an interaction protocol is the capability policy: cases (b) and (c) do not compromise interoperability, hence they should
pass the conformance test; cases (a) and (d) instead should not pass the
of a set of entities of producing a conversation that is legal conformance test.
w.r.t. the protocol.
Let us now consider a given service that should play a role
in a protocol. In order to include it in the interaction we need this policy is not conformant to the protocol because the
to understand if it will be able to interact with the possible service might send a message that cannot be handled by any
players of the other roles. If we assume that the other players interlocutor that conforms to the protocol. The symmetric case
are conformant to their respective roles, we can represent in which the policy accounts for less outgoing messages than
them by the roles themselves. Roles, by the definition of the role specification (Figure 2, row (b)) is, instead, legal. The
protocol, are interoperable. Therefore, in order to prove the reason is that at any point of its conversations the entity will
interoperability of our service, it will be sufficient to prove anyway always utter only messages that the entities playing
for it the “ good properties” of its role. First of all, we should the other roles will surely understand. Hence, interoperability
prove that its policy does not send messages that the others is preserved. The restriction of the set of possible alternatives
cannot understand, which means that it will not send messages (w.r.t. the protocol) depends on the implementor’s own criteria.
that are not accounted for by the role. Moreover, we should Let us now consider the case reported in Figure 2, row
prove that it can tackle every incoming message that the other (c). Here, the service policy accounts for two conversations in
roles might send to it, which means that it must be able to which, after uttering a message m1 , the entity expects one
handle all the incoming messages handled by the role. Another of the two messages m2 or m3 . Let us also suppose that
important property is that whatever point of conversation has the protocol specification only allows the first conversation,
been reached, there is a way to bring it to an end. In practice, i.e. that the only possible incoming message is m2 . When
if a role can bring to an end a conversation in which it has the entity will interact with another that is conformant to the
been engaged, so must do the service. To summarize, in order protocol, the message m3 will never be received because the
to check a service interoperability it will be sufficient to check other entity will never utter it. So, in this case, we would
its conformance w.r.t. the desired role and this check will like the a priori conformance test to accept the policy as
guarantee that the service will be able to interact with services conformant to the specification.
equally, and separately, proved conformant to the other roles. Talking about incoming messages, let us now consider the
This, nevertheless, does not mean that the policy of the service symmetric case (Figure 2, row (d)), in which the protocol
must be a precise “ copy” of the role. specification states that after an outgoing message m1 , an
answer m2 or m4 will be received, while the policy accounts
A. Expectations for interoperability only for the incoming message m2 . In this case, the expec-
Let us now discuss some typical cases in which a policy and tation is that the policy is not conformant because there is
a role specification that differ in various ways are compared a possible incoming message (the one with answer m4 ) that
in order to decide if the policy conforms to the role so as can be enacted by the interlocutor, which, however, cannot be
to guarantee its interoperability with its future interlocutors handled by the policy. This compromises interoperability.
that will play the other roles in the protocol. With reference To summarize, at every point of a conversation, we expect
to Figure 2, let us begin with considering the case reported that a conformant policy never utters speech acts that are not
in row (a): here, the service can possibly utter a message expected, according to the protocol, and we also expect it to be
m3 that is not foreseen by the role specification. Trivially, able to handle any message that can possibly be received, once
154
Policy Protocol role of row (d) does not compromise the conformance, following
m2 ! m2 !
what reported in Figure 2, row (c).
m1 ! m1 !
(a)
m3 !
≤ m3 ! B. Conformance and interoperability
m1 !
m2 ! In this section we define a test, for checking conformance,
m2 !
that is derived from the observations above. A first consider-
m1 ! m1 !
ation is that a conformance test is not an inclusion test w.r.t.
(b)
m3 !
No!
6≤ m3 ! the set of possible conversations that are produced. In fact,
m1 ! for instance, in row (d) of Figure 2 the policy produces a
m2 ? m2 ? subset of the conversations produced by the role specification
m1 ! No! Missing edge m1 ! but interoperability is not guaranteed. Instead, if we consider
(c)
m3 ? 6≤ m3 ? row (c) in the same figure, the set of conversation traces,
m1 ! No! Missing edge produced by the policy, is a superset of the one produced
m2 ? m2 ? by the protocol; despite this, interoperability is guaranteed.
m1 ! m1 ! A second consideration is that a conformance test is not a
(d) ≤ bisimulation test w.r.t. the role specification. Actually, the
m3 ? m3 ?
m1 ! (bi)simulation-based test defined in concurrency theory [16]
is too strict, and it imposes constraints, that would exclude
policies which instead would be able to interoperate, within
Fig. 3. A set of cases that exemplifies our expectations about a conformant the context given by the protocol specification. In particular,
policy: differently than in Figure 2, for every row, the policy and the role
produce the same conversations but the structure of their implementations
all the cases reported in Figure 3 would not be considered
differ. as conformant because they are all pairs of processes with
different branching structures. Despite this, we would like our
test to recognize cases (a) and (d) as conformant because they
again according to the protocol. However, the policy is not do not compromise interoperability.
obliged to foresee (at every point of conversation) an outgoing The solution that we propose is inspired by (bi)simulation,
message for every alternative included in the protocol but it but it distinguishes the ways in which incoming and outgoing
must foresee at least one of them if this is necessary to proceed messages are handled, when a policy is compared to a role 1 .
with the conversation. Trivially, in the example of row (b), In the following, we will use “ A1 ≤ A2 ” to denote the fact
a policy containing only the conversation m1 ? (not followed that A1 conforms to A2 . This choice might seem contradictory
either by m2 ! or by m4 !) would not be conformant. after the previous discussion, in fact, in general A1 ≤ A2 does
Let us now consider a completely different set of situations, not entail A1 ⊆ A2 . However, with symbol “ ≤” we capture the
in which the “ structure” of the policy implemented and the fact that A1 will actually produce a subset of the conversations
structure of the role specification are taken into account. These forseen by the role, when interacting with entities that play
situations are taken from the literature on communicating the other roles in the protocol (see Propositions 3.3 and 3.4).
processes [13]. Figure 3 reports a set of cases in which the role This is what we expect from a conformant policy and from
description and the policy allow the same conversations but our definition of interoperability. Let A an FSA, let us denote
their structure differs: in rows (a) and (c) the policy decides by Succ(l, s) the set of states {s0 | (s, l, s0 ) ∈ A.T }.
which message to send (receive, respectively) after m1 from Definition 3.2 (Conformant simulation): Given two FSA’s
the very beginning, while in the protocol this decision is taken A1 and A2 , A1 is a conformant simulation of A2 , written
after m1 is sent. In row (b) and (d) the situation is inverted. A1 ≤ A2 iff there is a binary relation R between A1 and A2
The case of row (a) does not compromise conformance in such that
the same way as the case reported at row (b) of Figure 2 1) A1 .s0 RA2 .s0 ;
does not: after a non-deterministic choice the set of alternative 2) if si Rsj , where si ∈ A1 .S and sj ∈ A2 .S, then
outgoing messages is restricted but in both cases only legal a) for every (si , m!, si+1 ) ∈ A1 .T , Succ(m!, sj ) 6= ∅
messages that can be handled by the interlocutor will be sent. and si+1 Rs0 for every s0 ∈ Succ(m!, sj );
The analogous case reported in row (c), concerning incoming b) for every (sj , m?, sj+1 ) ∈ A2 .T , Succ(m?, si ) 6= ∅
messages, instead, compromises the conformance. In fact, after and sj+1 Rs0 for every s0 ∈ Succ(m?, si );
the non-deterministic step the policy might receive a message Particularly relevant is the case in which A2 is a role in
that it cannot handle, similarly to row (d) of Figure 2. a protocol and A1 is a policy implementation. Notice that,
The case of row (b), Figure 3, compromises the confor- in this case, conformance is defined only w.r.t. the role that
mance because after the non-deterministic choice the role the single policy implements, independently from the rest of
specification allows a single outgoing message with no alterna- the protocol. As anticipated above, Definition 3.2 does not
tives. The policy, instead, might utter one out of two alternative
messages (similarly to row (a) of Figure 2). Finally, the case 1 All proofs are omitted for lack of space, they will be supplied on demand.
155
imply the fact that “ A1 ≤ A2 entails A1 ⊆ A2 ” . Instead, the The issue of conformance is widely studied in the literature
following proposition holds. in different research fields, like multi-agent systems (MAS)
Proposition 3.3: Let A1 ⊗· · ·⊗Ai ⊗· · ·⊗An be a protocol, and service-oriented computing (SOA). In particular, in the
and A0i a policy such that A0i ≤ Ai , then A1 ⊗ · · · ⊗ A0i ⊗ · · · ⊗ area of MAS, in [7], [5] we have proposed two preliminary
An ⊆ A1 ⊗ · · · ⊗ Ai ⊗ · · · ⊗ An . versions of the current proposal, the former, based on a
This proposition catches the intuition that a conformant policy trace semantics, consisting in an inclusione test, the latter,
is able to produce a subset of the legal conversations defined disregarding the case of different branching structures. The
by the protocol but only when it is executed in the context second technique was also adapted to web services [8]. Both
given by the protocol. works were limited to protocols with only two roles while,
The above proposition can be generalized in the following by means of the framework presented in this paper we can
way. Here we consider a set of policies that have been individ- deal with protocols with an arbitrary finite number of roles.
ually proved as being conformant simulations of the various Inspired to this work the proposal in [1]: here an abductive
roles in a protocol. The property states that the dialogues that framework is used to verify the conformance of services to
such policies can produce will be legal w.r.t. the protocol. a choreography with any number of roles. The limit of this
Proposition 3.4: Let A1 ⊗ · · · ⊗ An be a protocol and let work is that it does not consider the cases in which policies
A01 , . . . , A0n be n policies such that A0i ≤ Ai , for i = 1, . . . , n, and roles have different branching structures. The first proposal
then A01 ⊗ · · · ⊗ A0n ⊆ A1 ⊗ · · · ⊗ An of a formal notion of conformance in a declarative setting is
In order to prove interoperability we need to prove that our due to Endriss et al. [11], the authors, however, do not prove
policies will actually produce a conversation when interacting, any relation between their definitions of conformance and
while so far we have only proved that if a conversation will interoperability. Moreover, they consider protocols in which
be generated, it will be legal. By assumption, in a protocol two partners strictly alternate in uttering messages.
it is always possible to conclude a conversation whatever the In the SOA research field, conformance has been discussed
point at which the interaction arrived. We expect a similar by Foster et al. [12], who defined a system that translates
property to hold also for a set of policies that have been choreographies and orchestrations in labeled transition systems
proved conformant to the roles of a protocol. The relation ≤ so that it becomes possible to apply model checking techniques
is too weak, so we need to introduce the notion of complete and verify properties of theirs. In particular, the system can
conformant simulation. check if a service composition complies with the rules of
Definition 3.5 (Complete conformant simulation): Given a choreography by equivalent interaction traces. Violations
two FSA’s A1 and A2 we say that A1 is a complete are highlighted back to the engineer. Once again, as we
conformant simulation of A2 , written A1 £ A2 , iff there is a discussed, basing on traces can be too much restrictive. In
A1 is a conformant simulation of A2 under a binary relation [9], instead, “ conformability bisimulation” is defined, a variant
R and of the notion of bisimulation. This is the only work that
• for all si ∈ A1 .F such that si Rsj , then sj ∈ A2 .F ; we have found in which different branching structures are
• for all sj ∈ A2 .S such that sj is alive and si Rsj , si ∈ considered but, unfortunately, the test is too strong. In fact,
A1 .S, then si is alive. with reference to Figure 2, it excludes the cases (b) and (c),
Now, we are in the position to give the following fundamental and it also excludes cases (a) and (d) from Figure 3, which
result. do not compromise interoperability. A recent proposal, in this
Theorem 3.6 (Interoperability): Let A1 ⊗ · · · ⊗ An be a same line, is [18], which suffers of the same limitations.
protocol and let A01 , . . . , A0n be n policies such that A0i £ Ai , 1) Acknowledgements.: This research has partially been
for i = 1, . . . , n. For any common string σ 0 of A01 ⊗ · · · ⊗ A0n funded by the European Commission and by the Swiss Federal
and A1 ⊗ · · · ⊗ An there is a run σ 0 σ 00 such that σ 0 σ 00 is an Office for Education and Science within the 6th Frame-
accepted string of A01 ⊗ · · · ⊗ A0n . work Programme project REWERSE number 506779 (cf.
Intuitively, whenever two policies, that have independently http://rewerse.net), and it has also been supported by MIUR
been proved conformant to the two roles of a protocol, start PRIN 2005 “ Specification and verification of agent interaction
an interaction, thanks to Proposition 3.4, they will be able protocols” national project.
to conclude their interaction producing a legal accepted run.
Therefore, Theorem 3.6 implies Definition 3.1 (interoperabil- R EFERENCES
ity).
[1] M. Alberti, F. Chesani, M. Gavanelli, E. Lamma, P. Mello, and M. Mon-
IV. C ONCLUSIONS AND RELATED WORKS tali, “An abductive framework for a-priori verification of web services,”
in Principles and Practice of Declarative Programming, PPDP’06).
In this work we have given a definition of conformance ACM Press, 2006.
and of interoperability that is suitable to application in open [2] M. Alberti, D. Daolio, P. Torroni, M. Gavanelli, E. Lamma, and P. Mello,
environments, like the web. Protocols have been formalized “ Specification and verification of agent interaction protocols in a logic-
based system,” in ACM SAC 2004. ACM, 2004, pp. 72–78.
in the simplest possible way (by means of FSA) to capture
[3] G. Alonso, F. Casati, H. Kuno, and V. Machiraju, Web Services.
the essence of interoperability and to define a fine-grain Springer, 2004.
conformance test. [4] A. Arnold, Finite Transition Systems. Pearson Education, 1994.
156
[5] M. Baldoni, C. Baroglio, A. Martelli, and Patti, “ Verification of protocol
conformance and agent interoperability,” in Post-Proc. of CLIMA VI, ser.
LNCS State-of-the-Art Survey, vol. 3900. Springer, 2006, pp. 265–283.
[6] M. Baldoni, C. Baroglio, A. Martelli, and V. Patti, “ Reasoning about
interaction protocols for customizing web service selection and compo-
sition,” J. of Logic and Alg. Progr., special issue on Web Services and
Formal Methods, 2006, to appear.
[7] M. Baldoni, C. Baroglio, A. Martelli, V. Patti, and C. Schifanella, “ Ver-
ifying protocol conformance for logic-based communicating agents,” in
Proc. of CLIMA V, ser. LNCS, no. 3487. Springer, 2005, pp. 192–212.
[8] — — , “ Verifying the conformance of web services to global interaction
protocols: a first step,” in Proc. of WS-FM 2005, ser. LNCS. Springer,
September, 2005, vol. 3670, pp. 257–271.
[9] N. Busi, R. Gorrieri, C. Guidi, R. Lucchi, and G. Zavattaro, “ Chore-
ography and orchestration: a synergic approach for system design,” in
Proc. of 4th International Conference on Service Oriented Computing
(ICSOC 2005), 2005.
[10] B. Eckel, Thinking in Java. Prentice Hall, 2005.
[11] U. Endriss, N. Maudet, F. Sadri, and F. Toni, “ Logic-based agent com-
munication protocols,” in Advances in agent communication languages,
ser. LNAI, vol. 2922. Springer-Verlag, 2004, pp. 91–107, invited
contribution.
[12] H. Foster, S. Uchitel, J. Magee, and J. Kramer, “ Model-based analysis of
obligations in web service choreography,” in Proc. of IEEE International
Conference on Internet&Web Applications and Services 2006, 2006.
[13] R. v. Glabbeek, “ Bisimulation,” Encyclopedia of Distributed Com-
puting (J.E. Urban & P. Dasgupta, eds.), Kluwer, 2000, available at
http://Boole.stanford.edu/pub/DVI/bis.dvi.gzz.
[14] F. Guerin and J. Pitt, “ Verification and Compliance Testing,” in Com-
munication in Multiagent Systems, ser. LNAI, H. Huget, Ed., vol. 2650.
Springer, 2003, pp. 98–112.
[15] G. J. Holzmann, The SPIN Model Checker : Primer and Reference
Manual. Addison-Wesley Professional, 2003.
[16] R. Milner, Communication and Concurrency. Prentice Hall, 1989.
[17] OMG, “ Unified modeling language: Superstructure,” 2005.
[18] X. Zhao, H. Yang, and Z. Qui, “ Towards the formal model and
verification of web service choreography description language,” in Proc.
of WS-FM 2006, 2006.
157