Meriem Ouederni

Uli Fahrenberg

Axel Legay

Gwen Salaün

Flooding-Based Algorithm for Behavioural Compatibility Measuring

Nowadays, large software systems are mostly built using existing services. These are not always designed to interact, i.e., their public interfaces often present some mismatches. Checking compatibility of service interfaces allows one to avoid erroneous executions when composing the services and ensures correct reuse and interaction. Service compatibility has been intensively studied, in particular for discovery purposes, but most of existing approaches return a Boolean result. In this paper, we present a quantitative approach for measuring the compatibility degree of service interfaces. Our method is generic and flooding-based, and fully automated by a prototype tool.

Introduction

In service oriented computing, software systems are mostly built using existing services. Services are considered as black boxes accessed through their public interfaces which present four interoperability levels [START_REF] Becker | Towards an engineering approach to component adaptation[END_REF], i.e., signature, interaction protocols, quality of services, and semantics. These interfaces must be compatible in order to ensure the correct composition and reuse of loosely-coupled services. This paper deals with the compatibility verification of service interfaces and focuses on the interaction protocol level. Checking the compatibility of interaction protocols is a tedious and hard task, even though it is of utmost importance to avoid run-time errors, e.g., deadlock situations or unmatched messages.

Most of the existing approaches (see [START_REF] Durán | A generic framework for n-protocol compatibility checking[END_REF] for a detailed survey) return a "True" or "False" result to detect whether services are compatible or not. Unfortunately, a Boolean answer is not very helpful for many issues. Firstly, in real world case studies, there will seldom be a perfect match, and when service protocols are not compatible, it is useful to differentiate between services that are slightly incompatible and those that are totally incompatible. Secondly, a Boolean result does not give any detailed information on which parts of service protocols are compatible or not. Thirdly, regarding the incompatible parts of protocols, such a result typically does not come with a mismatch list which enables us to understand and then resolve the incompatibility issues.

To overcome the aforementioned limits, a new solution aims at quantifying the compatibility degree of service interfaces. This issue has been addressed by a few recent works, see for instance Related Work Section. However, most of them are based upon description models of service interfaces, e.g., business Fig. 1. A simple medical management system. protocols [START_REF] Nezhad | Protocol-aware Matching of Web Service Interfaces for Adapter Development[END_REF], which do not consider value-passing coming with exchanged messages and internal behaviours (τ transitions). Internal behaviours in interface models are very important because some services can be compatible from an observable point of view, but their execution will behave erroneously if these behaviours are not taken into account [START_REF] Ouederni | Tau be or not tau be? -a perspective on service compatibility and substitutability[END_REF]. Moreover, existing approaches, such as [START_REF] Wu | Computing Compatibility in Dynamic Service Composition[END_REF], measure the interface compatibility using a simple (i.e., not iterative) traversal of protocols, and the results lack the preciseness which is essential for detecting subtle protocol mismatches. Lastly, a unique compatibility notion is always considered to check the services, and this makes the approaches useful only for specific application areas, e.g., service choreography [START_REF] Lohmann | Correcting deadlocking service choreographies using a simulation-based graph edit distance[END_REF] or service adaptation [START_REF] Nezhad | Protocol-aware Matching of Web Service Interfaces for Adapter Development[END_REF].

As an example, we refer to the symbolic transition systems 4 in Fig. 1, describing an on-line medical management system which handles patient appointments within a health care institution, either with general practitioners or with specialist doctors. The Client can first log on to a server by sending her user name and password (login!). Then, she asks for an appointment with a general practitioner (reqDoc!) and receives an appointment identifier. We present three services for the medical server, which all seem to match the Client service, yet they all fail in subtle ways: MedServer0 can only receive user name and password separately, whereas Client wants to send them together; MedServer1 has a type mismatch on the usr parameter; and with MedServer2, communication can deadlock (if it silently proceeds to state s6, for example after a timeout). Hence none of the MedServer services are compatible with Client. We shall, however, later see that, using our quantitative techniques, there is a clear preference for MedServer1 in which the incompatibilities are much easier mended than in the other two.

In this paper, we propose a novel approach for quantifying the compatibility degree of interacting services. Instead of a Boolean result, we compute a numerical measure in the interval [0..1], where 0 means no compatibility and 1 means perfect compatibility. We describe service interfaces using a formal model, taking into account interaction protocols, i.e., messages and their application order, but also value-passing and internal actions. We propose a generic framework where the compatibility degree of service interfaces can be automatically measured according to different compatibility notions. We illustrate our approach using bidirectional and unidirectional compatibility notions, namely unspecified receptions [START_REF] Yellin | Protocol Specifications and Component Adaptors[END_REF] and unidirectional complementarity; additional notions can easily be added to our framework. The compatibility is computed in two steps. First, we compute a set of static compatibility degrees where the execution order of messages is not taken into account. Then, we user a flooding algorithm to compute the compatibility degree of interaction protocols using the static compatibility results. The computation process also returns the mismatch list indicating the interoperability issues, and a global compatibility degree for two interaction protocols. Our solution is fully automated by a prototype tool Comparator [START_REF]Comparator web[END_REF] we have implemented.

This paper improves previous preliminary approaches [START_REF] Ouederni | Quantifying service compatibility: A step beyond the boolean approaches[END_REF][START_REF] Ouederni | Measuring the compatibility of service interaction protocols[END_REF] as follows. We give the mathematical definitions of our heuristics used for computing the compatibility of two service interfaces. We also show how our approach can be used for systems interacting using an asynchronous communication model. We prove, using Banach's fixed point theorem, that the flooding-based computation always converges. Finally, we present several experiments to better evaluate our prototype tool.

Quantifying protocol compatibility brings more advantages than the Boolean approaches, because it returns a detailed measure but also a list of mismatches that can be useful for many service applications, such as automatic service ranking, service discovery, composition, or adaptation. In the case of service adaptation [START_REF] Mateescu | Adaptation of service protocols using process algebra and on-the-fly reduction techniques[END_REF] for instance, if a set of services are incompatible, the detailed measure and the mismatch list help to understand which parts of these services do not match. Thus, the mismatches can be worked out using adaptation techniques, and service composition can be achieved in spite of existing mismatches.

Service Model and Notations

We describe service interfaces using interaction protocols represented by Symbolic Transition Systems (STSs). Our STSs are a variant of STGs (Symbolic Transition Graphs) [START_REF] Hennessy | Symbolic Bisimulations[END_REF] where guards are replaced with internal τ transitions. These transitions keep an abstraction closer to the service implementation and ensure (if services are compatible) a correct interaction whatever values are exchanged. Definition 1. A Symbolic Transition System, or STS, is a tuple (A, S, I, F, T ) where: A is an alphabet which corresponds to the set of labels associated to transitions, S is a set of states, I ∈ S is the initial state, F ⊆ S is a nonempty set of final states, and T ⊆ S \ F × A × S is the transition relation.

A label is either the (internal) τ action or a tuple (m, d, pl) where m is the message name, d is the communication direction (either an emission ! or a reception ?), and pl is either a list of typed data terms if the label corresponds to an emission, or a list of typed variables if the label is a reception. Here, services interact with each other based on a synchronous and binary communication model. The operational semantics of this model is formalised in [START_REF] Durán | A generic framework for n-protocol compatibility checking[END_REF].

The STS model is simple, yet offers a good abstraction level for describing and analysing service behaviours. Moreover, STSs can be easily derived from abstract descriptions implemented in existing programming languages (e.g., Abstract BPEL -Business Process Execution Language or WF -Workflow) [START_REF] Cámara | Itaca: An integrated toolbox for the automatic composition and adaptation of web services[END_REF] for verification, <?xml v e r s i o n=" 1 . 0 " e n c o d i n g="UTF-8" ?> < p r o c e s s name=" M e d i c a l D a t a b a s e " /> <p a r t n e r L i n k s> <p a r t n e r L i n k name="DB" p a r t n e r L i n k T y p e=" tns:MedDb " myRole=" MedDbPortTypeRole " /> </ p a r t n e r L i n k s> . . . <s e q u e n c e> < r e c e i v e name=" a v a i l a b i l i t y _ R E C _ 1 " p a r t n e r L i n k="DB" o p e r a t i o n=" a v a i l a b i l i t y " p o r t T y p e=" tns:MedDbPortType "> </ r e c e i v e> . . . < r e p l y name=" a v a i l a b i l i t y _ I N V _ 1 " p a r t n e r L i n k="DB" o p e r a t i o n=" a v a i l a b i l i t y " p o r t T y p e=" tns:MedDbPortType "> </ r e p l y> </ s e q u e n c e> </ p r o c e s s> Fig. 2. Simplified BPEL and its STSs.

composition or adaptation purposes. For instance, BPEL is used by the service community for building large applications by reusing distributed and interacting services to reply complex user requests. Fig. 2 illustrates a simplified version of a BPEL example and the extracted STS.

In the rest of the article we will describe service interfaces only with their corresponding STSs. Signatures will be left implicit, yet they can be inferred from the typing of arguments in STS labels. We suppose that there are no cycles of internal transitions, i.e., no transition sequences (s 1 , τ, s 2 ), . . . , (s n , τ, s 1 ).

Service Compatibility

Service compatibility is achieved if services can correctly interact with each other, i.e., synchronisations over observable actions which are exchanged between services. Checking for correct service interaction needs to verify if service protocols satisfy a criterion, i.e., compatibility notion. In this article, we compute the compatibility for two services and we distinguish two classes of notions, i.e., bidirectional and unidirectional, depending on the direction of the compatibility checking. We particularly illustrate our approach with a bidirectional notion, namely unspecified receptions (UR for short), and with an unidirectional notion, namely unidirectional complementarity (UC for short). In the case of unidirectional compatibility checking, one of the two services plays a particular role because its requirements (messages) must all be satisfied by the partner service. This class can be useful for checking, e.g., a client/server model. In this setting, a server service must be able to receive and answer all requests from a client, but this server can also handle other requests from other clients.

Before defining both UR and UC, we give below some preliminary concepts on which those compatibility notions rely: Static Compatibility. Parameter compatibility requires that the parameter list expected to be received matches (same types in the same order) the parameter list coming with the sent message. Label compatibility requires labels to have opposite directions, same names, and compatible parameters. Reachable States. Reachability analysis aims at computing the set of global states that interacting protocols can access, in zero or more steps, from a current global state (s 1 , s 2 ). Protocols can move into reachable states through synchronisations on compatible labels or independent evolutions, i.e., τ transitions. Deadlock-Freeness. This is required for checking successful system termination, i.e., the services can always interoperate starting from a given global state until reaching final states. All the traversed global states belong to the set of deadlockfree states (referred to as DF) . State Compatibility. Service interaction depends on synchronisation over observable actions and is defined using a criterion to be checked on reachable global states. For a given global state (s 1 , s 2 ) of two protocols STS i = (A i , S i , I i , F i , T i ), this state is compatible if every message l 1 sent (received) by STS 1 at state s 1 will be eventually received (sent, respectively) by STS 2 at state s 2 , such that both protocols evolve into a compatible global state, and vice-versa. If STS 2 is not able to interact with STS 1 's action, then both protocols must be able to reach a global state (s 1 , s 2 ) in which this action will be satisfied, i.e., ∃(s 2 , l 2 , s 2 ) ∈ T 2 such that l 1 and l 2 are compatible, and vice-versa. In this case, both states (s 1 , s 2 ) and (s 1 , s 2 ) must also be compatible. Note that we handle τ actions similarly to branching equivalence [START_REF] Van Glabbeek | Branching time and abstraction in bisimulation semantics[END_REF].

Additionally to the forward exploration above, state compatibility is determined by backtracking along transitions. Hence, every transition in one ST S leading to (s 1 , s 2 ) must much with a transition in the other ST S where their labels are compatible. Furthermore both transitions must come from compatible states such that τ actions are handled similarly as stated above.

Unspecified Receptions (UR). This notion is inspired from [START_REF] Yellin | Protocol Specifications and Component Adaptors[END_REF] and requires that two services are compatible if (i) they are deadlock-free, and (ii) if one service can send a message at a reachable state, then its partner must eventually receive that emission such that both services evolve into a compatible global state. In real-life cases, one service must receive all requests from its partner, but can also be ready to accept other receptions, since the service could interoperate with other partners. Hence, there might be additional unmatched receptions in reachable states, possibly followed by unmatched emissions. These emissions do not give rise to an incompatibility issue as long as their source states are unreachable when protocols interact with each other. Unidirectional Complementarity (UC ). Two services are compatible wrt. the UC notion if (1) they are deadlock-free and (2) one of them (the complementer) must eventually receive and send all messages that its partner (complemented) expects to send and receive, respectively, at all global reachable states. Hence, the complementer service may send and receive more messages than the complemented service. This asymmetric notion is useful to check the successful communication in the client/server model where a server can interact with clients with different behaviours. In this setting, each client behaviour must be satisfied (complemented) by the server.

Quantifying Compatibility

This section presents our techniques for measuring the compatibility of two service protocols. These techniques rely on the compatibility definitions given in Section 3. We compute the compatibility at several levels of service interfaces such as states, labels, and parameters. We aim at using all information described in service interfaces in order to get the highest precision for the computed compatibility. The final compatibility degree of two interaction protocols is computed relying on all these sources of compatibility, and following a divide-and-conquer approach.

For purpose of clarity, we assume in the rest of this article that the different functions defined have access to the STS i = (A i , S i , I i , F i , T i ) even if they are not explicitly passed as input parameters. However, we make parameters explicit if they are modified. The approach overviewed in Fig. 3 consists first in computing three static compatibility measures (Section 4.1) where the order of exchanged messages is not considered. In a second step, these static measures are used for computing the behavioural compatibility degree for all global states (Section 4.2). Lastly, we show how the global compatibility degree is computed (Section 4.3).

Static Compatibility

State Nature. We compare state nature using the function nat((s 1 , s 2 )). It returns 1 if states s 1 and s 2 have the same nature, i.e., both are either initial, final or none of the two. Otherwise, nat((s 1 , s 2 )) = 0 returns 0: Parameters. The compatibility degree of two lists of parameters exchanged with messages pl 1 and pl 2 depends on three auxiliary measures, namely: (i) the compatibility of parameter number, (ii) the compatibility of parameter order, and (iii) the compatibility of parameter type. These measures must be set to 1 if pl 1 ∪ pl 2 = ∅. Otherwise, they are computed as follows:

number(pl 1 , pl 2 ) = 1 -abs(|pl1|-|pl2|) max(|pl1|,|pl2|) order(pl 1 , pl 2 ) = 1 -|unorderedT ypes(pl1,pl2)| |sharedT ypes(pl1,pl2)| type(pl 1 , pl 2 ) = 1 -|unsharedT ypes(pl1,pl2)| |pl1|+|pl2|
Here, the function unorderedT ypes returns the set of parameter types existing in pl 1 and pl 2 -i.e., shared types-but which are not in the same order in both lists. The function unsharedT ypes returns the set of parameter types existing in only one list.

The function par-comp then computes the parameter compatibility as the average of the measures returned by the three previous functions: par-comp(pl 1 , pl 2 ) = number(pl1,pl2)+order(pl1,pl2)+type(pl1,pl2) 3 Labels. We measure label compatibility as follows. Given a pair of labels (l 1 , l 2 ) ∈ A 1 × A 2 with l i = (m i , d i , pl i ), the function lab-comp(l 1 , l 2 ) returns 0 if l 1 and l 2 have the same direction, and otherwise computes the average of the semantic compatibility of message names 5 and par-comp(pl 1 , pl 2 ):

lab-comp(l 1 , l 2 ) = 0 if d 1 = d 2 sem-comp(m1,m2)+par-comp(pl1,pl2) 2 otherwise

Behavioural Compatibility

We now present our metrics to compute the behavioural compatibility for two service protocols, STS i = (A i , S i , I i , F i , T i ), using the static measures previously introduced in Section 4.1. The intuition underlying theses metrics relies on the compatibility definitions given in Section 3. We describe a flooding algorithm which performs an iterative measuring of behavioural compatibility for every global state in S 1 × S 2 . This algorithm incrementally propagates the compatibility between neighbouring states using backward and forward processing. Such a propagation relies on the intuition that two states are compatible if their backward and forward neighbouring states are compatible.

The flooding algorithm returns a matrix CM k CN,D . Each entry CM k CN,D [s 1 , s 2 ], stands for the compatibility measure of global state (s 1 , s 2 ) at the k th iteration. The parameter CN refers to the considered compatibility notion, which is checked using either an unidirectional (D = →) or a bidirectional (D = ↔) protocol traversal. CM 0 CN,D represents the initial compatibility matrix where all states are supposed to be perfectly compatible, i.e., ∀(s

1 , s 2 ) ∈ S 1 × S 2 , CM 0 CN,D [s 1 , s 2 ] = 1. In order to compute CM k CN,D [s 1 , s 2 ], we define two functions, obs-comp k CN,D
and state-comp k CN,D detailed as follows. The first function, observational compatibility, computes the compatibility of outgoing and incoming observable transitions. The second function, state compatibility, propagates the compatibility from the forward and backward neighbouring states to (s 1 , s 2 ), taking into account τ transitions and observational compatibility. The compatibility propagation is also parametrised according to the parameter D. In this article, we only present the forward compatibility, as the backward compatibility is handled in a similar way.

Before defining obs-comp k CN ,D , we present a few functions necessary to its computation. Given a state s ∈ S and a transition relation T , we define the set of emissions, receptions, and forward transitions from s as follows: 5 We assume that message names match if they are synonyms according to the Wordnet similarity package [START_REF] Pedersen | Wordnet::similarity -measuring the relatedness of concepts[END_REF].

E(s, T ) = {t ∈ T | t = (s, (m, !, pl), s )} R(s, T ) = {t ∈ T | t = (s, (m, ?, pl), s )} Fw (s, T ) = E(s, T ) ∪ R(s, T )
We let tau(s, T ) = {t ∈ T | t = (s, τ, s )} denote the set of τ -transitions emanating from a state s. We define the function sum k CN ,D ((s 1 , s 2 ), T 1 , T 2 ) as the sum of the best compatibility degree of forward neighbours of state s 1 and those of state s 2 :

sum k CN ,D ((s 1 , s 2 ), T 1 , T 2 ) =        (s1,l1,s 1 )∈T1 max (s2,l2,s 2 )∈T2 (lab-comp(l 1 , l 2 ) • CM k-1 CN,D [s 1 , s 2 ]) if |Fw (s 1 , T 1 )| = 0 and |(Fw (s 2 , T 2 )| = 0 0 otherwise
We are now able to define the function obs-comp k CN,D according to the UR and UC notions presented in Section 3. Unspecified Receptions. For a global state (s 1 , s 2 ), obs-comp k UR,↔ returns 1 if there are no emissions from the states and they are deadlock free, and otherwise recursively measures the best compatibility of emissions with receptions, taking the compatibility of the states reached into account: Definition 2. Given a global state (s 1 , s 2 ), the observational compatibility is computed wrt. the UR compatibility notion as follows:

obs-comp k U R,↔ ((s 1 , s 2 )) =            1 if E(s 1 , T 1 ) ∪ E(s 2 , T 2 ) = ∅ and (s 1 , s 2 ) ∈ DF 0 if (s 1 , s 2 ) / ∈ DF 1 |E(s1,T1)|+|E(s2,T2)| • sum k U R,↔ ((s 1 , s 2 ), E(s 1 , T 1 ), R(s 2 , T 2 )) + sum k U R,↔ ((s 2 , s 1 ), E(s 2 , T 2 ), R(s 1 , T 1 )) otherwise
Unidirectional Complementarity. We compute how well one state s er (in the complementer protocol) complements the state s ed (in the complemented protocol).

The comparison returns 1 if there is a subset of outgoing observable transitions in Fw (s er , T er ) such that their respective labels are perfectly compatible with those of transitions in Fw (s ed , T ed ). Additionally, these transitions must lead into compatible states. If there is a deadlock, then this function returns 0. Otherwise, obs-comp k U C,→ ((s er , s ed )) measures the best compatibility of every transition label in Fw (s er , T er ) with those in Fw (s ed , T ed ), leading to the neighbouring states which have the highest compatibility degree: Definition 3. For a global state (s er , s ed ), the observational compatibility is computed wrt. the UC compatibility notion as follows, for T ed = Fw (s ed , T ed ) and T er = Fw (s er , T er ):

obs-comp k U C,→ ((s er , s ed )) =        1 if sum k U C,→ ((s ed , s er ), T ed , T er ) = |Fw (s ed , T ed )| and (s ed , s er ) ∈ DF 0 if (s ed , s er ) / ∈ DF sum k U C,→ ((s ed ,ser),T ed ,T er ) max(|T ed |,|T er |)
otherwise

As far as τ transitions are concerned, we define the function fw-propag k CN ,D , D ∈ {↔, →}, which handles these internal behaviours based upon either a bidirectional or unidirectional compatibility propagation: Bidirectional Compatibility. Here, compatibility is computed from both services' point of view. That is, for a given global state (s 1 , s 2 ), we compute the compatibility of the forward neighbours of s 1 with those of s 2 and vice-versa. For each τ transition, fw-propag k CN ,↔ must be checked on the target state, and observable transitions out of (s 1 , s 2 ) are compared using obs-comp k CN,↔ :

Definition 4. Given a global state (s 1 , s 1 ):

fw-propag k CN,↔ ((s 1 , s 2 )) = d-fw-propag k CN,↔ ((s1,s2))+d-fw-propag k CN,↔ ((s2,s1)) 2 d-fw-propag k CN,↔ ((s 1 , s 2 )) =    (s 1 ,τ,s 1 ) ∈T 1 fw-propag k CN,↔ ((s 1 ,s2)) |tau(s1,T1)| if tau(s 1 , T 1 ) = 0 and |Fw (s 1 , T 1 )| = 0 (s 1 ,τ,s 1 ) ∈T 1 fw-propag k CN ,↔ ((s 1 ,s2))+obs-comp k CN ,↔ ((s1,s2)) |tau(s1,T1)|+1 otherwise Unidirectional Compatibility. To compute fw-propag k CN,→ ((s 1 , s 2 ))
, from the point of view of s 2 as the complemented state, we first follow any τ -transitions from s 1 , and if there are no such transitions, 6 then we follow any τ -transitions from s 2 . Measuring the compatibility after every τ -transition enables us to check whether this protocol is able to fulfil its partner requirements at the target state: Definition 5. Given a global state (s 1 , s 2 ):

fw-propag k CN,→ ((s 1 , s 2 )) =    ( (s 1 ,τ,s 1 )∈T 1 fw-propag k CN,→ ((s 1 ,s2)))+obs-comp k CN,→ ((s1,s2)) |tau(s1,T1)|+1 if tau(s 1 , T 1 ) = ∅ ( (s 2 ,τ,s 2 )∈T 2 fw-propag k CN,→ ((s1,s 2 )))+obs-comp k CN,→ ((s1,s2)) |tau(s2,T2)|+1
otherwise State Compatibility. We compute the weighted average of three measures, forward and backward compatibility and state nature:

state-comp k U C,→ (s 1 , s 2 ) = w1•fw-propag k U C,→ (s1,s2)+w2•bw-propag k U C,→ (s1,s2)+nat(s1,s2) w1+w2+1
where the weights w 1 and w 2 denote the number of best matches found among the outgoing and incoming, respectively, transition labels in states s 1 and s 2 . Compatibility Flooding. Finally, the compatibility degree of (s 1 , s 2 ) at the k th iteration is computed as the average of its previous compatibility at the (k -1) th iteration and the current state compatibility: Example 6. The table in Fig. 4 (right) shows the matrix obtained, after 7 iterations, for the example depicted according to the UC notion. Let us comment on the compatibility of states c0 and s0. The measure is quite high because both states are initial and the emission seek! at c0 perfectly matches the reception search? at s0 (they are WordNet synonyms). However, the compatibility degree is less than 1 due to the backward propagation of the deadlock from the global state (s1, c3) to (s1, c1), and then from (s1, c1) to (s0, c0).

CM k CN,D [s 1 , s 2 ] = CM k-1 CN,D [s1,s2]+state-comp k CN,D ((s1, s2
Convergence. In appendix, we give a detailed formal proof that the computation described here always converges to a unique compatibility matrix CM CN,D . The argument is based on the fact, proven in the supplement, that the function on matrices defined in this section is a contraction, hence by Banach's fixed point theorem, it converges to a unique fixed point. For practical purposes, our iterative process is terminated when the Euclidean metric

ε k = |CM k CN,D -CM k-1 CN,D
| goes beyond a pre-determined threshold. Mismatch Detection. Our compatibility measure also returns a list of mismatches which identifies the incompatibility sources, e.g., unmatched message names, different state natures or unshared parameter types. For instance, the states s0 and c1 in Fig. 4 present several mismatches, e.g., s0 is initial while c1 is not, and their outgoing transition labels have the equal directions. Extensibility. Our approach is generic and can be easily extended to integrate other compatibility notions. Adding a compatibility notion CN only requires to define a new function obs-comp k CN,D , where D ∈ {→, ↔}.

Analysis of Compatibility Measures

In this section, we first present how total protocol compatibility can be computed from the matrix. In the case of incompatible services, we propose some techniques for computing a global compatibility measure. Compatible Protocols. Our flooding algorithm ensures that every time a mismatch is detected in a reachable global state, its effect will be propagated to the initial states. Hence, the forward and backward compatibility propagation implies that protocols are compatible if and only if their initial states are also compatible, i.e., CM CN,D [I 1 , I 2 ] = 1. Such information is useful, e.g., for automatically selecting available services in order to compose them. Global Protocol Compatibility. The global compatibility measure helps to differentiate between services that are slightly incompatible and those which are totally incompatible. This is useful to perform a first service selection step in order to find some candidates among a large number of services. Seeking for services with high global compatibility degree enables to simplify further processing to resolve their interface incompatibility, e.g., using service adaptation [START_REF] Mateescu | Adaptation of service protocols using process algebra and on-the-fly reduction techniques[END_REF].

The global compatibility can be computed differently depending on the user preferences. A first solution consists in computing the average of the maximal compatibility degrees computed for all states. An alternative, shown in Algorithm 1, is to compute the global compatibility degree as the average of all compatibility degrees that are higher than or equal to a threshold t. To account for unmatched states, we multiply this average by the rate of states which have at least one possible matching with compatibility degree higher than t.

Algorithm 1 computes the global compatibility measure from one STS's point of view, and this works for the unidirectional compatibility notions. For the bidirectional compatibility notions, the global compatibility is computed as the average of the values returned by both functions global-comp(S 1 , S 2 , CM CN,D , t) and global-comp(S 2 , S 1 , CM CN,D , t). Example 7. This example illustrates the computation of the global compatibility degree for the online store system of Fig. 4. Given a threshold t = 0.7 and the matrix of Table 4, the application of Algorithm 1 returns a global compatibility degree of 0.6. This rather low measure is justified by the state mismatch at c1 of the Customer protocol, which does not match with any state of the O-Store protocol (all compatibility values are below the threshold).

We can now also finish our example from the introduction, cf. Fig. 1. As this is a client-server setting, we compute compatibility using the UR notion. Using our tool Comparator and a threshold of 0.7 as above, we can compute the three MedServers' compatibility degrees with the Client service to 0.55, 0.85, and 0.76, respectively, hence preferring MedServer1 over the other two.

Tool Support

Our approach for measuring the compatibility degree of service protocols has been fully implemented in a prototype tool called Comparator [START_REF]Comparator web[END_REF]. The framework architecture is given in Fig. 5. The tool, implemented in Python, accepts as input two XML files corresponding to the service interfaces and an initial configuration, i.e., the compatibility notion, the checking direction, and a threshold t. The tool returns the compatibility matrix, the mismatch list, and the global compatibility degree which indicates how compatible both services are. The implementation is highly modular, which makes easy its extension with new compatibility notions or other strategies for comparing message names and parameters. The tool can be used through a Web application [START_REF]Comparator web[END_REF].

We have validated our prototype tool on more than 110 examples, ranging from small ones, to experiment boundary cases, to real-world examples, e.g., a car rental [START_REF] Cubo | A model-based approach to the verification and adaptation of WF[END_REF], a travel booking system [START_REF] Mateescu | Adaptation of service protocols using process algebra and on-the-fly reduction techniques[END_REF], a video-on-demand application [START_REF] Poizat | An Adaptation-based Approach to Incrementally Build Component Systems[END_REF], music player system [START_REF] Poizat | An Adaptation-based Approach to Incrementally Build Component Systems[END_REF], a medical management system [START_REF] Cámara | Interactive specification and verification of behavioural adaptation contracts[END_REF], and a multi-function device service [START_REF] Salaün | Generation of Service Wrapper Protocols from Choreography Specifications[END_REF]. Many case studies are available online at [START_REF]Comparator web[END_REF] and present the results of our approach for quantifying the compatibility.

Our experiments have shown that, even though efficiency was not our main concern in the application, Comparator can compute the compatibility degree of quite large systems in a reasonable time. Computation time depends on the size of the examples and the number of τ -transitions and loops.

To evaluate the preciseness of our compatibility measure, we have used the well-known precision and recall metrics [START_REF] Salton | Introduction to Modern Information Retrieval[END_REF] to estimate how much the measure automatically computed meets the expected result (see [START_REF]Comparator web[END_REF] for more details). For compatible protocols, our method yields a precision and recall of 100%. For incompatible protocols, we computed precision and recall metrics of 85% / 95% for the car rental example [START_REF] Cubo | A model-based approach to the verification and adaptation of WF[END_REF] and 91% / 100% for a flight advice system [START_REF]Comparator web[END_REF]; all other examples of our database returned values above 90% for both metrics. between them, until reaching final states. This notion is too weak since it does not guarantee deadlock-freeness for service composition. The authors compute the compatibility degree of two services as the average of the number of successful transition sequences. Neither detailed compatibility of different protocol states nor the mismatch list is returned. Edit Distance. In [START_REF] Aït-Bachir | Measuring similarity of service interfaces[END_REF][START_REF] Lohmann | Correcting deadlocking service choreographies using a simulation-based graph edit distance[END_REF], the authors calculate the edit distance between a given defective service and synthesised correct services. They also detect the differences between two versions of one service interface described using finite state machines. The quantitative simulation measures the state similarity based on the analysis of outgoing transition labels without any semantic comparison of these label names, and there is no propagation of compatibility between neighbouring states. Similarity Flooding. In [START_REF] Melnik | Similarity flooding: A versatile graph matching algorithm and its application to schema matching[END_REF], the similarity flooding technique was applied to the problem of model matching. This algorithm returns a matrix for the similarity propagation which is updated iteratively. The authors propose a set of metrics to measure correspondences between elements of data structures such as data schemas or data instances, described with LTSs. This work aims at assisting developers in matching elements of a schema by suggesting candidates. However, their tool does not enable fully automated matching. More recently, [START_REF] Nezhad | Protocol-aware Matching of Web Service Interfaces for Adapter Development[END_REF] propose a semi-automated approach for checking the matching of messages in two business process models such that the computed values can be updated depending on the user feedback. The authors combine a depth and flooding-based interface matching for measuring the behavioural compatibility of two interacting protocols. This work aims at detecting the message merge/split mismatch in order to help the automatic specification of adaptation contacts. Quantitative Model Checking. The quantitative approach to service compatibility which we advocate here is related to recent quantitative approaches to model checking and verification. Here, Boolean notions of verification are replaced by distances, just as we do here for service compatibility. A general framework for such distance-based quantitative verification has been developed in [START_REF] Fahrenberg | The quantitative linear-time-branching-time spectrum[END_REF]. We summarise in Table 1 the comparison of our approach with the closest related work. 7

Conclusion

To the best of our knowledge, we suggest here the first generic framework for automatically quantifying the compatibility degree of service interfaces. Our measuring method relies on a compatibility flooding algorithm and is parametrised by different compatibility notions. In addition to computing the matrix and the global measure of compatibility, a list of mismatches is returned. Our computation always converges to a unique compatibility matrix.

Our proposal is fully supported by the Comparator tool which has been validated on many examples. We present some of these in a separate appendix; others are available online at [START_REF]Comparator web[END_REF]. The quality of results was measured using precision and recall, showing a low rate of false-positive results.

Our work has straightforward applications to service-related issues, e.g., automatic discovery, selection, ranking, and composition. On a wider scale, our solution can be used to verify all software systems which can be described using STSs. In particular, Comparator has been used in a real-world case study in the context of the ITACA project [START_REF] Cámara | Itaca: An integrated toolbox for the automatic composition and adaptation of web services[END_REF] for service composition and adaptation. Comparator has also been integrated into a prototype tool, called Updator [START_REF] Ouederni | Client update: A solution for service evolution[END_REF], which we implemented to deal with service evolution issues.

Our main perspective is to to apply our compatibility measuring approach for the automatic generation of adaptor protocols. This is a difficult issue, and only few attempts have been made in that direction. As an example, the techniques presented in [START_REF] Martín | Automatic generation of adaptation contracts[END_REF] automate the generation of adaptation contracts for two services by combining graph search algorithms and heuristics. Unfortunately, this approach is costly and imprecise when services do not present only simple mismatches. We believe that by exploiting our method, we should obtain much better results in terms of computation time and relevance of adaptation contracts.

Appendix: Applications

Our compatibility measure can be applied to several domains and can be used for verifying all software systems that can be described using STSs, e.g., Web service and software components. For illustration purposes, we present the application of our detailed measure for solving some applications in service-oriented computing, namely service discovery [START_REF] Zisman | A Framework for Dynamic Service Discovery[END_REF], service adaptation [START_REF] Cámara | Interactive specification and verification of behavioural adaptation contracts[END_REF] and service evolution [START_REF] Ouederni | Client update: A solution for service evolution[END_REF].

A Service Discovery

Service discovery consists in selecting one or more services from a large number of candidates in order to integrate themselves in a second step into a service composition. Discovering compatible services is a hard and error-prone process if this is not assisted using automated techniques. In most cases, there is no compatible service and we are interested in finding the most compatible one in order to simplify, for instance, the adaptation techniques (see Section B) that can be used for solving mismatch issues.

Service discovery consists of the following steps: First, the providers advertise their services to a registry (e.g., UDDI for Web services) where these services are stored; second, the requester asks the registry about the available services; third, the registry applies some search techniques in order to determine which service better matches the request.

In this setting, our global compatibility measure simplifies the discovery process in order to find services that are either perfectly compatible, i.e., the global compatibility is equal to 1, or services that are mostly compatible, e.g., having a high compatibility degree. In the latter case, the selection process relies on the global measure provided by our approach. The detailed compatibility measure, e.g., the compatibility matrix and the mismatch list, can be helpful in a second step for resolving the mismatches (see, for instance, Sections B and C).

Example 8. Let us focus on the example given in Fig. 6 to illustrate the use of our global compatibility degree for service discovery. This example describes an on-line medical management system which handles patient appointments within a health care institution, either with general practitioners, or specialist doctors. The Client can first log on to a server by sending his/her user name and password (login!). Then, he/she asks for an appointment with a general practitioner (reqDoc!) and receives an appointment identifier. We present three services for the medical server, namely, MedServer0, MedServer1, and MedServer2 which are slightly different, yet they all can receive the patient name and password. Next, they can receive, and reply to, a request for an appointment with either a general practitioner (reqDoc?) or a specialist doctor (reqSpec?).

Considering the UR notion, the global compatibility degree for Client and the three possible medical servers MedServer0, MedServer1, and MedServer2 is equal to 0.55, 0.85, and 0.76, respectively. Note that without our measure, it is not obvious even for such a simple example to distinguish which service better matches the client requirements. However, using our results, we can decide to select MedServer1 instead of MedServer0 or MedServer2. Client presents only a parameter mismatch with MedServer1 (the usr parameter is defined using a different type in the two interfaces). In contrast, Client can deadlock with MedServer2, i.e., due to the internal τ action (corresponding to a termination after a timeout). Client and MedServer0 present several mismatches (message names and number). Generally speaking, the highest global compatibility degree corresponds to the lowest number of mismatches between the two interfaces. In our example, the parameter issue in the client protocol is much easier to resolve than the deadlock problem, particularly because we cannot modify the servers, assuming a black-box hypothesis.

B Service Adaptation

Adaptation aims at computing an intermediate service -called adaptor -to resolve mismatches presented between services interacting with each other. An adaptor describes composition constraints and adaptation requirements among these services and is built from abstract descriptions -called contracts -of how interface mismatches can be worked out.

The work given in [START_REF] Cámara | Interactive specification and verification of behavioural adaptation contracts[END_REF] proposes a graphical environment -called ACIDE -for interactive contract specification using our compatibility measure. Note that, so far, ACIDE only considers the UR compatibility notion. The graphical notation for a service interface in ACIDE includes a representation of behavioural models (STSs) and a collection of ports. Each label on the STS corresponds to a port in the graphical description of the interface. Ports include a data port for each parameter contained in the parameter list of the label. Correspondences between the different service interfaces are represented as port bindings and data port bindings. Starting from the graphical representation of the interfaces, the architect can build a contract between them by successively connecting ports and data ports. This results in the creation of bindings which specify how the interactions should be carried out between the services. Example 9. Fig. 7 shows the graphical presentation of the STSs given in Fig. 6 in the main paper. 8In order to specify the adaptation contract in ACIDE, our compatibility measure can be used in different ways. Firstly, it is possible to automatically generate port bindings for labels that perfectly match.

Example 10. Considering the STSs presented in Fig. 6 in the main paper, the result of automatic port binding is shown in Fig. 8.

In ACIDE, the user can also select a transition label l in one protocol (we call s its source state in the rest of this paragraph), and then Comparator is used to return the best label matching in the other protocol. Note that Comparator can return several possible matchings for either states or labels that are compatible with each other in a partner service. This is similar to the simulation (preorder) relation in concurrency theory [START_REF] Cleaveland | Equivalence and preorder checking for finite-state systems[END_REF] where several states can be simulated by one state. In this case, designer intervention is required to decide which bindings should be kept (See Example 12 for illustration). To do so, two functions have been implemented where: (i) the first function labels all states in the other protocol with compatibility measures between s and every state in the partner interface, and (ii) the second function seeks the highest value (s, s j ) in the matrix (where s j is a partner state) and returns the label going out from s j the most compatible with l. These functions can be completed with other alternatives such as returning the best label matching for each state in the partner, or for each state whose compatibility measure with respect to s is higher than a threshold t. To highlight these results in the graphical interface, ACIDE does not only display the compatibility measures but also colour in red the best matchings.

Example 11. Fig. 9 shows the binding result returned for state s0 in the O-Store protocol with all states of the Customer protocol given in Fig. 6 in the main paper. As we can observe, s0 matches the initial state c0 on Customer with which it has the highest compatibility value equal to 92.9%. Based on this highest state compatibility measure, the labels going out from s0 will be matched with the most compatible labels going out from c0. We recall that label binding can be done manually based on the measure of label compatibility or following the automatic binding as presented in Fig. 8.

Example 12. Let us focus on the example given in Fig. 10 to illustrate how our global compatibility degree can yield a false-positive evaluation considering service adaptation. This example describes an on-line medical management system [START_REF] Cámara | Interactive specification and verification of behavioural adaptation contracts[END_REF] which handles patient appointments within a health care institution, either with general practitioners or specialist doctors. We present two versions of the Medical Server, namely MedServer0 and MedServer1 which are slightly different. MedServer0 starts with receiving the patient login (connectL?) and then his/her password (connectP?), while MedServer1 expects to receive the password at its initial state. Next, both can receive, and reply to, a request for an appointment with either a general practitioner (reqDoc?) or a specialist doctor (reqSpec?). The Client sends his/her password followed by his/her user name. Then, the Client asks for an appointment with a general practitioner (reqDoc!) and receives an appointment identifier.

Considering the UR notion, the global compatibility degree for MedServer0 and MedServer1 with Client is equal to 0.49 and 0.68, respectively. Based on our compatibility measure, one would prefer to adapt MedServer1 with Client. However, the adaptation does not work in this case to resolve the missing parameter issue (i.e., usr is missing in MedServer1 but present in Client). In the other case, although both MedServer0 and Client return a lower value, these can be adapted using message reordering techniques such as those proposed in [START_REF] Mateescu | Adaptation of service protocols using process algebra and on-the-fly reduction techniques[END_REF].

C Service Evolution

We now present another application of our compatibility measure, namely, service evolution. Although many efforts have been devoted by researchers for automating service adaptation, this solution cannot be applied in some cases, e.g., the types of sent and received parameters mismatch, yet type conversion is not allowed. Therefore, services interfaces should be changed in order to work out such interoperability issues.

The remainder of this section shows how our compatibility measure is used to resolve the interface mismatches and make a service and its client (user application) compatible. To this end, we consider the UC notion for illustration purposes such that the client and the service represent the complemented and the complementer partners, respectively. In the following, we present the intuition behind the application and we refer the readers to [START_REF] Ouederni | Client update: A solution for service evolution[END_REF] for technical details. The application is automated by a prototype tool (called Updator).

Overview of the Client Update Process. In order to resolve the incompatibility issues, an automated process to change the client interface has been proposed, and this is shown in Fig. 11. In step 1, it computes the compatibility measure which compares both interfaces. Then, step 2 relies on the resulting compatibility matrix to generate an interface mapping tree which describes the best state matching on both interfaces. Based on the analysis of the mapping tree, the client interface is Fig. 11. Overview of our Client Update Process modified as follows. In step 3, behavioural mismatches are resolved, e.g., addition of missing transitions or removal of mismatching transitions to and from the client interface. Steps 4 and 5 compute the interface compatibility and the mapping tree again in order to take the changes made in the previous step into account. The resulting mapping tree describes 1-to-1 state mapping, where every state on one interface has its corresponding matching state on the other interface. By doing so, in step 6, the updated tree is considered to resolve the static mismatches, which can be presented between labels of transitions going out from matched states. Lastly, after resolution of interface mismatches, step 7 computes the compatibility measure to validate that the updated client has become compatible with its service interface. At this very last step, a new iteration starts from step 2 if the interface compatibility is achieved yet the user requirements are not satisfied. Otherwise, the update process terminates here.

Note that the interface mapping tree describes a set of linked nodes where each node represents the best matching of a client state with one state among those on the service interface. Furthermore, each node is linked to its parent and children nodes.

The update process can be parametrised by a set of user requirements to prevent undesirable behaviours that the designer does not want to appear in the new client interface. These requirements consist of a set of messages which must not appear in the updated interface.

Example 13. Let us illustrate the computation of an interface mapping tree from a compatibility matrix and some user requirements. We give in Fig. 12 a simplified example of a database management system where a User (complemented) can access an online Database (complementer) to search data or make an update, and waits for its acknowledgement. The database service first receives a request for an update or a registration to be acknowledged. Unfortunately, the protocols are not compatible.

Let us first suppose an empty set of user requirements. Each node in the mapping tree represents a User state with its best state match among those in Database. the update process changes the User protocol into User', which is compatible with Database protocol.

We now suppose a non-empty set of user requirements, which is equal to {ackR}, i.e., the user does not want to receive the registration acknowledgement. The computation of the mapping tree returns a deadlock node (represented by the dashed rectangle in Fig. 12). This node does not have any child because the message ackR! going out from state s3 cannot be matched with any message at state c2 due to the restriction made by the user requirements. Thus, no compatible user interface can be generated using this interface mapping tree.

Resolution of Behavioural Mismatches. An interface mapping tree is used for resolving the behavioural mismatches. The techniques aim at ensuring the 1-to-1 state matching from the client viewpoint. To do so, several systematic changes can be made using pre-defined patterns. The very first pattern is referred to as add/remove states and enables us to check whether one or more client states must be removed if they have no match on the service interface. This pattern makes it also possible to add states to the client interface if there exist service states with no match. The top of Fig. 13 illustrates an example where the service's state s2 does not have any match in Int clt . Note that states s1 and s3 match states c1 and c2, respectively. Thus, since s2 is the successor of s1 and also the predecessor of s3, the client change consists in adding a new state to be matched with s2.

Add/remove states may lead to another pattern called merge/split transitions where transitions can be removed or added. This behavioural change deals with the protocol information in order to keep it coherent wrt. the predecessor and successor behaviour of a removed or added transition. For instance, the bottom of Fig. 13 shows that there are two search transitions on the service protocol matching one search transition on the client interface. To resolve this mismatch, the client search transition is split into two transitions. Regarding the rest of the client protocol, here the client behaviour starting from state c2, the link of such a state with its successors is updated, considering the added state c3. Resolution of Static Mismatches. The mismatch list computed by Comparator is used to resolve the static mismatches. Such mismatches concern either state nature or labels. Here, three possible changes are applied: (i) unifying the nature of matched states; (ii) renaming transition labels; or (iii) updating the signature and the alphabets with new labels and operation profiles. We have shown that lab-comp(l 1 , l 2 ) M 1 (s 2 , s 1 ) -M 2 (s 2 , s 1 )

F (M 1 ) -F (M 2 ) ≤ 1 2 max i,j |M ij 1 -M ij 2 | + 1
≤ 1 n j max i |M ij 1 -M ij 2 | ≤ max i,j |M ij 1 -M ij 2 | .
This now entails that

F (M 1 ) -F (M 2 ) ≤ 1 2 max i,j |M ij 1 -M ij 2 | + 1 2 w1+w2 w1+w2+1 max i,j |M ij 1 -M ij 2 | = λ M 1 -M 2 ,
which is what was to be shown.

Fig. 3 .

 3 Fig. 3. Compatibility measuring process.

Fig. 4 .

 4 Fig.[START_REF] Cámara | Interactive specification and verification of behavioural adaptation contracts[END_REF]. STSs of online store system (left) and associated compatibility matrix.

Fig. 5 .

 5 Fig. 5. Comparator architecture.

Fig. 6 .

 6 Fig. 6. STSs of a Medical Management System.

Fig. 7 .

 7 Fig. 7. Online Store (II) Graphical Presentation in ACIDE.

Fig. 8 .

 8 Fig. 8. Label-based Matching in ACIDE.

Fig. 9 .

 9 Fig. 9. State-based Matching in ACIDE.

Fig. 10 .

 10 Fig. 10. STSs of a Medical Management System.

Fig. 12 .

 12 Fig. 12. Database Management System.

Fig. 13 .

 13 Fig. 13. Patterns: Add State and Split Transitions (top), Add State and Split Transitions (bottom)

τ →s 1 fwτ →s 1 obsτ →s 1 obs

 111 sequences of τ -transitions: assuming tau(s 2 ) = ∅ for now, we havefw-propag U C,→ (M )(s 1 , s 2 ) = obs-comp U C,→ (M )(s1,s2) |tau(s1)|+1 + s1 -propag U C,→ (M )(s 1 ,s2) |tau(s1)|+1 = obs-comp U C,→ (M )(s1,s2) |tau(s1)|+1 + s1 -comp U C,→ (M )(s 1 ,s2) (|tau(s1)|+1)(|tau(s 1 )|+1) U C,→ (M )(s 1 ,s2) (|tau(s1)|+1)(|tau(s 1 )|+1) = • • • , thus, fw-propag U C,→ (M 1 )(s 1 , s 2 ) -fw-propag U C,→ (M 2 )(s 1 , s 2 ) = obs-comp U C,→ (M1)(s1,s2)-obs-comp U C,→ (M2)(s1,s2) |tau(s1)|+1 + s1 -comp U C,→ (M1)(s 1 ,s2)-obs-comp U C,→ (M2)(s 1 ,s2) (|tau(s1)|+1)(|tau(s 1 )|+1) lifting the assumption that tau(s 2 ) = ∅, we see that|fw-propag U C,→ (M 1 )(s 1 , s 2 ) -fw-propag U C,→ (M 2 )(s 1 , s 2 )| ≤ max s 1 ,s2|obs-comp U C,→ (M 1 )(s 1 , s 2 ) -obs-comp U C,→ (M 2 )(s 1 , s 2 )| .

  U C,→ (M 1 ) ij -obs-comp U C,→ (M 2 ) ij | . Now to bound |obs-comp U C,→ (M 1 )(s 1 , s 2 ) -obs-comp U C,→ (M 2 )(s 1 , s 2 )| from above, we see that its maximum is attained when both values fall in the last case of (9), and then|obs-comp U C,→ (M 1 )(s 1 , s 2 ) -obs-comp U C,→ (M 2 )(s 1 , s 2 )| = |sum U C,→ (M )(s2,s1,Fw (s2),Fw (s1))-sum U C,→ (M )(s2,s1,Fw (s2),Fw (s1))| max(|Fw (s2)|,|Fw (s1)|) (l 1 , l 2 ) M 1 (s 2 , s 1 ) (l 1 , l 2 ) M 2 (s 2 , s 1 )

Table 1 .

 1 A Summary of Approaches Based on Quantitative Behavioural Analysis.

	Model	Messages and protocols Value-passing Internal actions	[15] √ × ×	[25] √ × ×	[11] √ × ×	[1] √ × ×	[27] √ × √	[16] √ × ×	Our approach √ √ √
		Description language Statechart	LTS	Finite Automaton	FSM	π-calculus	FSM	STS
	Analysis	Issue Notion(s) Message semantics	Similarity BIS √	Similarity (WK) SIM/BIS ×	Similarity WK SIM ×	Similarity SIM ×	Compatibility Compatibility Compatibility OP DF UR/UC/. . . × √ √
		Processing	Iterative	Simple	Simple	Simple	Simple	Iterative
	Computation

We shall introduce symbolic transition systems more formally in Section 2.

Given that we have excluded τ -loops, this will eventually be the case.

√ √ √ √ √

BIS, SIM, WK, and OP abbreviate bisimulation, simulation, weak, and one path, respectively.

In this example, the Wordnet similarity package is omitted and the seek! label is renamed into search!.

Related work

We present several related approaches to measuring similarity or compatibility of interfaces. These are applied for service substitution and composition, respectively. Protocol Traversal. The work in [25] measures the similarity of two computer viruses described using labelled transition systems (LTSs). It uses quantitative functions which are computed by a simple (not iterative) forward traversal of two LTSs. This work does not return the differences which distinguish one service from another, and there is no computation of a global similarity degree. In [27], the authors check the compatibility of two services described using the π-calculus.

Here, two services are compatible if there is always at least one transition sequence

Appendix: Proof of Convergence

In this appendix we provide a detailed proof that our algorithm for computing behavioural compatibility between services converges in a finite number of steps, regardless of its input.

We show the proof for unidirectional complementarity only; it is similar for the other notions. For ease of reference, we repeat the relevant equations from Section 4.2:

Let F : [0, 1] n×n → [0, 1] n×n be the function defined by equations (1) to (5) above, i.e.

Let λ = 1 2 (1 + w1+w2 w1+w2+1 ), then λ < 1. We show that F is λ-Lipschitz continuous, hence a contraction. Banach's fixed-point theorem then ensures that F has a unique fixed point and that the iteration given by equations ( 6) to [START_REF] Hennessy | Symbolic Bisimulations[END_REF] in finitely many steps reaches the fixed point with arbitrary precision.

We use the max-metric for matrices, i.e.

and as the formulas for fw-propag U C,→ and bw-propag U C,→ are entirely analogous, we can assume that

w1+w2+1 fw-propag U C,→ (M 1 ) -fw-propag U C,→ (M 2 ) .

To obtain an upper bound for fw-propag U C,→ (M 1 ) -fw-propag U C,→ (M 2 ) , we note that fw-propag U C,→ (M )(s 1 , s 2 ) essentially computes a weighted average of obs-comp U C,→ (M )(s 1 , s 2 ) for all states s 1 , s 2 reachable from s 1 , resp. s 2 , by


Joanne M Atlee
email: jmatlee@uwaterloo.ca

Uli Fahrenberg
email: ulrich.fahrenberg@inria.fr

Axel Legay
email: axel.legay@inria.fr

Measuring Behaviour Interactions between Product-Line Features

We suggest a method for measuring the degree to which features interact in feature-oriented software development. We argue that our method is practically feasible, easily extendable and useful from a developer's point of view.

I. INTRODUCTION

The behaviour of a software system is often described in terms of its features, where each feature is a unit of functionality that adds value to the system. Feature-oriented software development (FOSD) is a software-development strategy that is based on feature decomposition and modularity. Features can be separate modules that are developed in isolation, allowing for parallel, incremental, or multi-vendor development of features. Feature orientation is particularly important in software product lines, where a family of related products is managed and evolved in terms of its features: a product line comprises a collection of mandatory and optional features, and individual products are derived by selecting among and integrating features from this feature set. A product line can be expressed as a single model, in which feature-specific behaviour is conditional on the presence of the feature in a product.

The downside of FOSD is that, although features are conceptualized, developed, managed, and evolved as separate concerns, they are not truly separate. They can interact with each other, for example by trying to control the same variables or external phenomena, by issuing events that trigger the other feature, or by affecting conditions that suppress the other feature. In general, there is a behaviour interaction whenever the behaviour of a feature deviates from its specification due to the presence of other features.

A number of researchers have investigated the automatic detection of feature interactions ( [START_REF] Apel | Detecting dependences and interactions in feature-oriented design[END_REF], [START_REF] Calder | Feature interaction: a critical review and considered forecast[END_REF], [START_REF] Calder | Feature interaction detection by pairwise analysis of LTL properties -A case study[END_REF], [START_REF] Dominguez | Feature interaction detection in the automotive domain[END_REF], [START_REF] Jayaraman | Model composition in product lines and feature interaction detection using critical pair analysis[END_REF], [START_REF] Scholz | Automatic detection of feature interactions using the Java modeling language: an experience report[END_REF], etc.). The primary result of such analyses is effectively a boolean determination of whether a combination of features interact. The formulation of the result may be different for different tools (e.g., returning the set of features that interact with a given feature f ; or returning the combinations of features, from a given feature set, that interact). Some techniques may also report a witness execution trace that manifests a detected interaction, to help the developer understand exactly how the features interact -as a first step towards addressing the interaction. But the essence of the analyses is to report simply the presence or absence of interactions.

We are interested in exploring how to measure the degree to which features interact. Features may have multiple interactions, where each interaction instance represents work for the developer: specifically, the interaction must be analyzed to determine if it is a problem; if so, then a patch must be designed, implemented, and tested. Thus, a measure of the number of ways in which features in a product line can interact would tell the developer more about the amount of effort needed to integrate features -or suggest that certain combinations of features should be prohibited -than a simple interaction-existence check provides.

We first provide an overview of our models of features, products, and product lines, and how to use bisimulation to detect the presence of feature interactions [START_REF] Shaker | Behaviour interactions among product-line features[END_REF]. We then explore some ideas for computing richer measures that better reflect the degree to which features interact. We also consider how these measurements can be performed efficiently over a model of the product line, by computing metrics for each feature simultaneously and taking advantage of the commonalities among products.

II. FEATURES, PRODUCT LINES, AND INTERACTIONS

A software system is modelled as a transition system (TS) [START_REF] Baier | Principles of model checking[END_REF], which, for simplicity, we consider to be a set of states, and a set of transitions between states that are triggered by actions.

Definition 1 A transition system (TS) S = (S, Σ, I, T ) consists of a set of states S, a set of initial states I ⊆ S, a set of actions Σ, and a set of transitions T ⊆ S × Σ × S. We write s a -→ s to indicate that (s, a, s ) ∈ T .

We follow [START_REF] Classen | Featured transition systems[END_REF] and consider a feature to be an optional unit of behaviour that is modelled as transitions that are conditional on the presence of the feature. Let N be a set of features.

B(N) denotes the set of Boolean expressions over N .

Definition 2 A featured transition system (FTS) F = (S, Σ, I, T, γ) consists of a TS (S, Σ, I, T ) and a mapping γ : T → B(N). For s, s ∈ S in a FTS and p ⊆ N , we write

s a -→ p s if s a -→ s and p |= γ(s, a, s ).
Example 1 Figure 1 displays a FTS model of an ATM which we will use as running example. The base feature B, whose

0 1 2 3 4 5 card PIN amount cash card [¬R] rec [R] card [R] dep [D] cancel [C] cancel [C] cancel [C] more [M ∧ ¬R] more [M ∧ R]
Fig. 1. FTS F modelling an ATM presence we have not indicated for sake of brevity, consists of a cycle of card insertion, PIN entrance, amount specification, cash retrieval, and card retrieval. Optional features allow for cancellation, cash deposit, more than one transaction, and obtaining a receipt. This last "R" feature is interesting, as it not only adds new behaviour to the ATM but also disables other behaviour.

In order to identify a feature interaction, we look for a discrepancy between a feature's behaviour in isolation versus its behaviour in the presence of other features. To do this, we need to be able to refer to a feature's behaviour within a larger product. We use projection over an FTS [START_REF] Classen | Featured transition systems[END_REF]:

Definition 3
The projection over an FTS F = (S, Σ, I, T, γ) with respect to a feature expression φ ∈ B(N) is the FTS π φ (F) = (S, Σ, I, T , γ ), given by γ (t) = γ(t) ∧ φ and

T = {t ∈ T | γ(t) ∧ φ = ∅}.
If φ = {p} contains but a single product, we can forget about γ in the projection (as we will have γ (t) = p for all t ∈ T ), hence single-product projections, which we also will denote π p (F), can be seen as plain TS.

As shown in [START_REF] Shaker | Behaviour interactions among product-line features[END_REF], discrepancy in behaviours can be detected using bisimulation [START_REF] Milner | Communication and concurrency[END_REF]. Formally, a behaviour interaction is a violation of bisimilarity between the behaviours of a feature f in isolation and the behaviours of f when integrated with other (interacting) features. Violation of bisimilarity encompasses a number of specific types of interactions (e.g., conflicting actions, introduced nondeterminism, shared-trigger interactions [START_REF] Kolberg | Feature interactions in services for internet personal appliances[END_REF], missed-trigger interactions [START_REF] Kolberg | Feature interactions in services for internet personal appliances[END_REF]), thereby enabling a single analysis to detect a wide variety of interactions. Definition 4 Given an FTS F, a product p ⊆ N , and a feature f ∈ N , we say that f has a behaviour interaction with p if π p (F) and π p (π p∧f (F)) are not bisimilar.

Example 2 We want to know whether the feature R in the FTS of Fig. 1 has an interaction with the base ATM. The projections are depicted in Fig. 2; note how the green transitions are projected away in π B (π B∧R (F)). We hence check whether π B (F) and π B (π B∧R (F)) are bisimilar, which of course is not the case, as state 4 misses the card transition of state 4.

In [START_REF] Cordy | Simulation-based abstractions for software product-line model checking[END_REF] it is shown that FTS admit a notion of bisimilarity at FTS level, called featured bisimilarity: Definition 5 The FTS F = (S, Σ, I, T, γ) and F = (S , Σ, I , T , γ ) are featured bisimilar with respect to a product p ⊆ N if there exists a mapping R : S × S → (2 N → {ff, tt}) such that

• ∀i ∈ I : ∃i ∈ I : R(i, i )(p), • ∀i ∈ I : ∃i ∈ I : R(i, i )(p), • if R(s, s )(p), then ∀s a -→ p t : ∃s a -→ p t : R(t, t )(p), • if R(s, s )(p), then ∀s a -→ p t : ∃s a -→ p t : R(t, t )(p).
The following lemma, also from [START_REF] Cordy | Simulation-based abstractions for software product-line model checking[END_REF], then allows to use featured bisimilarity to at once compute all products p with which f has a behaviour interaction. It is shown in [START_REF] Cordy | Simulation-based abstractions for software product-line model checking[END_REF] that this is about 30 times faster than to compute all single bisimilarities.

Lemma 1 FTS F, F are featured bisimilar with respect to p ⊆ N iff the TS π p (F) and π p (F ) are bisimilar.

III. BEHAVIOURAL DISTANCES

We wish to generalize bisimilarity of TS to a notion which not only tells us whether or not two TS are bisimilar, but how close they are to being bisimilar. To this end, Algorithm 1 computes the number of unique behaviours, i.e., the number of behaviours which are present in only one of the two TS.

The intuition is that the algorithm tries to match transitions in one TS as good as possible in the other. Hence the function dist(s, s ) tries to match every transition s a -→ t in S with a transition s a -→ t in S . If no such exists, a missing behaviour is detected and 1 is added to the score; if there are transitions s a -→ t , then distance is recursively computed for the pair t, t with the best match. In the second half of the algorithm, a symmetric match from s to s is computed. Once a pair s, s of states has been checked for behaviour mismatches in this way, it is added to a Passed list of states which need not be checked again; hence the algorithm finishes after at most |S| • |S | iterations.

The behavioural distance faithfully extends bisimilarity:

Algorithm 1 Calculates behavioural distance d(S, S ) between TS S = (S, Σ, I, T ) and S = (S , Σ, I , T )

IV. MEASURING FEATURE INTERACTIONS

We can now use our behavioural distance to measure feature interactions. The following definition of a behaviour interaction score generalizes Definition 4 and allows us to count, algorithmically, the number of behaviour interactions between a feature and a product. Definition 6 Given an FTS F, a product p ⊆ N , and a feature f ∈ N , the behaviour interaction score of f with respect to p is d(π p (F), π p (π p∧f (F)).

Note that by Theorem 1, the behaviour interaction score is 0 iff there is no behaviour interaction.

Example 3 We have already seen that the feature R has a behaviour interaction with the base ATM. To see how many of these are present, we compute d(π

B (F), π B (π B∧R (F))). We have d(0, 0 ) = d(1, 1 ) = d(2, 2 ) = d(3, 3 ) = d(4, 4 ) = 1.
This fits with the intuition that there is precisely one behaviour missing in π B (π B∧R (F)) compared to π B (F), i.e., the feature R has one behaviour interaction with the base ATM. We also want to know how many interactions R has with B ∧ M , i.e. d(π B∧M (F), π B∧M (π B∧M ∧R (F))). The projections are depicted in Fig. 3. We have

d(0, 0 ) = d(1, 1 ) = d(2, 2 ) = d(3, 3 ) = d(4, 4 ) = 2,
as expected: π B∧M (π B∧M ∧R (F)) misses two behaviours compared to π B∧M (F), i.e., the feature R has two behaviour interactions with the product B ∧ M .

Lastly, we count the number of interactions between the all-feature ATMs with and without R, see Fig. 4: d

(0, 0 ) = d(1, 1 ) = d(2, 2 ) + d(4, 4 ) = d(3, 3 ) + d(4, 4 ) = d(4, 4 ) = 2.
We want to lift our behaviour interaction score to FTS level, so that we can compute at once the score of f for all possible products. This generalization is provided by algorithm 2. Intuitively, like algorithm 1, algorithm 2 tries to match transitions in one FTS as good as possible in the other, but for all products p. Hence the Passed list is now a function of products, and at every iteration, the algorithm loops through all products. Note Algorithm 2 Calculates featured behavioural distance fd(F, F ) between FTS F = (S, Σ, I, T, γ) and F = (S , Σ, I , T , γ ) return d that the algorithm returns a function fd which maps products to behavioural distances.

Work in [START_REF] Cordy | Simulation-based abstractions for software product-line model checking[END_REF] shows that the similar algorithm for computing featured bisimilarity can be implemented efficiently; we believe that similar ideas apply to our algorithm for featured behavioural distance.

Theorem 2 For all FTS F, F and all products p ⊆ N , d(π p (F), π p (F )) = fd(F, F )(p).

Proof sketch: Similar to the proof of Theorem 11 in [START_REF] Cordy | Simulation-based abstractions for software product-line model checking[END_REF]: The computations in algorithm 1 can be integrated into a loop over all p ⊆ N , which then can be split like in algorithm 2.

V. VISION

We have shown that it is possible to measure the degree to which features interact in feature-oriented software development. Using a simple but realistic example of a featured transition system, we have seen that the measure we have defined concurs with the intuition.

The measure we have introduced here is but one example of a so-called branching distance between transition systems [START_REF] Fahrenberg | General quantitative specification theories with modal transition systems[END_REF], [START_REF] Fahrenberg | The quantitative linear-time-branchingtime spectrum[END_REF], and many other such distances may be defined. Precisely which of them are useful in FOSD remains to be seen.

Measuring the degree to which features interact in FOSD will be a useful addition to the developer's tool box, allowing her to determine how much integration of a feature affects the overall product line. Our algorithm can easily be extended to also show precisely where the features interact, hence giving visual feed-back to the developer where there may be problems in the model.

Using other and more realistic examples, also expressed with a richer modelling language, we intend to further gauge the usefulness of our behaviour interaction score and other possible measures for feature interaction. For this, it will be useful to devise an efficient implementation of our algorithms.

We note that the algorithms presented in this paper are of a conceptual rather than a practical nature. [START_REF] Cordy | Simulation-based abstractions for software product-line model checking[END_REF] have shown that similar algorithms for determining whether or not there are feature interactions can be implemented efficiently and give experimental evidence on realistic examples. More precisely, they implement their equivalent of our algorithm 2 using iteration instead of recursion and feature expressions instead of sets of products. Both ideas can be transferred to our setting.

Using a richer modelling language such as e.g. FORML [START_REF] Shaker | A Feature-Oriented Modelling Language and a Feature-Interaction Taxonomy for Product-Line Requirements[END_REF], [START_REF] Shaker | A feature-oriented requirements modelling language[END_REF], one can differentiate between intended and unintended behaviour interactions, c.f. [START_REF] Shaker | Behaviour interactions among product-line features[END_REF]. This is useful from a practical point of view and can be integrated into our approach by extending the syntax to be able to express such intentions.

To conclude, we argue that measurement of behavioural interactions in software product lines is an important part of feature-oriented software development, and that the methods we envision for doing so are both practically feasible and would be a useful addition to the developer's tool box.

Fig. 2 .

 2 Fig. 2. Projections π B (F ), π B∧R (F ) and π B (π B∧R (F ))

Theorem 1

 1 TS S, S are bisimilar iff d(S, S ) = 0.Proof sketch: If S = (S, Σ, I, T ) and S = (S , Σ, I , T ) are bisimilar, then there is a bisimulation relation R ⊆ S × S. It can easily be shown that algorithm 1 will follow this relation when computing the distance, so that every time dist(s, s ) is called, (s, s ) ∈ R. But then all transitions s a -→ t have a match s a -→ t , and vice versa, with (t, t ) ∈ R, so that dist(s, s ) = 0. For the other direction of the proof, one easily sees that R ⊆ S ×S defined by R = {(s, s ) | dist(s, s ) = 0} is a bisimulation.

Fig. 3 .Fig. 4 .

 34 Fig. 3. Projections π B∧M (F ) and π B∧M ∧R (F )

1 :

 1 global Passed : 2 N → Set 2: for all p ⊆ N do Passed(p) ← ∅ 3: return max max

		i∈I	min i ∈I	fdist(i, i ), max i ∈I	min i∈I	fdist(i, i )
	4: function fdist(s, s )
	5:	for all p ⊆ N do
	6:	Add (s, s ) to Passed(p)
	7:	d ← fdista(s, s ) + fdista(s , s)
	8:	return d
	9: function fdista(p, s, s )
	10: 11: 12:	local m ← ∞, d ← 0 for all s a -→ p t do if s a -→ p then d ← d + 1
	13: 14:	else for all s	a -→ p t do
	15:	if (t, t ) / ∈ Passed(p) then
	16:		m ← min(m, fdist(t, t ))
	17:	d ← d + m
	18: