Conformance and Interoperability in Open Enviroments

Abstract

- An important issue, in open environments like the web, is guaranteeing the interoperability of a set of services. When the interaction scheme that the services should follow is given (e.g. as a choreography or as an interaction protocol), it becomes possible to verify, before the interaction takes place, if the interactive behavior of a service (e.g. a BPEL process specification) respects it. This verification is known as “conformance test”. Recently some attempts have been done for defining conformance tests w.r.t. a protocol but these approaches fail in capturing the very nature of interoperability, turning out to be too restrictive. In this work we give a representation of protocol, based on message exchange and on finite state automata, and we focus on those properties that are essential to the verification the interoperability of a set of services. In particular, we define a conformance test that can guarantee, a priori, the interoperability of a set of services by verifying properties of the single service against the protocol. This is particularly relevant in open environments, where services are identified and composed on demand and dynamically, and the system as a whole cannot be analyzed.

I. INTRODUCTION

In this work we face the problem of verifying the interoperability of a set of peers by exploiting an abstract description of the desired interaction. On the one hand, we will have an interaction protocol (possibly expressed by a choreography), capturing the global interaction of a desired system of services; on the other, we will have a set of service implementations which should be used to assemble the system. The protocol is a specification of the desired interaction, as thus, it might be used for defining several systems of services [ 3 ]. In particular, it contains a characterization of the various roles played by the services [ 6 ]. In our view, a role specification is not the exact specification of a process of interest, rather it identifies a set of possible processes, all those whose evolutions respect the dictates given by the role. In an open environment, the introduction of a new peer in an execution context will be determined provided that it satisfies the protocol that characterizes such an execution context; as long as the new entity satisfies the rules, the interoperability with the other components of the system is guaranteed.

The computational model to which web services are inspired is that of distributed objects [ 10 ]. An object cannot refuse to execute a method which is invoked on it and that is contained in its public interface, in the very same way as a service cannot refuse to execute over an invocation that respects its public interface (although it can refuse the answer). This, however, is not the only possible model of execution. In multi-agent systems, for instance, an agent sending a request message to another agent cannot be certain that it will ever be answered, unless the interaction is ruled by a protocol. The protocol plays, in a way, the role of the public interface: an agent conforming to a protocol must necessarily answer and must be able to handle messages sent by other agents in the context of the protocol itself. The difference between the case of objects and the case of protocols is that the protocol also defines an “execution context” in which using messages. Therefore, the set of messages that it is possible to use varies depending on the point at which the execution has arrived. In a way, the protocol is a dynamic interface that defines messages in the context of the occurring interaction, thus ruling this interaction. On the other hand, the user of an object is not obliged to use all of the methods offered in the public interface and it can implement more methods. The same holds when protocols are used to norm the interaction. Generally speaking, only part of the protocol will be used in an entity’s interaction with another and they can understand more messages than the one forseen by the protocol. Moreover, we will assume that the initiative is taken from the entity that plays as a sender, which will commit to sending a specific message out of its set of alternatives. The receiver will simply execute the reception of the message. Of course, the senders should send a message that its counterpart can understand. For all these reasons, performing the conformance test is analogous to verifying at compilation time (that is, a priori) if a class implements an interface in a correct way and to execute a static typechecking.

Sticking to a specification, on the other hand, does not mean that the service must do all that the role specification defines; indeed, a role specification is just a formal definition of what is lawful to say or to expect at any given moment of the interaction. Taking this observation into account we need to define some means for verifying that a single service implementation comforms to the specification of the role in the protocol that it means to play [ 14 ]. The idea is that if a service passes the conformance test it will be able to interact with a set of other services, equally proved individually conformant to the other roles in the protocol, in a way that respects the rules defined in the protocol itself.

A typical approach to the verification that a service implementation respects a role definition is to verify whether the execution traces of the service belong to the protocol [ 1 ], [ 12 ], [ 7 ]. This test, however, does not consider processes with different branching structures. Another approach, that instead takes this case into account, is to apply bisimulation and say that the implementation is conformant if it is bisimilar to its role or, more generally, that the composition of a set of policies is bisimilar to the composition of a set of roles [ 9 ], [ 18 ]. Bisimulation [ 16 ], however, does not take into account the fact that the implementor’s decisions of cutting some interaction path not necessarily compromise the interaction. Many services that respect the intuitions given above will not be bisimilar to the specification. Nevertheless, it would be very restrictive to say that they are not conformant (see Section IIIA). Thus, in order to perform the conformance test we need a softer test, a test that accepts all the processes contained in a space defined by the role. In this work we provide such a test (Section III). This proposal differs from previous work that we have done on conformance [ 7 ], [ 8 ] in various aspects. First of all, we can now tackle protocols that contain an arbitrary (though finite) number of roles. Second, we account also for the case of policies and roles which produce the same interactions but have different branching structures. This case could not be handled in the previous framework due to the fact that we based it exclusively on a trace semantics.

II. PROTOCOLS, POLICIES, AND CONVERSATIONS

A conversation policy is a program that defines the communicative behavior of an interactive entity, e.g. a service, implemented in some programming language [ 3 ]. A conversation protocol specifies the desired communicative behavior of a set of interactive entities. More specifically, a conversation protocol specifies the sequences of messages (also called speech acts) that can possibly be exchanged by the involved parties, and that we consider as lawful.

In languages that account for communication, speech acts often have the form m(as, ar, l), where m is the kind of message, or performative, as (sender) and ar (receiver) are two interactive entities and l is the message content. In the following analysis it is important to distinguish the incoming messages from the outgoing messages w.r.t a role of a protocol or a policy. We will write m? (incoming message) and m! (outgoing message) when the receiver or the utterer and the 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? from the point of view of ar, and m! from the point of view of the sender. By the term conversation we will, then, denote a sequence of speech acts that is a dialogue of a set of parties.

Both a protocol and a policy can be seen as sets of conversations. In the case of the protocol, it is intuitive that it will be the set of all the possible conversations allowed by its specification among the partners. In the case of the single policy, it will be the set of the possible conversations that the entity can carry on according to its implementing program. Although at execution time, depending on the interlocutor and on the circumstances, only one conversation at a time will actually be expressed, in order to verify conformance a priori we need to consider them all as a set. It is important to remark before proceeding that other proposal, e.g. [ 2 ], focus on a different kind of conformance: run-time conformance, in which only the ongoing conversation is checked against a protocol.

Let us then introduce a formal representation of policies and protocols. We will use finite state automata (FSA). This choice, though simple, is the same used by the well-known verification system SPIN [ 15 ], whose notation we adopt. FSA will be used for representing individual processes that exchange messages with other processes. Therefore, FSA will be used both for representing the roles of a protocol, i.e. the abstract descriptions of the interacting parties, as well as for representing the policies of specific entities involved in the interaction. In this work we do not consider the translation process necessary to turn a protocol (e.g. a WS-CDL choreography) or an entity’s policy (e.g. a BPEL process) in a FSA; our focus is, in fact, conformance and interoperability. It is possible to find in the literature some works that do this kind of translations. An example is [ 12 ].

Definition 2.1 (Finite State Automaton): A finite state automaton is a tuple (S; s0; L; T; F ), where S is a finite set of states, s0 2 S is a distinguished initial state, L is a finite set of labels, T µ (S £ L £ S) is a set of transitions, F 2 S is a set of final states.

Similarly to [ 15 ] we will denote by the “dot” notation the components of a FSA, for example we use A:s to denote the state s that belongs to the automaton A. The definition of run is taken from [ 15 ].

Definition 2.2 (Runs and strings): A run ¾ of a FSA (S; s0; L; T; F ) is an ordered, possibly infinite, set of transitions (a sequence) (s0; l0; s1); (s1; l1; s2); (s2; l2; s3); : : : such that 8i ¸ 0, (si; li; si+1) 2 T , while the sequence l0l1 : : : is the corresponding string ¾.

Definition 2.3 (Acceptance): An accepting run of a finite state automaton (S; s0; L; T; F ) is a finite run ¾ in which the final transition (sn¡1; ln¡1; sn) has the property that sn 2 F . The corresponding string ¾ is an accepted string.

Given a FSA A, we say that a state A:s1 2 A:S is alive if there exists a finite run (s1; l1; s2); : : : ; (sn¡1; ln¡1; sn) and sn 2 A:F . Moreover, we will write A1 µ A2 iff every string of A1 is also a string of A2.

In order to represent compositions of policies or of individual protocol roles we need to introduce the notions of free and of synchronous product. These definitions are an adaptation to the problem that we are tackling of the analogous ones presented in [ 4 ] for Finite Transition Systems.

Definition 2.4 (Free product): Let Ai, i = 1; : : : ; n, be n FSA’s. The free product A1 £ ¢ ¢ ¢ £ An is the FSA A = (S; s0; L; T; F ) defined by: ² S is the set A1:S £ ¢ ¢ ¢ £ An:S; ² s0 is the tuple (A1:s0; : : : ; An:s0); ² L is the set A1:L £ ¢ ¢ ¢ £ An:L; ² T is the set of tuples ((A1:s1; : : : ; An:sn); (l1; : : : ; ln); (A1:s01; : : : ; An:s0n)) 0 such that (Ai:si; li; Ai:si) 2 Ai:T , for i = 1; : : : ; n; and ² F is the set of tuples (A1:s1; : : : ; An:sn) 2 A:S such that si 2 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 2 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 messages 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 (where each FSA represents the communicative behavior of the role). Moreover, we will assume that the automata that compound the synchronous product have some “good properties”, which meet the commonly shared intuitions behind protocols. In particular, we assume that for the set of such automata the following properties hold: 1) any message that can possibly be sent, at any point of the execution, will be handled by one of its interlocutor; 2) whatever point of conversation has been reached, there is a way to bring it to an end.

An arbitrary synchronous product of n FSA’s might not meet these requirements, which can, however, be verified by using automated systems, like SPIN [ 15 ].

Note that protocol specification languages, like UML sequence (activity) diagrams and automata [ 17 ], naturally follow these requirements: an arrow starts from the lifeline of a role, ending into the lifeline of another role, and thus corresponds to an outgoing or to an incoming message depending on the point of view. Making an analogy with the computational model of distributed objects, one could say that the only messages that are sent are those which can be understood. Moreover, usually protocols contain finite conversations.

We will say that a conversation is legal w.r.t. a protocol if it respects the specifications given by the protocol, i.e. if it is an accepted string of the protocol.

III. INTEROPERABILITY AND CONFORMANCE TEST

We are now in position to explain, with the help of a few simple examples, the intuition behind the terms “conformance” and “interoperability”, that we will, then, formalize. By interoperability we mean the capability of a set of entities of actually producing a conversation when interacting with one another [ 5 ]. Interoperability is a desired property of a system of interactive entities and its verification is fundamental in order to understand whether the system works. Such a test passes through the analysis of all the entities involved in the interaction.

Figure 1 shows an intuitive example, in which a group of persons wish to attend a summer school. Each of them can speak and understand different languages. For instance, Jan can speak English, Dutch, and French. The school registration form requires the interested attendee to speak and understand English, which is the official language of the school. This requirement allows a person to decide if it will be in condition to interact with the other participants before attending the school. So, for instance, Matteo, who speaks Italian and could therefore interact with Guido, will not be in condition to understand the other participants. Jan and Leon could interact by speaking Ducth, however, since they also know English, they will be able to interact with all the other attendees and so they will be in condition to participate. The fact that they understand other languages besides the one required by the “school protocol” does not compromise their interoperability with the others. In fact, within the context of the school everybody will speak English with them. Interoperability is compromised when one does not understand (part of) the protocol (e.g. Matteo) or when one decides to speak a language that is not agreed (e.g. Leon when speaking Dutch).

In an open system, however, it is quite unlikely to have a global view of the system either because it is not possible to read part of the necessary information (e.g. some services do not publish their behavior) or because the interactive entities are identified at different moments, when necessary.

Protocols are adopted to solve such problems, in fact, having an interaction schema allows the distribution of the tests in time, by checking a single entity at a time against the role that it should play. The protocol, by its own nature guarantees the interoperability of the roles that are part of it. One might argue why we do not simply verify the system obtained by substituting the policy instead of its role within the protocol and, then, check whether any message that can be sent will be m2! handled by some of the interlocutor roles, bringing to an end (a) m1? 6· m1? the conversations. Actually, this solution presents some flaws, m3! fapLosrerottthmouecs1oflkoanlnwlodoiwwththinsetgunhbrcesitoteiutwunrtoateeilters-tseo:fxoaArrom1lmepls2eAe,np2adrnsotdhvmeeAs1.p3oLtsloeiectnyAduss2w, mhcAoi2cn2hst,iodwfieAarris2ttas,. (b) m1? OmkN!2o!! · m1? mm42!! waits for m2 and then it waits for m1. The three partners m2? m2? cwoinllvepresarfteiocntlsybuint ttehreopceornavteersaantidonstuhcacteisssfpurlolyducceodncilsundoet ltehgeairl (c) m1! · m1! w.r.t. the protocol. In protocol-based systems, the proof of the m3? interoperability of an entity with others, obtained by checking mOk2!? m2? ttahhseecscoyonsmftoemmrmu(naiin.ecc.aetaigvteaesintb.setIhnaatnvuiiiotnirtveeorlfayc,thtiteohniesnpttreiotsyttocamogulasiinttssgetlufta)h,reaisnrtukelneeostwhonef (d) m1! No! Missing edge6· m1! m4? 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 Ionftearospeetroabfileintytitwie.sr.to.fanpriondtuercainctgioan cpornovtoecrsoaltiiosnthtehactapisableilgitayl cppoaosnlisfcoytr:hmceaanscecosen(ftboe)rsmta.nadnc(ec) tdeostn;octacsoemsp(rao)mainsed in(dte)roinpsetreaabdilistyh,ohueldncenothtepyasshsouthlde 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 to understand if it will be able to interact with the possible players of the other roles. If we assume that the other players are conformant to their respective roles, we can represent them by the roles themselves. Roles, by the definition of protocol, are interoperable. Therefore, in order to prove the interoperability of our service, it will be sufficient to prove for it the “ good properties” of its role. First of all, we should prove that its policy does not send messages that the others cannot understand, which means that it will not send messages that are not accounted for by the role. Moreover, we should prove that it can tackle every incoming message that the other roles might send to it, which means that it must be able to handle all the incoming messages handled by the role. Another important property is that whatever point of conversation has been reached, there is a way to bring it to an end. In practice, if a role can bring to an end a conversation in which it has been engaged, so must do the service. To summarize, in order to check a service interoperability it will be sufficient to check its conformance w.r.t. the desired role and this check will guarantee that the service will be able to interact with services equally, and separately, proved conformant to the other roles.

This, nevertheless, does not mean that the policy of the service must be a precise “ copy” of the role. this policy is not conformant to the protocol because the service might send a message that cannot be handled by any interlocutor that conforms to the protocol. The symmetric case in which the policy accounts for less outgoing messages than the role specification (Figure 2, row (b)) is, instead, legal. The reason is that at any point of its conversations the entity will anyway always utter only messages that the entities playing the other roles will surely understand. Hence, interoperability is preserved. The restriction of the set of possible alternatives (w.r.t. the protocol) depends on the implementor’s own criteria.

Let us now consider the case reported in Figure 2, row (c). Here, the service policy accounts for two conversations in which, after uttering a message m1, the entity expects one of the two messages m2 or m3. Let us also suppose that the protocol specification only allows the first conversation, i.e. that the only possible incoming message is m2. When the entity will interact with another that is conformant to the protocol, the message m3 will never be received because the other entity will never utter it. So, in this case, we would like the a priori conformance test to accept the policy as conformant to the specification.

Talking about incoming messages, let us now consider the symmetric case (Figure 2, row (d)), in which the protocol specification states that after an outgoing message m1, an answer m2 or m4 will be received, while the policy accounts only for the incoming message m2. In this case, the expectation is that the policy is not conformant because there is a possible incoming message (the one with answer m4) that can be enacted by the interlocutor, which, however, cannot be handled by the policy. This compromises interoperability.

To summarize, at every point of a conversation, we expect that a conformant policy never utters speech acts that are not expected, according to the protocol, and we also expect it to be able to handle any message that can possibly be received, once

A. Expectations for interoperability

Let us now discuss some typical cases in which a policy and a role specification that differ in various ways are compared in order to decide if the policy conforms to the role so as to guarantee its interoperability with its future interlocutors that will play the other roles in the protocol. With reference to Figure 2, let us begin with considering the case reported in row (a): here, the service can possibly utter a message m3 that is not foreseen by the role specification. Trivially, No! Missing edge

6· m3? No! Missing edge m2? · 6· · m1! m1! m1! m1! m1! m1! (a) (b) (c) (d) m1! m1! m1! m1! m1! m1! again according to the protocol. However, the policy is not obliged to foresee (at every point of conversation) an outgoing message for every alternative included in the protocol but it must foresee at least one of them if this is necessary to proceed with the conversation. Trivially, in the example of row (b), a policy containing only the conversation m1? (not followed either by m2! or by m4!) would not be conformant.

Let us now consider a completely different set of situations, in which the “ structure” of the policy implemented and the structure of the role specification are taken into account. These situations are taken from the literature on communicating processes [ 13 ]. Figure 3 reports a set of cases in which the role description and the policy allow the same conversations but their structure differs: in rows (a) and (c) the policy decides which message to send (receive, respectively) after m1 from the very beginning, while in the protocol this decision is taken after m1 is sent. In row (b) and (d) the situation is inverted.

The case of row (a) does not compromise conformance in the same way as the case reported at row (b) of Figure 2 does not: after a non-deterministic choice the set of alternative outgoing messages is restricted but in both cases only legal messages that can be handled by the interlocutor will be sent. The analogous case reported in row (c), concerning incoming messages, instead, compromises the conformance. In fact, after the non-deterministic step the policy might receive a message that it cannot handle, similarly to row (d) of Figure 2.

The case of row (b), Figure 3, compromises the conformance because after the non-deterministic choice the role specification allows a single outgoing message with no alternatives. The policy, instead, might utter one out of two alternative messages (similarly to row (a) of Figure 2). Finally, the case m3! m2! m3! m2? m3? m2? m3? of row (d) does not compromise the conformance, following what reported in Figure 2, row (c).

B. Conformance and interoperability

In this section we define a test, for checking conformance, that is derived from the observations above. A first consideration is that a conformance test is not an inclusion test w.r.t. the set of possible conversations that are produced. In fact, for instance, in row (d) of Figure 2 the policy produces a subset of the conversations produced by the role specification but interoperability is not guaranteed. Instead, if we consider row (c) in the same figure, the set of conversation traces, produced by the policy, is a superset of the one produced by the protocol; despite this, interoperability is guaranteed. A second consideration is that a conformance test is not a bisimulation test w.r.t. the role specification. Actually, the (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 the context given by the protocol specification. In particular, all the cases reported in Figure 3 would not be considered 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 do not compromise interoperability.

The solution that we propose is inspired by (bi)simulation, but it distinguishes the ways in which incoming and outgoing messages are handled, when a policy is compared to a role 1. In the following, we will use “ A1 · A2” to denote the fact that A1 conforms to A2. This choice might seem contradictory after the previous discussion, in fact, in general A1 · A2 does not entail A1 µ A2. However, with symbol “ ·” we capture the fact that A1 will actually produce a subset of the conversations forseen by the role, when interacting with entities that play the other roles in the protocol (see Propositions 3.3 and 3.4). This is what we expect from a conformant policy and from our definition of interoperability. Let A an FSA, let us denote by Succ(l; s) the set of states fs0 j (s; l; s0) 2 A:T g.

Definition 3.2 (Conformant simulation): Given two FSA’s A1 and A2, A1 is a conformant simulation of A2, written A1 · A2 iff there is a binary relation R between A1 and A2 such that 1) A1:s0RA2:s0; 2) if siRsj , where si 2 A1:S and sj 2 A2:S, then a) for every (si; m!; si+1) 2 A1:T , Succ(m!; sj ) 6= ; and si+1Rs0 for every s0 2 Succ(m!; sj ); b) for every (sj ; m?; sj+1) 2 A2:T , Succ(m?; si) 6= ; and sj+1Rs0 for every s0 2 Succ(m?; si); Particularly relevant is the case in which A2 is a role in a protocol and A1 is a policy implementation. Notice that, in this case, conformance is defined only w.r.t. the role that the single policy implements, independently from the rest of the protocol. As anticipated above, Definition 3.2 does not 1All proofs are omitted for lack of space, they will be supplied on demand. imply the fact that “ A1 · A2 entails A1 µ A2” . Instead, the following proposition holds.

Proposition 3.3: Let A1 ­¢ ¢ ¢­Ai ­¢ ¢ ¢­An be a protocol, and A0i a policy such that A0i · Ai, then A1 ­ ¢ ¢ ¢ ­ A0i ­ ¢ ¢ ¢ ­ An µ A1 ­ ¢ ¢ ¢ ­ Ai ­ ¢ ¢ ¢ ­ An.

This proposition catches the intuition that a conformant policy is able to produce a subset of the legal conversations defined by the protocol but only when it is executed in the context given by the protocol.

The above proposition can be generalized in the following way. Here we consider a set of policies that have been individually proved as being conformant simulations of the various roles in a protocol. The property states that the dialogues that such policies can produce will be legal w.r.t. the protocol.

Proposition 3.4: Let A1 ­ ¢ ¢ ¢ ­ An be a protocol and let A01; : : : ; A0n be n policies such that A0i · Ai, for i = 1; : : : ; n, then A01 ­ ¢ ¢ ¢ ­ A0n µ A1 ­ ¢ ¢ ¢ ­ An In order to prove interoperability we need to prove that our policies will actually produce a conversation when interacting, while so far we have only proved that if a conversation will be generated, it will be legal. By assumption, in a protocol it is always possible to conclude a conversation whatever the point at which the interaction arrived. We expect a similar property to hold also for a set of policies that have been proved conformant to the roles of a protocol. The relation · is too weak, so we need to introduce the notion of complete conformant simulation.

Definition 3.5 (Complete conformant simulation): Given two FSA’s A1 and A2 we say that A1 is a complete conformant simulation of A2, written A1 £ A2, iff there is a A1 is a conformant simulation of A2 under a binary relation R and ² for all si 2 A1:F such that siRsj , then sj 2 A2:F ; ² for all sj 2 A2:S such that sj is alive and siRsj , si 2

A1:S, then si is alive.

Now, we are in the position to give the following fundamental result.

Theorem 3.6 (Interoperability): Let A1 ­ ¢ ¢ ¢ ­ An be a protocol and let A01; : : : ; A0n be n policies such that A0i £ Ai, for i = 1; : : : ; n. For any common string ¾0 of A01 ­ ¢ ¢ ¢ ­ An 0 and A1 ­ ¢ ¢ ¢ ­ An there is a run ¾0¾00 such that ¾0¾00 is an accepted string of A01 ­ ¢ ¢ ¢ ­ An. 0 Intuitively, whenever two policies, that have independently been proved conformant to the two roles of a protocol, start an interaction, thanks to Proposition 3.4, they will be able to conclude their interaction producing a legal accepted run. Therefore, Theorem 3.6 implies Definition 3.1 (interoperability).

IV. CONCLUSIONS AND RELATED WORKS

In this work we have given a definition of conformance and of interoperability that is suitable to application in open environments, like the web. Protocols have been formalized in the simplest possible way (by means of FSA) to capture the essence of interoperability and to define a fine-grain conformance test.

The issue of conformance is widely studied in the literature in different research fields, like multi-agent systems (MAS) and service-oriented computing (SOA). In particular, in the area of MAS, in [ 7 ], [ 5 ] we have proposed two preliminary versions of the current proposal, the former, based on a trace semantics, consisting in an inclusione test, the latter, disregarding the case of different branching structures. The second technique was also adapted to web services [ 8 ]. Both works were limited to protocols with only two roles while, by means of the framework presented in this paper we can deal with protocols with an arbitrary finite number of roles. Inspired to this work the proposal in [ 1 ]: here an abductive framework is used to verify the conformance of services to a choreography with any number of roles. The limit of this work is that it does not consider the cases in which policies and roles have different branching structures. The first proposal of a formal notion of conformance in a declarative setting is due to Endriss et al. [ 11 ], the authors, however, do not prove any relation between their definitions of conformance and interoperability. Moreover, they consider protocols in which two partners strictly alternate in uttering messages.

In the SOA research field, conformance has been discussed by Foster et al. [ 12 ], who defined a system that translates choreographies and orchestrations in labeled transition systems so that it becomes possible to apply model checking techniques and verify properties of theirs. In particular, the system can check if a service composition complies with the rules of a choreography by equivalent interaction traces. Violations are highlighted back to the engineer. Once again, as we discussed, basing on traces can be too much restrictive. In [ 9 ], instead, “ conformability bisimulation” is defined, a variant of the notion of bisimulation. This is the only work that we have found in which different branching structures are considered but, unfortunately, the test is too strong. In fact, with reference to Figure 2, it excludes the cases (b) and (c), and it also excludes cases (a) and (d) from Figure 3, which do not compromise interoperability. A recent proposal, in this same line, is [ 18 ], which suffers of the same limitations.

1) Acknowledgements.: This research has partially been funded by the European Commission and by the Swiss Federal Office for Education and Science within the 6th Framework Programme project REWERSE number 506779 (cf. http://rewerse.net), and it has also been supported by MIUR PRIN 2005 “ Specification and verification of agent interaction protocols” national project.

References

[1] M. Alberti , F. Chesani , M. Gavanelli , E. Lamma, P. Mello , and M. Montali , “ An abductive framework for a-priori verification of web services,” in Principles and Practice of Declarative Programming , PPDP'06) . ACM Press, 2006 .

[2] M. Alberti , D. Daolio , P. Torroni , M. Gavanelli , E. Lamma, and P. Mello , “ Specification and verification of agent interaction protocols in a logicbased system,” in ACM SAC 2004 . ACM, 2004 , pp. 72 - 78 .

[3] G. Alonso , F. Casati , H. Kuno , and V. Machiraju , Web Services. Springer, 2004 .

[4] A. Arnold , Finite Transition Systems. Pearson Education , 1994 .

[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 composition,” 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 , “ Verifying 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, “ Choreography 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 communication 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 Computing (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 Communication 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 .