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