Saddek Bensalem
email: bensalem@imag.fr

Marius Bozga
email: bozga@imag.fr

Jean Quilbeuf
email: quilbeuf@imag.fr

Joseph Sifakis
email: sifakis@imag.fr

Optimized Distributed Implementation of Multiparty Interactions with Restriction $

Keywords: multiparty interaction, priority, observation, conflict resolution, distributed systems Interactions + Priority Interactions + Restriction 1 Interactions + Restriction Knowledge-Based Optimization Interactions 3 Interactions 3 Message Passing Restriction-Aware Implementation Restriction-Aware Implementation Multiparty-Based Implementation Multiparty-Based Implementation

Using high level coordination primitives allows enhanced expressiveness of component-based frameworks to cope with the inherent complexity of present-day systems designs. Nonetheless, their distributed implementation raises multiple issues, regarding both the correctness and the runtime performance of the final implementation. We propose a novel approach for distributed implementation of multiparty interactions subject to scheduling constraints expressed by priorities. We rely on new composition operators and semantics that combine multiparty interactions with Restriction. We show that this model provides a natural encoding for priorities. We provide a knowledge-based optimization that modifies the Restriction operator to avoid superfluous communication in the final implementation. We complete our framework through an enhanced conflict resolution protocol that natively implements Restriction. A prototype implementation allows us to compare performances of different optimizations.

Introduction

Correct design and implementation of computing systems has been an active research topic over the past three decades. This problem is significantly more challenging in the context of distributed systems due to a number of factors such as non-determinism, asynchronous communication, race conditions, fault occurrences, etc. Model-based development of such applications aims to ensure correctness through the usage of explicit model transformations from high-level models to code.

In this paper, we focus on distributed implementation for models defined using the BIP framework [START_REF] Basu | Modeling heterogeneous real-time components in BIP[END_REF]. BIP (Behavior, Interaction, Priority) is based on a semantic model encompassing composition of heterogeneous components. The behavior of components is described as an automaton extended by data and associated functions written in C. BIP uses an expressive set of composition operators for obtaining composite components from a set of components. The operators are parameterized by a set of multiparty interactions between the composed components and by priorities, used to specify different scheduling mechanisms between interactions 1 .

A multiparty interaction is a high-level construct that expresses a strong synchronization between a fixed set of components. Such an interaction takes place only if all its participant components agree to execute it. If two multiparty interactions involve a common component, they are conflicting because the 2. Second, we show that the knowledge-based optimization originally presented in [START_REF] Bensalem | Knowledge-based distributed conflict resolution for multiparty interactions and priorities[END_REF] can be easily applied to a model with Restriction, to reduce implicit synchronization of the model. This optimization (Transformation 2 of Figure 1) modifies only the Restriction operator. [START_REF] Bagrodia | Process synchronization: Design and performance evaluation of distributed algorithms[END_REF]. Third, a model with Restriction can be used as an intermediate step in the transformations leading to a distributed implementation. We show that observation conflicts, that usually follow from encoding of priorities, can be dealt more efficiently than structural conflicts, where two multiparty interactions involve at least a common component. In particular, we compare two approaches for generating a distributed implementation. The first consists in encoding Restriction with multiparty interactions and then using a conflict resolution protocol (Transformations 3 and 4). The second is new and uses a conflict resolution protocol designed to handle Restriction (Transformation 5). 4. These approaches have been fully implemented and evaluated through benchmarks.

The paper is organized as follows. Section 2 introduces the main concepts of the BIP framework together with the new Restriction composition operator. An adaptation of the knowledge-based optimization from [START_REF] Bensalem | Knowledge-based distributed conflict resolution for multiparty interactions and priorities[END_REF] for Restriction is presented in Section 3. Section 4 recalls the principles for distributed implementation of BIP models, focusing on conflict resolution by using counter-based protocols and present a solution for distributed implementation of Restriction. Experiments are reported in Section 5. Section 6 presents the related work for conflict resolution, priorities and knowledge. Section 7 provides conclusions and perspectives for future work.

Semantic Models of BIP

In this section, we present BIP [START_REF] Basu | Modeling heterogeneous real-time components in BIP[END_REF], a component framework for building systems from a set of atomic components by using two types of composition operators: Interaction and Priority. We then present an alternative type of composition, named Restriction, that can express Priority. Finally, we present a transformation from a component with Restriction into an equivalent component with only Interaction. Atomic Components. An atomic component B is a labelled transition system represented by a tuple (Q, q 0 , P, T ) where Q is a set of control locations or states, q 0 is the initial state, P is a set of communication ports and T ⊆ Q × P × Q is a set of transitions.

We write by q p -→ q if (q, p, q ) ∈ T . If the target state is irrelevant, we write q p -→ to express that an outgoing transition labeled by p is possible at state q.

Interactions & Priorities

In order to compose a set of n atomic components {B i = (Q i , q 0 i , P i , T i )} i=1,n , we assume that their respective sets of control locations and ports are pairwise disjoint; i.e., for any two i = j in {1..n}, we require that Q i ∩ Q j = ∅ and P i ∩ P j = ∅. We define the global set P def = n i=1 P i of ports. An interaction a is a set of ports such that a contains at most one port from each atomic component. In the sequel, we denote by participants(a) the components that participate in a, and by I a ⊆ {1, . . . , n} the corresponding indices. We also denote a = {p i } i∈Ia , where p i ∈ P i is the port of B i participating in a.

Priorities. Given a set γ of interactions, we define a Priority as a strict partial order π ⊆ γ × γ. We write a < π b for (a, b) ∈ π to express that a has lower priority than b.

Composite Components. A composite component πγ(B 1 , . . . , B n ) (or simply component) is defined by a set of atomic components {B i = (Q i , q 0 i , P i , T i )} i=1,n composed by a set of interactions γ and a Priority π ⊆ γ × γ. If π is the empty relation, then we omit π and simply write γ(B 1 , . . . , B n ). A global state q of πγ(B 1 , . . . , B n ) is defined by a tuple of control locations q = (q 1 , . . . , q n ). The behavior of πγ(B 1 , . . . , B n ) is a labelled transition system (Q, q 0 , γ, → πγ ), where Q = n i=1 Q i , q 0 = (q 0 1 , . . . , q 0 n ) and → γ , → πγ are the least sets of transitions satisfying the rules:

a = {p i } i∈Ia ∈ γ
∀i ∈ I a . (q i , p i , q i ) ∈ T i ∀i ∈ I a . q i = q i (q 1 , . . . , q n ) a → γ (q 1 , . . . , q n )

[inter] q a -→ γ q ∀a ∈ γ. a < π a =⇒ q a γ q a -→ πγ q

[prio]

Transitions → γ defined by rule [inter] specify the behavior of the component without considering priorities.

A component can execute an interaction a ∈ γ iff for each port p i ∈ a, the corresponding atomic component B i can execute a transition labeled by p i . If this happens, a is said to be enabled. Execution of a modifies atomically the state of all interacting atomic components whereas all others stay unchanged. The behavior of the component is specified by transitions → πγ defined by rule [prio]. This rule restricts execution to interactions which are maximal with respect to the priority order among the enabled ones. An enabled interaction a can execute only if no other interaction a with higher priority is enabled.

Example 1. A BIP component is depicted in Figure 2 using a graphical notation. It consists of two atomic components named M and S. The component S is a server, that may receive requests (through the port req) and acknowledge them (through the port ack ). Formally, S = ({lst, dwn, srv }, dwn, {h S , b S , req, ack }, {(lst, h S , dwn), (dwn, b S , lst), (lst, req, srv ), (srv , ack , lst) }). The component M is a manager that may perform upgrades (upg) and needs to reboot (rb) the server for the upgrade to be done. Interactions are represented using connectors between the interacting ports. There are 4 unary interactions, that are interactions involving a single port, and 2 binary interactions. Formally γ = {{b M , b S }, {h M , h S }, {rb}, {upg}, {req}, {ack }}.

On the figure, we use names to denote interactions, for instance {b M , b S } is called boot. The depicted system goes up and down through the binary interactions boot and halt respectively. The priority π = {(reboot, request), (reboot, acknowledge)} is used to prevent a reboot whenever a request or an acknowledgement are possible.

Interaction and Restriction

The priority operator is defined over a system made of components composed by interactions. We consider a new operator, defined over components composed by interactions, called Restriction operator. A Restriction operator assigns a predicate, defined on the global states, to each interaction. This operator inhibits execution of interactions, for which the predicate evaluates to false at the current state. We later show that a priority operator can be expressed as a Restriction operator.

Given a BIP component γ(B 1 , . . . , B n ), we define Restriction as a function ρ, such that for each interaction a ∈ γ, ρ(a) is a boolean formula involving atomic predicates of the form at(q), where q ∈ n i=1 Q i is one of the local states of the atomic components. The predicate at(q) is true at a given global state (q 1 , . . . , q n ), if q is a local state of the atomic component B i and q = q i . We denote by ρ a : Q → {True, False} the predicate obtained by combining the at(q) predicates according to ρ(a), that is the semantics of ρ(a). In the sequel, we often refer directly to the predicate ρ a , instead of using the formula ρ(a).

A composite component with Restriction ργ(B 1 , . . . , B n ) is defined from a component γ(B 1 , . . . , B n ) and a Restriction operator ρ over this component. The behavior of ργ(B 1 , . . . , B n ) is the labeled transition system (Q, q 0 , γ, -→ ργ ), where Q = n i=1 Q i is the set of global states, q 0 = (q 0 1 , . . . , q 0 n ) is the initial state, and -→ ργ is the least set of transitions satisfying the rule:

q a -→ γ q ρ a (q) q a -→ ργ q [restr]
The rule [restr] states that a transition a can execute if it is already a valid transition in the component γ(B 1 , . . . , B n ) and if the predicate ρ a holds for the current state of the components.

Although it is defined on the global state, a Restriction predicate ρ a might depend only on a subset of the components. We use the syntactical definition given for the formula ρ(a) to determine the set of components on which ρ a depends. More precisely, we denote by support(ρ(a)) the set of components {B i | ∃q ∈ Q i . at(q) appears in ρ(a)}. The components in observed ρ (a) def = support(ρ(a)) \ participants(a) play a particular role in the execution of the interaction a: they do not participate in the interaction but their state is observed to decide whether it can execute. Example 2. Figure 3 depicts a composite component with Restriction. Each interaction is labeled by the corresponding formula, which is omitted if it is true The Restriction operator specified in the example implements the priority operator from the Example 1. Here, reboot is the only interaction whose formula is not true, because it is the only low priority interaction. The formula assigned to reboot is ¬(at(lst)∨at(srv )). It evaluates to false whenever interactions with more priority than reboot are enabled.

The Restriction operator violates the component encapsulation principle as it depends on the inner states of components and not only on their interfaces (ports). It is however useful because it explicitly defines the components to observe for deciding the execution of an interaction a. Indeed, this decision can be taken solely based on the states of components in observed ρ (a) and participants(a).

Implementing Priority with Restriction

In Figure 3, we presented an example of composite component with Restriction. Note that the predicate associated to reboot actually encodes the priority rule of Figure 2, since it guarantees that nor request neither acknowledge are enabled when executing reboot. We show that given a Priority π one can obtain a Restriction ρ π such that the behaviors of the components with Priority and Restriction are identical. This corresponds to the Transformation 1 of Figure 1.

Using at(q) predicates, we define the predicate EN a stating whether the interaction a is enabled. First, we define the predicate EN i pi characterizing enabledness of port p i in a component

B i = (Q i , P i , T i ), that is EN i pi = (qi,pi,-)∈Ti at(q i ).
Then, the predicate EN a can be defined by: EN a = pi∈a EN i pi . Note that this predicate depends only on components in participants(a). For the example in Figure 2, the only low-priority interaction is reboot. For every other interaction a, the predicate ρ π a is T rue. The component with Restriction obtained from the component with Priority is exactly the one depicted in Figure 3. Indeed, the predicate ρ reboot is ¬at(lst) ∧ ¬at(srv) which is equivalent to ¬EN request ∧ ¬EN acknowledge .

Implementing Restriction with Interactions

We start from a component with Restriction ργ(B 1 , . . . , B n ) and translate it into an observably equivalent BIP component γ (B 1 , . . . , B n ) by using the Transformation 3 of Figure 1. In order to implement Restriction, each atomic component has to make explicit its current state, both for interactions where it participates and for interactions where it is observed. Then each interaction is extended so that components that are observed by an interaction a because of the Restriction ρ become participants in the corresponding interactions in γ .

Transforming Atomic Components.

Given an atomic component B = (Q, q 0 , P, T ), we define the corresponding observable atomic component as a labeled transition system B = (Q , q 0 P , T ), where:

• Q = Q and q 0 = q 0 the states are the same as in the original component as well as the initial state.

• P = (P ∪ {obs}) × Q: we add a new port denoted obs, that will be used for observation. All ports contain the information of the current state. We denote by p(q) the port (p, q) ∈ P .

• For each transition (q, p, q ) ∈ T , T contains the transition (q, p(q), q ) where the current state of the component is explicit in the offered port. For q ∈ Q, T contains the loop transition (q, obs(q), q) that is used when the component is observed.

The ports of the transformed atomic component are actually couples made of one port and one state of the original component. These explicit the current state of the component to the interactions, in order to evaluate Restriction predicates.

Transforming Interactions.

Given a set γ of interactions and a Restriction ρ, we define the set of interactions γ . If a ∈ γ is an interaction, it is transformed into a set of interactions that are included in γ . By definition, given a global state q = (q 1 , . . . , q n ), the value of ρ a (q) depends only on components in participants(a) ∪ observed ρ (a). We denote by I a (resp. J a ) the indices of components in participants(a) (resp. observed ρ (a)), and we denote by {i 1 , • • • , i k } the indices in I a and J a . For each interaction a = {p i } i∈Ia and each partial state (q i1 , . . . , q i k ) that satisfies ρ a , γ contains the interaction a(q i1 , . . . , q i k ) = {p i (q i )} i∈Ia ∪ {obs j (q j )} j∈Ja . This construction extends the each original interaction a = {p i } i∈Ia to a set of interactions defined over the transformed ports p i (.) and the additional ports obs j (.) of the observed components. The interaction between ports p i (q i ) and obs j (q j ) is added only if ρ a (q 1 , . . . , q n ) evaluates to true.

Proposition 2. We have -→ γ =-→ ργ by mapping the interactions a(q j1 , . . . , q j k ) of γ to a.

Proof. The state spaces of ργ(B 1 , . . . , B n ) and γ (B 1 , . . . , B n ) are the same. The transition q a -→ ργ q can be fired if and only if the components visible to a, namely participants(a)∪observed ρ (a), denoted {B i1 , . . . , B i k }, are in a state (q i1 , . . . , q i k ) satisfying the predicate ρ a . In that case γ contains an interaction a(q i1 , . . . , q i k ). This interaction only changes the state of participants in a, thus we have q a -→ γ q . Conversely, if we have q a -→ γ q , with q = (q 1 , . . . , q n ), there is an interaction a(q i1 , . . . , q i k ) in γ . By definition of γ we have ρ a (q). If a(q i1 , . . . , q i k ) is enabled at state q, each port p i (q i ) for i ∈ I a is enabled, thus a is enabled. By combining that a is enabled at q and ρ a (q) holds, we have q a -→ ργ q . If the transition

q i pi(qi)
-→ q i is in the component B i , then the transition q i pi -→ q i is in the component B i , therefore q = q . Note that the duplication of interactions can be avoided by using models extended with variables and guards on interactions, such as the one presented in [START_REF] Bonakdarpour | A framework for automated distributed implementation of component-based models[END_REF]. In that case, instead of creating a new port p(q) for any pair in P × Q, each port exports a state variable q. Then ρ a is the guard associated with the interaction a, and depends only on variables exported by the ports involved in a.

Knowledge-based Reduction of Observation

Before executing an interaction a, one must check that the states of atomic components in participants(a) and in observed ρ (a) satisfies ρ a . In a distributed context, consistently checking this condition requires a synchronized observation of the corresponding components. Therefore, our first optimization, corresponding to Transformation 2 of Figure 1, tries to minimize the number of components to synchronize in order to check ρ a . Since executing an interaction a involves synchronizing its participants, the only set that could be reduced is observed ρ (a).

In this section, we use distributed knowledge to replace a given Restriction ρ by a new one ρ . The new Restriction reduces the set of observed components observed ρ (a) for each interaction. The distributed knowledge ρ a is a safe under-approximation of ρ a , depending only on participants(a) and observed ρ (a). Distributed knowledge assumes that every component knows the set of reachable states, or at least one over-approximation of it.

There is a tradeoff between minimizing the number of observed components in ρ and the faithfulness of the under-approximation. When restricting the set of observed components observed ρ (a), one also restricts the set of global states where ρ a detects a valid interaction, that is, evaluates to true. To characterize how much of originally valid transitions are detected, we define detection levels.

We first explain in Subsection 3.1 how the set of reachable states is approximated using invariants. We then present distributed knowledge in Subsection 3.2. In Subsection 3.3, we show how knowledge can be used to compute a correct Restriction, provided that the set of components to observe is given. We also define two detection levels that characterize faithfulness of the obtained component with respect to the original one. In Subsection 3.4, we provide heuristics that try to minimize the number of observed components, while ensuring a given detection level.

Invariants and reachable states

Let B = ργ(B 1 , • • • , B n ) be a component with Restriction. We say that the state q is reachable (from the initial state q 0 ) if there exist a sequence of interactions a 1 , • • • , a k ∈ γ and states q 1 , • • • , q k such that

q 0 a1 -→ ργ q 1 a2 -→ ργ • • • a k -→ ργ q k = q.
We denote by R the set of reachable states of B. An invariant of B is a predicate I : Q → {T rue, F alse} satisfied by all reachable states of B. The characteristic set R of I provides an over-approximation of the reachable states (R ⊆ R). We are interested in two types of inductive invariants that can be generated automatically [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF], respectively:

• boolean invariants, that is, conjunctions of boolean constraints of the form j∈J at(q j ). For the example of Figure 2, at(on up ) ∨ at(on) ∨ at(dwn) is a boolean invariant. Indeed, by executing any transition from a state where the invariant holds, we reach a state where the invariant still holds.

For instance, executing the interaction halt disables the predicates at(on) or at(on up ) but enables the predicate at(dwn). It characterizes a set of control locations such that at each global state, at least one location of the set is active. Such constraints are obtained using methods described in [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF].

• linear invariants, that is, conjunctions of linear constraints of the form j∈J k j at(q j ) = k 0 , where all k j and k 0 are integer constants, and at(q i ) is equal to 1 if q i is active and 0 otherwise. For the example of Figure 2, at(on up ) + at(on) + at(dwn) = 1 is a linear constraint. Again, by executing any transition from a state where the invariant holds, we reach a state where the invariant still holds. A linear constraint corresponds to a set of places such that the weighted sum of tokens in the places remains constant throughout the execution. Linear invariants are obtained using algebraic techniques as described in [START_REF] Krückeberg | Mathematical methods for calculating invariants in petri nets[END_REF].

The two above categories of invariants are particularly useful for several reasons. First, they provide good approximations for the enabling/disabling conditions of interactions. This has been empirically demonstrated by the successful application of such invariants for checking deadlock-freedom of component-based systems in BIP [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF][START_REF] Bensalem | D-finder: A tool for compositional deadlock detection and verification[END_REF]. Second, the methods for computing these invariants are tractable and scale for large systems. Their computation is based on the (interaction) structure of the system and can be done incrementally [START_REF] Bensalem | Incremental component-based construction and verification using invariants[END_REF]. In particular, it does not involve fixpoints computation and avoids state space exploration.

Knowledge and Undistinguishability

Given a model γ(B 1 , . . . , B n ), the knowledge of a set of atomic components L ⊆ {B 1 , • • • , B n } is the information about the current global states through a synchronized observation of the components in L. Intuitively, the synchronized observation of the components gives a partial state of the system. The corresponding global state is (1) reachable and (2) coherent with the partial state observed on L. The information obtained through an observation of L correspond to properties that are true in all global states verifying condition (1) and (2). Any subset L induces an equivalence relation on the global states, defined as follows.

Definition 2 (Undistinguishability Equivalence for L). Given L, we define the undistinguishability equivalence ∼ L on global states q ∈ Q as q ∼ L q iff ∀B j ∈ L q j = q j . Intuitively, two states are undistinguishable for L if their restrictions to the states of atomic components in L are identical. An equivalence class of this relation is a set of global states that are coherent with an observation of the local state of atomic components in L. Given an over-approximation R of the reachable states and an arbitrary state predicate φ, we define the predicate "L knows φ" as follows K R L φ(q) = ∀q ∈ R q ∼ L q =⇒ φ(q ). This predicate is defined on R. Intuitively, a set of components L knows a predicate φ at a global state q if φ holds in any reachable state q that L cannot distinguish from q.

Figure 4 illustrates K L with respect to φ and R. Each global state within R is a point characterized by two coordinates: the projections of this state on the states of L and the states of its complement L = {B 1 , . . . B n } \ L. On the left, the gray region represents the characteristic set of φ. In the middle, the gray region represents the characteristic set of "L knows φ" that is the set of the global states where observation of L suffices to assert "φ is true". On the right, the gray region represents the set of the states where "L knows not φ" that is the set of the global states where observation of L suffices to assert "φ is false".

L φ L R L K R L ¬φ L R L K R L φ L R Figure 4
: Knowledge-based approximation of φ for observation L, within reachable states R.

Building a Restriction with reduced observation

This subsection defines a new Restriction ρ built as a knowledge approximation of ρ. This new Restriction is parameterized by assigning to each interaction a ∈ γ a set of components obs(a) that defines observation. We require that obs(a) ∩ participants(a) = ∅. Definition 3. Given a component B = ργ(B 1 , . . . , B n ), an over-approximation R of its reachable states and the sets of observed components {obs(a)} a∈γ , the Restriction ρ with reduced observation associates to each interaction a ∈ γ the predicate ρ a = K R La ρ a where L a = participants(a) ∪ obs(a).

By definition of knowledge, we have ρ a =⇒ ρ a . Furthermore, ρ a depends only on the state of components in L a . In other words, the actual set of observed components for each interaction a is exactly observed ρ (a) = L a \ participants(a), that is the parameter obs(a). Therefore, in the sequel, we directly denote by observed ρ (a) the parameter obs(a). Example 3. We detail the reduction of the Restriction predicate for the interaction reboot of the example in Figure 3. The predicate ρ reboot = ¬at(srv ) ∧ ¬at(lst) depends on the state of the component S, and thus we have originally observed ρ (reboot) = {S}. In that very simple example, the only possible reduction is to take observed ρ (reboot) = ∅. It means that we rely only on the state of M , that is the unique participant in reboot, to determine whether ρ reboot holds.

In Figure 5, we present all the global states of the system, and indicate whether they are reachable or not. This figure is the instantiation of the Figure 4 when considering the example in Figure 3 and observing only M . On this example, boolean and linear invariants yield the same result. For instance, the state (off , lst) is not reachable as it does not satisfy the boolean constraint at(on up ) ∨ at(on) ∨ at(dwn). We obtain the same conclusion by using the linear constraint at(on up ) + at(on) + at(dwn) = 1.

In the Figure, each local observation (state of M ) corresponds to a column representing the global states that are undistinguishable from that local observation. The interaction reboot is enabled at local state on up and off up . When the local state is on up , the system is either at state (on up , lst) or (on up , srv ). In both cases, ρ reboot does not hold, thus "M knows ¬ρ reboot " at that state. Conversely, at local state off up , the global state is (off up , dwn). Therefore, M knows that ρ reboot holds if its current state is off up . Finally, the new Restriction predicate for reboot is ρ reboot = at(off up ), which depends only on the state of M . By restricting too much the set observed ρ (a), one takes the risk of always obtaining ρ a = f alse, as the observation might not be sufficient to ensure that ρ a holds. We define two criteria characterizing different detection levels, namely basic and complete. Intuitively, the condition for basic detection ensures that the sets of states enabling at least one interaction from γ is the same for ρ and ρ . In contrast, the condition for complete detection ensures that every interaction in γ is enabled in the same states for ρ and ρ . Definition 4 (Detection levels). Let ργ(B 1 , • • • , B n ) be a component and ρ be a Restriction obtained by restricting observation in ρ using the over-approximation R of the reachable states. We say ρ is:

• basic iff ∀q ∈ R. a∈γ (ρ a (q) ∧ EN a (q)) = a∈γ (ρ a (q) ∧ EN a (q)) .
• complete iff for each interaction a ∈ γ: ∀q ∈ R. (EN a (q) ∧ ρ a (q) = EN a (q) ∧ ρ a (q)).

Theorem 1 below, relates the detection levels and corresponding guarantees on the component equipped with the computed Restriction ρ . Baseness ensures that ρ does not introduce deadlocks. Completeness ensures that the global behaviors of the component equipped with ρ and the component equipped with ρ are identical.

Theorem 1. Let ργ(B 1 , • • • , B n ) be
a component and ρ be the Restriction obtained by restricting observation in ρ. Then, -→ ρ γ ⊆-→ ργ and:

1. If ρ is basic, then q ∈ R is a deadlock for -→ ρ γ only if q is a deadlock for -→ ργ . 2. If ρ is complete, then -→ ρ γ =-→ ργ . Proof. Since for each a ∈ γ, ρ a =⇒ ρ a , we have -→ ρ γ ⊆-→ ργ .
1. By contraposition, let q ∈ R be a deadlock-free state for -→ ργ , i.e. such that ∃a ∈ γ (EN a (q)∧ρ a (q)).

Baseness ensures that a∈γ (EN a ∧ ρ a ) holds and thus ∃b ∈ γ such that EN b (q) ∧ ρ b (q). Thus q b -→ ρ γ and q is a deadlock-free state for -→ ρ γ .

2. Assume that q a -→ ργ q . Then EN a ∧ ρ a (q) holds. Completeness ensures that EN a ∧ ρ a (q) also holds. Thus q a -→ ρ γ q . These results characterize to what extent the original Restriction can be captured through partial observation. The approach suggested by this subsection is to come up with some sets of components to observe, then compute the corresponding Restriction and see whether it fits a given detection level. In the next subsection, we propose the reverse approach, that is heuristics that minimize the number of observed atomic components, yet ensuring the required detection level.

Heuristics to minimize observed components

In this subsection, we propose for each detection level from Definition 4 a heuristic that takes as input a component with Restriction and outputs minimized sets of observed components {observed ρ (a)} a∈γ . In general, finding the optimal solution, that is which minimizes the number of observed components while ensuring baseness or completeness is hard. This problem is actually similar to the identification of the minimal number of attributes required to distinguish a set of objects in the rough set theory [START_REF] Pawlak | Rudiments of rough sets[END_REF] which is known to be NP-hard. Each of the proposed heuristics guarantees that the reduced Restriction ρ built using the returned sets of observed components meets the corresponding detection level. The results depend upon the approximation R of the reachable states used for computing the knowledge. We assume throughout this subsection a fixed over-approximation R of the reachable states. In practice, R is provided by linear or boolean invariants.

We propose a solution to the minimizing observation problem based on the simulated annealing meta heuristic [START_REF] Kirkpatrick | Optimization by simulated annealing[END_REF]. A pseudo-code for the simulated annealing is shown in Algorithm 1. This heuristic allows searching for optimal solutions to arbitrary cost optimization problems. The search through the solution space is controlled by a temperature parameter Θ that ranges from Θ max to Θ min during the execution. At every iteration of the simulated annealing, temperature decreases slowly (line 9) and the current solution Θ:= 0.99 × Θ 10: end while 11: return sol moves into a new, nearby solution still ensuring either baseness or completeness (line 4). If the new solution is better (i.e. observes fewer components), then it becomes the current solution. Otherwise, it may be accepted with a probability that decreases when (1) the temperature decreases or (2) the extra cost of the new solution increases (line 6). The idea is to temporarily allow a bad (but correct) solution whose neighbors may be better than the current one. By the end of the process, the temperature is low, which prevents bad solutions from being accepted. The choice of the parameter Θ min and Θ max depends on the possible cost values that depend on the model, and also define the execution time of the simulated annealing. These values should be chosen so that a very bad solution can be accepted when temperature Θ = Θ max and that the probability to accept a solution worse than the current one is almost 0 when Θ = Θ min . However, we provide initial solutions init as well as alter and cost functions that are used to ensure either completeness or baseness.

Ensuring Completeness

According to Definition 4, checking for completeness is performed interaction by interaction. Therefore, minimizing observation can be carried out independently for each interaction. Given an interaction a we are seeking for a minimal set of atomic components L a such that K R La ρ a = ρ a . Note that finding such a set L a yields the corresponding set of components to observe by taking observed ρ (a) = L a \ participants(a).

The initial solution is obtained by taking the set of atomic components that are needed to decide ρ a , that is init a = participants(a) ∪ observed ρ (a). At each iteration of the simulated annealing, a new solution is computed using the alter function shown in Algorithm 2. First, one atomic component is removed from the solution (perturbation, line 3), possibly breaking completeness. Then, new atomic components are added randomly until the solution ensures complete detection again (completion, line 6). Note that loop terminates, as in worst case, observing all components is sufficient to decide whether ρ a holds. Finally, atomic components are removed randomly, provided they do not contribute to completeness (reduction, line 10). This loop stops when removing a component breaks completeness or when there is no more component to remove. The latter case arises when observing the participants is enough to evaluate the Restriction predicate. In that case (line 12), the simulated annealing can be stopped as participant(a) is an optimal solution.

After completion and during reduction steps, the completeness condition is checked (line 9). On termination, this ensures that the solution returned by the heuristic is complete.

The cost of a solution is obtained by counting the number of atomic components in observed ρ (a) = L a \ participants(a). The cost function is thus cost(L a ) = |L a \ participants(a)|.

Ensuring Baseness

Baseness is achieved if for every state where an interaction is allowed by ρ, at least one interaction is also allowed in ρ . Baseness is a global property for the set of all interactions. Indeed, when restricting Algorithm 2 Function alter for ensuring completeness Input: A component ργ(B 1 , . . . , B n ), an interaction a and a solution L a . Output: A solution L a that is a neighbor of L a .

1:

L a :=L a 2: choose B i in L a \ participants(a) 3: L a :=L a \{B i } //perturbation 4: while EN a ∧ K R L a ρ a = EN a ∧ ρ a do 5: choose B i in {B 1 , . . . , B n } \ L a 6: L a :=L a ∪ {B i } //completion 7: end while 8: choose B i in L a \ participants(a) 9: while EN a ∧ K R L a ρ a = EN a ∧ ρ a do 10: L a :=L a \ {B i } //reduction 11:
if L a = participants(a) then EXIT participants(a) //cannot observe less components 13:

end if

14:
choose B i in L a \ participants(a) 15: end while 16: return L a the set of components observed by an interaction, one restricts the set of states where this interaction can be executed. Whether this restriction breaks baseness depend on whether there exists another interaction which can execute at the removed states. Therefore, a solution {L a } a∈γ to the minimizing observation ensuring baseness cannot be built independently for each interaction.

The initial solution assumes that each interaction a observes all atomic components that are needed to decide ρ a , that is init a . Thus the initial solution is init = {init a } a∈γ . As for completeness, the alter function for baseness presented in Algorithm 3 computes a new solution based on the same three steps (perturbation, completion, reduction) being performed on a family of sets of observed atomic components, instead of a single set. As in the previous case, the completion terminates by observing all components in the worst case. Conversely, the reduction terminates either when the baseness property is broken or when no more component can be removed. Again, in the latter case the whole algorithm can be stopped as an optimal solution has been found.

After completion and during reduction steps, the baseness condition is checked (line 9). This guarantees that the returned solution is basic. Here the cost of the solution is the sum of the number of atomic components observed by each interaction. Thus, we define the cost function as cost({L a } a∈γ ) = a∈γ |L a \ participants(a)|.

Decentralized Implementation of BIP

We provide here the principle of the method for distributed implementation of BIP as presented in [START_REF] Bonakdarpour | A framework for automated distributed implementation of component-based models[END_REF][START_REF] Bonakdarpour | From high-level component-based models to distributed implementations[END_REF]. This method relies on a systematic transformation from arbitrary BIP components into distributed BIP components. A distributed BIP component relies only on message passing interactions. A message passing interaction is defined by a send port and a receive port and models the passing of a message between the corresponding components. The transformation guarantees that the receive port is always enabled when the corresponding send port becomes enabled, and therefore Send/Receive interactions can be safely implemented using any asynchronous message passing primitives (e.g., MPI send/receive communication, TCP/IP network communication, etc...).

In a distributed setting, each atomic component executes independently and thus has to communicate with other atomic components in order to ensure correct execution with respect to the original semantics. Thus, a reasonable assumption is that each component will publish its offer, that is the list of its enabled EXIT {participants(a)} a∈γ //cannot observe less components 13:

end if

14:
choose b in γ and B i in L b \ participants(b) 15: end while 16: return {L a } a∈γ ports, and then wait for a notification indicating which interaction has been chosen for execution. This behavior is obtained by splitting each transition: one part sends the offer, the other part is triggered by the notification and executes the chosen interaction.

A set of distributed atomic components that send offers and wait for notifications requires a mechanism that receives offers and send the notifications, accordingly to the offers received and the semantics of the original model. In our implementation, this mechanism consists of one or several additional components. Respecting the semantics of the original model can be described as two tasks:

1. Detect enabled interactions, that is, whose Restriction predicate evaluates to true, 2. Resolve conflicts between interactions that involve a common component.

Our solutions rely on Bagrodia's algorithms from [START_REF] Bagrodia | Process synchronization: Design and performance evaluation of distributed algorithms[END_REF]. These algorithms use counters to implement mutual exclusion of conflicting interaction. We propose an extended version that encompasses the Restriction operator.

In Subsection 4.1, we present the different kinds of conflicts that arise between interactions subject to Restriction. We then describe in Subsection 4.2 how atomic components are modified to send offers and receive notifications. In Subsection 4.3, we formally describe a solution relying on a single manager and prove its correctness in Subsection 4.4. Finally, we informally describe how this manager can be decentralized to obtain a 3-layer distributed implementation.

Conflicts and Observation

A conflict appears when two entities compete for a single resource. In our case, the potentially competing entities are the interactions and the resource is the participation of a component. Intuitively, two interactions are conflicting if they involve a common component, which is a participant for at least one of them.

As an example, consider the composite component depicted in Figure 6. It contains three atomic components and three fragments of interaction. Interactions a and b observe the atomic component B 2 . Execution of a or b will not change the state of B 2 since none of its transitions is involved. Intuitively, a and b can be executed in parallel, they do not really conflict. However, execution of c changes the state of the atomic component B 2 and may disable the predicate associated to a or b. Thus a and c cannot be executed simultaneously. They are conflicting. B 2 q p(q) obs(q) p(q) c . . . . . .

obs(q) B 1 p 1 (q 1 )
. . . a(q 1 , q, . . .)

B 3 p 3 (q 3 )
. . . b(q, q 2 , . . .)

Figure 7: Observable model obtained from the composite component with Restriction in Figure 6.

These types of conflicts also appear in transactional memories [START_REF] Herlihy | Transactional memory: architectural support for lock-free data structures[END_REF]. In this context, different transactions (interactions) can simultaneously read (observe) a variable (an atomic component), but writing on a variable (executing a transition) requires exclusive access to the variable.

The transformation of the model from Figure 6 into an observable model, as described in Subsection 2.4, yields the model depicted in Figure 7. The Restriction is implemented by adding a new port obs(q) to B 2 and extending interactions a and b to that new port. In this model, B 2 becomes a participant, through the port obs(q) in the interactions a and b. This results in a structural conflict between a and b.

In the context of multiparty interactions, a component either participates in or does not interfere with an interaction. In particular, models where interactions can observe components without modifying them, such as the one in Figure 6, cannot be directly implemented. The transformation presented in Subsection 2.4 allows to transform a model with Restriction into a model containing only multiparty interaction. Nevertheless, the obtained distributed implementation involves an unnecessarily high number of exchanged messages: Consider the model presented in Figure 7. Execution of interaction a followed by interaction b requires at least 4 messages between the component B 2 and the protocol. Indeed, each interaction requires at least one offer and one notification (on the port obs(q)). These four messages could be replaced by a single one, indicating that B 2 is at state q to the protocol, since the component B 2 does not need to be notified when it is observed.

Distributed Atomic Components

The transformation of atomic components consists in splitting each transition into two consecutive transitions: (i) an offer that publishes the current state of the component, and (ii) a notification that triggers the transition corresponding to the chosen interaction. The offer transition publishes its enabled ports through a port, labeled o. Definition 5 (Distributed atomic components). Let B = (Q, q 0 , P, T ) be an atomic component. The corresponding transformed atomic component is B ⊥ = (Q ⊥ , q 0 ⊥ , P ⊥ , T ⊥ ), such that:

• Q ⊥ = Q ∪ {⊥ q |q ∈
Q} is the union of stable states Q and busy states {⊥ q |q ∈ Q}.

• q 0 ⊥ =⊥ q 0 the initial state is the busy state associated to the initial state of the original component.

• P ⊥ = P ∪ {o}, where o is a new port which publishes the currently enabled ports and the current state of the component.

• the set of transitions T ⊥ includes, for every transition τ = (q, p, q ) ∈ T :

1. an offer transition (⊥ q , o, q) that goes from a busy to a stable state and publishes the port enabled from this stable state.

a notification transition q

We introduced a new port that publishes offers. The actual offer sent depends on the current state of the component. Given a stable state q ∈ Q, we denote by offer(q) = {p ∈ P | ∃q ∈ Q, q p -→ q } the set of ports enabled at state q. In a more concrete implementation, the port o exports the set offer(q) and the current state q through the offer port [START_REF] Bonakdarpour | A framework for automated distributed implementation of component-based models[END_REF].

Counter-based Conflict Resolution

In Bagrodia's solutions, the protocol is implemented through one or several managers that receive offers from the atomic components and reply with notifications. We extend these solutions to encompass Restriction predicates.

The first solution consists of a single manager. In order to ensure mutual exclusion of conflicting interactions, the protocol maintains two counters for each atomic component B i :

• The offer-count n i which counts the number of offers sent by the component so far. This counter is initially set to 0 and is incremented each time an offer from B i is received.

• The participation-count N i which counts the number of times the component participated in an interaction. This counter is initially set to 0 and is incremented each time the manager selects an interaction involving B i for execution.

Intuitively, the offer-count n i associated to an offer from a component B i correspond to a time stamp. The manager maintains the last used time stamp (N i ) for each component. If the time stamp (n i ) of an offer is greater than the last used time stamp (N i ), then the offer from B i has not been consumed yet. Otherwise, some interaction has taken place and the manager has to wait for a new offer from the component B i .

Furthermore, the manager knows the set of ports enabled and the current state through the offers sent by each component. Thus in order to schedule an interaction, it must check that 1. the interaction is enabled according to the last offers received, 2. the Restriction predicate associated to the interaction evaluates to true according to the last offers, and 3. these offers are still valid according to the n i and N i counters.

If these three conditions hold, the interaction can be executed. Upon execution the participation-counts (N i ) associated to the participants are updated to the values of the offer-counts (n i ), so that participants cannot interact again until a new offer is sent and n i > N i holds again. In particular, any other interaction that involve (as participants or for observation) one of the participants of the previously executed interaction is blocked until new offers from the conflicting components are sent. Hence, mutual exclusion of conflicting interactions is ensured.

The participation-count of the observed components are not updated, even if they are checked to ensure that offers satisfying the Restriction predicate are still valid. Thus a component can be "observed" many times, as long as it does not participate in an interaction. We define formally the behavior of the composition of the centralized protocol with the distributed atomic components. Definition 6. Given a BIP component with Restriction ργ(B 1 , . . . , B n ) we define the behavior of the adapted counter-based centralized implementation as an infinite state LTS (Q ⊥ , q 0 , γ ⊥ , T ⊥ ) where:

• The set of states Q ⊥ is the product of the states of the atomic components with the state of the protocol:

Q ⊥ = n i=1 Q ⊥ i × n i=1 N × N × 2 Pi × Q i
The state of the manager is defined by n quadruples m i = (n i , N i , offer i , q i ), one for each component B i , where n i and N i are the values of the corresponding counters, offer i is the last offer from B i and q i is the last known state from B i . We denote by (q, m) a state of Q ⊥ , q[i] and m[i] represent the ith element of the tuples q and m.

• q 0 = ((⊥ q 0 1 , . . . , ⊥ q 0 n ), ((0, 0, ∅, q 0 1 ), . . . , (0, 0, ∅, q 0 n ))). The initial state of system is obtained by taking the initial states of the distributed atomic components, and assigning 0 to each counter in the manager.

• The interactions of γ ⊥ include the interactions from the original component and the offers:

γ ⊥ = γ ∪ n i=1 {o i }
• There are two types of transitions in T ⊥ :

(1) offer transitions: From state (q, m) ∈ Q ⊥ , there is an offer transition in T ⊥ if for some component

B ⊥ i an offer is enabled: (q[i], o i , q i ) ∈ T ⊥ i .
In that case, T ⊥ contains the transition (q, m) oi -→ (q , m ), where:

-

q [i] = q i , -m [i] = (n i + 1, N i , offer(q i ), q i ), with m[i] = (n i , N i , , ), -for all j = i, q [j] = q[j] and m [j] = m[j].
(2) execute transitions: From state (q, m) ∈ Q ⊥ , there is an execute transition in T ⊥ if there is an interaction a = {p i } i∈Ia , such that (we denote m[i] = (n i , N i , offer i , q i )):

-∀B i ∈ participants(a), p i ∈ offer i : the interaction is enabled according to the last offers, -ρ a ((q 1 , . . . , q n )) evaluates to true according to the values stored in the manager state m, -∀B i ∈ participants(a) ∪ observed ρ (a), n i > N i : the last offers of participants and observed components are still valid.

Then, the transition (q, m) a -→ (q , m ) is in T ⊥ with (q , m ) defined by:

-∀i ∈ participants(a), q [i] is the state such that (q[i], p i , q [i]) ∈ T ⊥ i , -∀i ∈ participants(a), m [i] = (n i , N i + 1, offer i , q i ): counters of participants are incremented.

-∀j / ∈ participants(a), q

[j] = q[j] ∧ m [j] = m[j]
A global state (q, m) of this protocol clearly separates the state of the components q and the state of the manager m. The enabling of offer transitions depends exclusively on the state of the component sending the offer. Similarly, the enabling of execute transitions is decided by the manager alone. Thus we can assume an asynchronous execution where an offer or an execute transition correspond to a message passing. In the case of the offer transition, the message is sent from the atomic component to the manager. For the execute transition, messages are sent from the manager to each participant in the interaction.

With components where all Restriction predicates are always true, the above construction falls back to the original solution from Bagrodia. Therefore, we can compare a multiparty-based implementation, obtained by encoding Restriction predicates into multiparty interactions, with a Restriction-aware implementation that directly encompass Restriction predicates.

Example 4. Consider again the model depicted in Figure 6. We obtain a Multiparty-based implementation by transforming it into the model of Figure 7 and building a distributed implementation from that model. The protocol presented here is able to build a Restriction-aware implementation directly from the model in Figure 6. In Figure 8, we compare the behavior of the two approaches, when executing the interaction sequence a, b, c. On the left, we show the messages exchanged in the Multiparty-based implementation. On the right we show the messages exchanged in the Restriction-aware implementation. For each process (the distributed components B i and the protocol P ) Figure 8 presents the sequence of messages received and sent. The black circles indicate that an interaction is scheduled by the Protocol. Note that the component Multiparty-based implementation followed by a new offer (o()). With the Restriction-aware implementation, the first offer sent by B 2 is observed but not consumed by a and b. So, there is no need to send notifications and wait for corresponding offers. Only the execution of c consumes the offer. For this particular execution sequence, the Restrictionaware implementation spares 4 messages and increases parallelism since b and c can be launched directly after a, without waiting for a new offer.

B 1 B 3 P B 2 o 3 o2 o 1 a p1 b p3 c p

Restriction-aware implementation

Correctness

We show that the component ργ(B 1 , . . . , B n ) and the corresponding counter-based implementation are observationally equivalent in the sense of Milner [START_REF] Milner | Communication and concurrency[END_REF]. We first prove the following lemma on the reachable states of the distributed implementation.

Lemma 1. Let B ⊥

i be a distributed atomic component. The component

B ⊥ i is in a stable state q i iff n i > N i . Furthermore, if B ⊥
i is in a stable state we have m i = (n i , N i , offer(q i ), q i ).

Proof. The construction of B ⊥ i implies that it alternates offer and execute transitions. In the initial configuration, n i = N i = 0 and B ⊥ i is in a busy state. Therefore the equivalence holds. The only possible transition from this configuration is an offer, which brings the system to a state where n i = N i + 1 > N i and the B ⊥ i is in a stable state. In this configuration, the equivalence holds as well. Furthermore, the offer transition ensures that the offer and state in m i correspond to those of B ⊥ i . In the configuration where B ⊥ i is in a stable state and n i = N i + 1 > N i , the only next possible step in B ⊥ i is an execute action. By executing this step we reach again a configuration where n i = N i and B ⊥ i is a busy state.

In order to show observational equivalence, we have to define the observable actions of both systems. For the component γ(B 1 , . . . , B n ) the observable actions are the interactions γ. These interactions correspond to the execute interactions of the distributed implementation, that are also γ. We denote by β the offer interactions.

We define a relation between states Q of the centralized component and states Q ⊥ of its distributed implementation. To each state (q ⊥ , m) ∈ Q ⊥ of the distributed implementation, we associate a state e((q ⊥ , m)) ∈ Q of the original component. For each component B ⊥ i , q ⊥ [i] is either a stable state q i or a busy state ⊥ qi . In both cases, we take e((q ⊥ , m))[i] = q i . We say that a state q ∈ Q and (q ⊥ , m) ∈ Q ⊥ are equivalent, denoted by (q ⊥ , m) ∼ q, if q = e((q ⊥ , m)).

Proposition 3 (Correctness of Centralized Counter-based Implementation). Given a component ργ(B 1 , . . . , B n ), the labeled transitions systems (Q, q 0 , γ, → ργ ) and (Q ⊥ , q 0 ⊥ , γ ⊥ , → ⊥ ) of its distributed implementation are observationally equivalent.

Proof. We have to prove that:

1. If (q ⊥ , m) β -→ ⊥ (r ⊥ , m ), then ∀q ∈ Q.(q ∼ (q ⊥ , m) =⇒ q ∼ r ⊥ ). 2. If (q ⊥ , m) a -→ ⊥ (r ⊥ , m), then ∀q ∈ Q.(q ∼ (q ⊥ , m) =⇒ ∃r ∈ Q.(q a -→ ργ r ∧ r ∼ (r ⊥ , m ))). 3. If q a -→ ργ r, then ∀(q ⊥ , m) ∈ Q ⊥ .((q ⊥ , m) ∼ q =⇒ ∃(r ⊥ , m) ∈ Q ⊥ .((q ⊥ , m) β * a -→ ⊥ (r ⊥ , m) ∧ r ∼ (r ⊥ , m))).
1. This is a consequence of the definition of ∼. 2. The transition ((q ⊥ , m), a, (r ⊥ , m)) is possible at state (q ⊥ , m) ∈ Q ⊥ if for each participant and observed component B i in the interaction, the counters verify n i > N i , for each port p i ∈ a, we have p i ∈ offer i , and ρ a evaluates to true according to the state m of the manager. The Lemma 1 ensures that in the equivalent state q ∈ Q, we have for each component B i participant in a p i ∈ offer(q i ). Furthermore, the Lemma ensures that for all participant and observed component, the state stored in m is the actual state in q ⊥ , which is equal to q by definition of ∼. Therefore ρ a (q) evaluates to true and q a -→ ργ r. The construction of distributed atomic components ensures that r ∼ (r ⊥ , m).

If q

a -→ ργ r, then for each state (q ⊥ , m) ∼ q, each participant B i in a is either in a busy or in a stable state. In the first case, it can perform an offer transition, labeled β, and reach a stable state. Let (s ⊥ , m ) be a state such that (q ⊥ , m)

β * -→ ⊥ (s ⊥ , m ) β ⊥ .
Such state is attained when all components have performed their offer transitions. Since offers transitions do not modify any common part of the state, executing same in any order yields the same final state and therefore there is a unique state (s ⊥ , m ) as above. By Lemma 1, since at (s ⊥ , m ) all distributed components are in a stable state, we have for 1 ≤ i ≤ n:

• n i > N i
• m i = (n i , N i , offer(q i ), q i ) where q i = q i by definition of ∼.

According to m , ρ a ((q 1 , . . . , q n )) = ρ a (q) evaluates to true and for each port p i ∈ a, we have p i ∈ offer(q i ). Thus (s ⊥ , m ) a -→ ⊥ (r ⊥ , m ). By construction (r ⊥ , m ) ∼ r.

3-layer Distributed Architecture

With a single manager we obtain a 2-layer implementation, namely the components layer and the manager. In [START_REF] Bonakdarpour | A framework for automated distributed implementation of component-based models[END_REF], we further decompose the manager in two layers, respectively an interaction layer, and a conflict resolution layer.

The interaction layer receives the offers from the components, compute the enabled interaction and evaluates the Restriction predicates. Whenever an interaction can be executed, the interaction layer sends a reservation request rsv to the conflict resolution layer for executing the interaction. The request contains the offer-count (n i ) of each component participant in or observed by the interaction. The interaction layer then waits for an answer from the conflict resolution layer. If the answer is positive (ok), the interaction is executed and the interaction layer sends a notification to each participant in the interaction. Otherwise the answer is f (fail), and the interaction protocol waits for a new offer before trying a new reservation.

The conflict resolution layer receives the requests along with the offer-count. It is also responsible for maintaining the participation-count N i . Upon reception of a request, it compares the received n i with the maintained N i . If for all involved components n i > N i , then all for all participants the value of N i is updated to n i and a positive answer ok is sent back. Otherwise a negative answer f (fail) is sent back.

As shown in Figure 9, the interaction layer can be separated in several processes (here IP 1 , IP 2 , IP 3 ), in order to allow concurrent execution of interactions. The transformation from a BIP model into a 3-layer implementation is actually parameterized by a partition of the interaction. Each class of the partition yields a distinct process in the final implementation. For our example, the partition is {{upgrade, reboot}, {boot, halt}, {request, acknowledge}}. Thus in our case, the process IP 1 is responsible for detecting whenever the interaction reboot or the interaction upgrade is enabled.

M ⊥ o M rb h M upg b M Components layer S ⊥ o S h S b S req ack IP1 o M n rb nupg rsv ok f IP2 o M o S n bt n hlt rsv ok f IP3

Interaction layer

o S nreq n ack rsv ok f If there are several processes handling interactions, each component maintain its n i counter and send it with the offer. The components send offer only to processes handling interactions in which they are observed or participate. If some interaction conflicts only with interactions that are handled in the same process, the conflict can be resolved locally. Thus, taking a coarser partition reduces the parallelism between execution of interactions but also reduce the load on the conflict resolution layer as more conflicts can be solved internally.

CRP Conflict resolution layer

Finally, the conflict resolution layer can be decentralized as well. Intuitively, the key property to ensure tis correctness is the atomicity of the operation consisting in checking that the offer-counts are greater than the participation-counts and updating the latter ones if true. Following Bagrodia [START_REF] Bagrodia | Process synchronization: Design and performance evaluation of distributed algorithms[END_REF], we propose three implementations:

• A centralized implementation, where a single process receives all the requests. In that case, atomicity is ensured as only this process can access the N i variables.

• A token ring implementation, where each interaction yields a separate process in the conflict resolution layer. Each process receives only the requests for executing the interaction it handles. A token carrying all the N i variables circles through all processes in the layer. Only the process holding the token can access these variables, which ensures the needed atomicity.

• An implementation based on a solution to the dining philosophers problem [START_REF] Chandy | Parallel program design: a foundation[END_REF]. This is the most decentralized solution. Each interaction yields a process in the conflict resolution layer. Interactions are mapped to philosophers, and forks represent conflicting components. Hence, two processes corresponding to two conflicting interactions share a fork, that is a token with the N i variables of the components causing the conflict. In order to execute an interaction, each process must acquire all forks shared with its neighbors. Then it is the only one to access the needed N i variables which ensures atomicity. Using a solution to the dining philosopher problem ensures that any process will eventually be able to acquire all the forks shared with its neighbors (no starvation).

Experiments

We compare the execution time and the number of exchanged messages for several distributed implementations of a component with priority. As shown in Figure 1, several sequences of transformations and optimizations can be applied to generate a distributed implementation. The first step (Transformation 1 in Figure 1) involves transformation of this component into a component with Restriction. The obtained component may be optimized using knowledge as explained in Section 3 (Transformation 2 in Figure 1). Whether the component is optimized or not, we consider the two following sequences of transformations leading to a distributed implementation. conflict resolution protocol described in Subsection 4.3, which in this case falls back to the original version by Bagrodia. This method (Transformations 3 and 4 in Figure 1) results in a multiparty-based implementation.

•

F i+1 eat i eat i-1 E i eat i+1 cleanleft i cleanright i cleanright i-1 cleanleft i+1 C i C i+1
• Directly transform the component with Restriction into a 3-layer distributed model embedding the conflict resolution protocol described in Subsection 4.3. This method (Transformation 5 in Figure 1) results in a Restriction-aware implementation.

For both cases, we used the centralized version of the conflict resolution protocol.

Dining Philosophers

We consider a variation of the dining philosophers problem, denoted by PhiloN where N is the number of philosophers. A fragment of this composite component is presented in Figure 10. In this component, an "eat" interaction eat i involves a philosopher and the two adjacent forks. After eating, philosopher P i cleans the forks one by one (cleanleft i then cleanright i ). We consider that each eat i interaction has higher priority than any cleanleft j or cleanright j interaction.

This example has a particularly strong priority rule. Indeed, executing one "clean" interaction potentially requires to check that all "eat" interactions are disabled. This check requires observing all components. This example compares the above implementations under strong priority constraints.

As explained in Section 4.5, the construction of our distributed implementation is structured in 3 layers. The second layer is parameterized by a partition of the interactions. For this example, the partition is built as follows. There is one interaction protocol E i for every eat i interaction and one interaction protocol C i for every pair cleanright i-1 , cleanleft i . Only the latter deals with low priority interactions that need to observe additional atomic components.

Minimizing Observed Components

We first define the quantity that we minimize. In the distributed implementation, each atomic component sends its state to interactions that are observing it. If interactions a and b, both observing a component B i , are handled by the same interaction protocol, the component B i sends only one message to that interaction protocol. In that case, we say that the atomic component is observed by the interaction protocol. We count as an observation each couple (component, interaction protocol) such that the interaction protocol observes the component, and the component is not involved in any interaction handled by the interaction protocol.

Minimizing the number of observations in a complete Restriction ρ is done independently for each interaction protocol. Table 1 shows the results, that is the number of observations involving the interaction protocol C 0 in the solution obtained with the heuristic described in Subsection 3.4.1. Note that same number of observations are needed for each other interaction protocol C i . The total number of atomic components in the composite component is indicated in column Size. The columns true, BI and LI provide the cost of the solutions obtained when using respectively true, the boolean invariant and the linear invariant as overapproximation of the global states. Using true as invariant does not allow actual optimization, therefore it shows the number of observations in the initial Restriction ρ. The column optimal indicates the cost of an optimal solution, that we know for this particular example. Here, the linear invariant gives better results than the boolean invariant, which is not precise enough to allow reducing observation comparatively to the true invariant. For N = 3, we provide the boolean and linear invariants respectively in Figures 11 and12. As an example, consider the linear constraint [START_REF] Bensalem | Knowledge based scheduling of distributed systems[END_REF]. It ensures that interaction cleanleft 0 and interaction eat 1 cannot be enabled concurrently, otherwise, control locations P 0 .eating and F 1 .f ree would be active and the sum in constraint [START_REF] Bensalem | Knowledge based scheduling of distributed systems[END_REF] would be equal to 2. Thus, the priority cleanleft 0 < π eat 1 never forbids execution of cleanleft 0 . A related boolean constraint, that is constraint (3) of boolean invariant guarantees that at least one of these locations is active. However, this constraint is not strong enough to discard the case where two of them are active.

Component

In general, the approximations of reachable states provided by boolean and linear invariants are not comparable. Consider the global state P 0 .cleaning ∧ F 0 .used ∧ P 1 .cleaning ∧ F 1 .used ∧ P 2 .cleaning ∧ F 2 .used . This state satisfies all the constraints of the linear invariant, but does not satisfy the constraint 8 of the boolean invariant.

∀i ∈ {0, 1, 2} (at(Fi.free) ∨ at(Fi.used))

∧ ∀i ∈ {0, 1, 2} (at(Pi.thinking) ∨ at(Pi.eating) ∨ at(Pi.cleaning))

∧ (at(P1.eating) ∨ at(P0.eating) ∨ at(P0.cleaning) ∨ at(F1.free))

∧ (at(P2.eating) ∨ at(P1.eating) ∨ at(P1.cleaning) ∨ at(F2.free))

∧ (at(P0.thinking) ∨ at(F0.used) ∨ at(P0.cleaning) ∨ at(P2.thinking))

∧ (at(P0.thinking) ∨ at(F1.used) ∨ at(P1.cleaning) ∨ at(P1.thinking))

∧ (at(P2.cleaning) ∨ at(F0.free) ∨ at(P2.eating) ∨ at(P0.eating))

∧ (at(F1.free) ∨ at(F2.free) ∨ at(F0.free) ∨ at(P1.eating) ∨ at(P2.eating) ∨ at(P0.eating))

∧ (at(F2.used) ∨ at(P2.cleaning) ∨ at(P1.thinking) ∨ at(P2.thinking))

∧ (at(F2.used) ∨ at(P2.cleaning) ∨ at(P1.thinking) ∨ at(F0.free) ∨ at(P0.eating))

∧ (at(F1.free) ∨ at(P1.eating) ∨ at(F0.used) ∨ at(P0.cleaning) ∨ at(P2.thinking))

∧ (at(P0.thinking) ∨ at(F2.free) ∨ at(F1.used) ∨ at(P2.eating) ∨ at(P1.cleaning)) The results for computing basic solutions are presented in Table 2. The column Size contains the total number of atomic components in the composite component. The columns true, BI and LI contains respectively the cost of the solutions obtained when using respectively true, the boolean invariant and the linear invariant. For Philo3, baseness is achieved when each engine observes only the components involved in the interactions it handles (i.e. no additional observation is needed), therefore the cost is 0.

Comparing Obtained Implementations

The goal of this subsection is to compare the different implementations that we obtained for the dining philosophers example. First, we consider different levels of optimization for the Restriction operator:

• No optimization: the Restriction operator is the direct rewriting of priorities rules, we do not apply any knowledge-based optimization (Transformation 2 in Figure 1).

• Basic: observation required by the Restriction operator is minimized while still ensuring baseness.

• Complete: observation required by the Restriction operator is minimized while still ensuring completeness.

As showed in the previous subsection, the Boolean invariant is not strong enough to reduce the number of observed components comparatively to the non-optimized version. Therefore, the basic and complete version of the Restriction operator have been computed using the linear invariant. For each optimization level considered, we generate a multiparty-based (MB) and a Restriction-aware (RA) implementation. Once we have built the distributed components, we use a code generator that generates a standalone C++ program for each atomic component. These programs communicate by using Unix sockets. The obtained code has been run on a UltraSparc T1 that allows parallel execution of 24 threads. For each run, we count the number of interactions executed and messages exchanged in 60 seconds, not including the initialization phase. For each instance we consider the average values obtained over 20 runs. The number of interactions executed by each implementation is presented in Figure 13. The total number of messages exchanged for the execution of each implementation is presented in Figure 14. First, remark that switching from a multiparty-based (gray) to a Restriction-aware (black) implementation improves performance, that is the number of interactions executed in 60 seconds. Furthermore, it always reduces the number of messages exchanged. The improvement is very visible with the unoptimized version (No opt). This can be explained as follows. Evaluating Restriction predicates requires to observe all components for executing a cleanleft i or a cleanright i interaction. In the multiparty-based implementation, observed components must synchronize to execute some interaction cleanleft i or cleanright i . Between two "clean" executions, each component has to receive a notification and to send a new offer. This strongly restricts the parallelism. In the observation-aware implementation, a component offer is still valid after execution of an interaction observing that component. After a "clean" interaction, only components that participated may need to send a new offer before another "clean" interaction can be executed. This explains the speedup.

Second, when comparing multiparty-based (gray) implementations, one sees that the Restriction operator ensuring completeness gives the best performance. The basic implementations exhibit poor performance because restricting observation in that case also restricts parallelism. For the example with 9 philosophers, multiparty-based implementation with optimized Restriction (Complete -MB) shows a significant gain in performance compared to the non optimized version (No opt -MB). The performance gained by optimizing the Restriction operator into a complete one is not visible anymore when switching to Restriction-aware (black) implementation. However, the optimization remains interesting in that case since it reduces by up to 10% the number of messages needed.

Jukebox

The second example is a jukebox depicted in Figure 15. It represents a system, where a set of readers R 1 . . . R 4 access data located on 3 disks D 1 , D 2 , D 3 . Readers may need to access any disk. Access to disks is managed by jukeboxes J 1 , J 2 that can load any disk to make it available to the connected readers. The interaction load i,k (respectively unload i,k ) allows loading (respectively unloading) the disk D i in the jukebox J k . Each reader R j is connected to a jukebox through the read j interaction. Once a jukebox has loaded a disk, it can either take part in a "read" or "unload" interaction. Each jukebox repeatedly loads all N disks in a random order.

If unload interactions are always chosen immediately after a disk is loaded, then readers may never be able to read data. Therefore, we add the priority unload i,k < π read j , for all i, j, k. This ensures that "read" interactions will take place before corresponding disks are unloaded. Furthermore, we assume that readers connected to J 1 need more often disk 1 and that readers connected to J 2 need more often disk 2. Therefore, loading these disks in the corresponding jukeboxes is assigned higher priority: load i,1 < π load 1,1 for i ∈ {2, 3} and load i,2 < π load 2,2 for i ∈ {1, 3}. Each interaction is handled by a dedicated interaction protocol.

The main difference with the dining philosopher examples is that here priority rules do not restrict parallelism since they are expressed between structurally conflicting interactions. Here a priority rule is used to express a scheduling policy that aims to improve the efficiency of the system, in terms of "read " interactions. Removing this priority rule results in a system that does less "read " interactions.

Minimizing Observed Components

Results of the simulated annealing heuristic are presented in Table 3. Interaction protocols handling a "read" interaction do not need to observe additional atomic components since there is no interaction with higher priority. The boolean invariant allows removing some observed atomic components, in the basic solution. As for PhiloN components, the linear invariant is stronger than the boolean invariant. Therefore, attaining the same level of detection requires less observed atomic components. For this example, the Boolean invariant (BI) provides enough information to reduce the observation. We consider the optimization levels: No optimization, Basic (I), and Complete (I), where I is either the boolean invariant BI or the linear invariant LI. For each optimization level, we compare multipartybased and Restriction-aware implementations. The number of interactions executed during 60 seconds is presented in Figure 16. Here the performance of the Restriction-aware implementation is not significantly better than the performance of the multiparty-based implementation. The best results are obtained with the basic optimization level using linear invariant. These results come from the fact that no parallelism is allowed between low priority interactions since they are structurally conflicting. Therefore patterns enabling parallelism as in Figure 8 do not arise. More precisely, the only gain in performance consists in time involving actually sending and receiving messages, not in waiting unneeded offers.

Comparing Obtained Implementations

Figure 17 shows that significantly fewer messages are exchanged with the Restriction-aware implementation. Intuitively, this difference corresponds to the notifications and subsequent offers to and from observed components, that are not necessary with the Restriction-aware implementation. Interestingly, the implementation giving the best performance (Basic (LI) optimization with Restriction-aware implementation) is also the one requiring the least number of messages.

Related Work

In [START_REF] German | Programming in a general model of synchronization[END_REF], German presents a framework providing multiparty interactions with priorities as primitives. The processes are described using a notation similar to the CCS. Interactions are specified as composite action labels made of conjunctions and negations of actions. For instance, the interaction reboot of the example from Figure 2 could be encoded as the action label rb ∧ ¬req ∧ ¬ack , assuming that BIP ports are mapped to simple actions. Encoding an interaction requires an additional process, that contains a single rule with the corresponding action label. The idea is to provide a language suitable for specifying distributed systems, with a high-level description that can be executed for rapid prototyping. This framework was used to model and verify a telephone switching application. To our knowledge, there is no distributed implementation for this framework, although it was apparently one of the goals in [START_REF] German | Programming in a general model of synchronization[END_REF].

Reo [START_REF] Arbab | Reo: a channel-based coordination model for component composition[END_REF] is a framework where components communicates using a basic set of dataflow connectors that are combined to form a complex connector. At each round, each component enables a set of input and output ports. In Reo, components are black boxes, only their interface is known at each state. A Reo connector defines a set of allowed dataflow interactions for each configuration of the enabled ports. A round consists of executing such an interaction, which transfers data. Furthermore, Reo basic connectors include FIFO 1 connectors that can store one data item, allowing the composed connector to save some data between two rounds. The FIFO connectors introduce a control state in the composed connector, which differs from BIP where interactions have no memory. The Dreams framework [START_REF] Proença | Synchronous Coordination of Distributed Components[END_REF][START_REF] Proença | Dreams: a framework for distributed synchronous coordination[END_REF] provides a distributed implementation for Reo. Each basic connector is implemented as an actor. A round synchronizes the actors through a consensus algorithm, in order to choose the next interaction. In order to achieve a more decentralized behavior, a GALS architecture is obtained by cutting the complex connector into synchronous regions. Two regions can be separated only if their only connections consist of FIFO connectors.

I/O automata [START_REF] Lynch | An introduction to input/output automata[END_REF] were introduced to formally model distributed systems. In this framework, each process is represented by an automaton whose transitions are labeled by actions, similarly to processes from this chapter. Each interaction is represented through a common label that is used in several processes to denote synchronization. I/O automata clearly distinguish between input (uncontrollable) actions and output (controllable) actions. Given an interaction label, there is exactly one process for which this label is an output action, in other processes it can appear only as an input action. Furthermore, from every state of an automaton, all its input actions are required to be enabled. With these restrictions, an interaction is completely controlled by the process for which it is an output action. In that sense, I/O automata interactions are similar to Send/Receive interaction where the sender controls the execution and the receiver should not block the sender. In particular, the fact that an interaction is enabled or not is local to the process that controls the corresponding output action. In that sense, there is no conflict between interactions. However, if two interactions a and b are scheduled simultaneously by two separate processes, the order should be consistent among all common participants in a and b. The solution proposed in the first sketch of a distributed implementation [START_REF] Garland | Foundations of component-based systems. chapter Using I/O automata for developing distributed systems[END_REF] is to require that each automaton reaches the same state for both orderings. In a later solution [START_REF] Georgiou | Automated implementation of complex distributed algorithms specified in the ioa language[END_REF][START_REF] Tauber | Verifiable Compilation of I/O Automata without Global Synchronization[END_REF], this problem is solved by adding a handshake protocol.

In [START_REF] Frølund | A language framework for multi-object coordination[END_REF][START_REF] Dinges | Scoped synchronization constraints for large scale actor systems[END_REF], Synchronizers are used to filter incoming messages for a set of actors. A message is delivered only if it matches an enabled pattern. Such patterns include atomic synchronization of a set of messages, that requires all involved messages to be pending before granting their transmission. According to [START_REF] Dinges | Scoped synchronization constraints for large scale actor systems[END_REF], synchronizers are implemented through dispatchers located on the target actors, that is the actors for which incoming messages are filtered. Upon reception of an incoming message, the dispatcher is responsible for checking whether the message is allowed for transmission according to the synchronizers. In case of atomic synchronization, this requires a protocol similar to the one for multiparty interactions. The actors communicate through asynchronous message-passing, which makes it difficult to exploit the synchronization of messages for verification purposes. This framework is mainly concerned with providing practical constructs for programming with actors.

Behavioral programming [START_REF] Marron | A decentralized approach for programming interactive applications with javascript and blockly[END_REF] is another model for programming interactions between processes. In that model, at each global state, each process provides three sets of actions: requested actions, watched actions and blocked actions. A (centralized) scheduler selects an action that is requested by at least a process and not blocked by any process. The selected action is executed by all processes that requested it and all processes that watched it. The system reaches the next global state by executing the selected action. This model differs from multiparty interactions as the set of participants in the common action is not fixed, but depends on the state. Decentralizing the scheduler while preserving centralized semantics requires to solve problems similar to Interaction and Restriction conflicts resolution. In particular, scheduling an action based on a partial set of offers requires to ensure that this action will not be blocked by a subsequent offer.

Knowledge. The formalization of different kinds of knowledge and related logic, called epistemic logic, have been intensively studied [START_REF] Fagin | Reasoning about Knowledge[END_REF][START_REF] Halpern | Modelling knowledge and action in distributed systems[END_REF][START_REF] Halpern | Knowledge and common knowledge in a distributed environment[END_REF]. In rough sets theory [START_REF] Pawlak | Rudiments of rough sets[END_REF], objects are defined through a set of attributes. Intuitively, an attribute can be the shape, the color, the weight . . . of the object. Each object is fully identified by the definition of its attributes. Given a subset of the objects, deciding whether a given object is part of that subset is always achieved by observing all attributes. Restricting the set of attributes that are observed creates a rough set, that approximates the subset. In that case indeed, there could be some objects whose membership in the subset depends on an unobservable attribute. One of the question in this theory is to find a minimal set of attributes whose observation is sufficient to distinguish any two objects [START_REF] Zhou | Research on complete algorithms for minimal attribute reduction[END_REF].

In [START_REF] Ricker | Know means no: Incorporating knowledge into discrete-event control systems[END_REF], Knowledge is applied to decentralized control of a plant. A plant is an automaton whose interactions are labeled by actions, some of them being forbidden. Multiple decentralized controllers are in charge of controlling the plant, through allowing or not a given subset of the actions. Each controller is defined by the set of actions it can observe and the set of actions it can control (i.e. execute). Knowledge is applied to allow each controller to infer which actions are legal from the current state and thus can be executed. An extension to distributed knowledge is proposed, whenever the information available to only one controller is not enough to decide. A criterion, called "Kripke observability" decides whether the extension to distributed knowledge is enough to control the plant.

In [START_REF] Bensalem | Methods for knowledge based controlling of distributed systems[END_REF][START_REF] Basu | Priority scheduling of distributed systems based on model checking[END_REF], the focus is on distributed controllers for executing Petri nets constrained by a given property. An example of such a constraining property is a priority order. Processes are defined as sets of Petri nets transitions. A transition can be common to several processes, in which case it describes a synchronization. Each process can observe its neighborhood, that is the places that are adjacent to its transitions. In [START_REF] Basu | Priority scheduling of distributed systems based on model checking[END_REF], Knowledge is used to build a support table for each process. This table indicates, for each local configuration, which interaction can be safely executed. Knowledge based on the state of the neighborhood is not always sufficient, two possible extensions are proposed. The first one consists in using knowledge with perfect recall. The second one, also proposed in [START_REF] Graf | Achieving distributed control through model checking[END_REF] consists in accumulating knowledge through additional synchronizations between processes. This additional synchronization is handled by a multiparty interaction protocol; α-core [START_REF] Pérez | An order-based algorithm for implementing multiparty synchronization[END_REF] is proposed. In [START_REF] Bensalem | Methods for knowledge based controlling of distributed systems[END_REF], an optimization is proposed by considering only executions satisfying the constraining property in order to build the knowledge. This approach allows reducing the state space and possibly increase the knowledge of each process.

Conclusion

We proposed different methods for generating a distributed implementation from a model described using multiparty interactions with Restriction. The proposed model ensures enhanced expressiveness as the enabling conditions of an interaction can be strengthened by state predicates of components non participating in that interaction. It directly encompasses modeling of priorities which are essential for modeling scheduling policies. We have proposed a transformation leading from a model with Restriction into an equivalent model with interactions. The transformation consists in creating events making visible state-dependent conditions.

Components whose state is needed to evaluate the Restriction predicate associated to an interaction are observed by this interaction. A synchronized up-to-date view of the observed components that satisfy the predicate is needed to launch the execution of the interaction. We proposed methods, based on the work in [START_REF] Bensalem | Knowledge-based distributed conflict resolution for multiparty interactions and priorities[END_REF] to compute a new Restriction with a reduced number of observed components. The obtained Restriction ensures either deadlock-freedom preservation or observational equivalence with the original model.

Expressing Restriction by interactions allows the application of existing distributed implementation techniques, such as the one presented in [START_REF] Bonakdarpour | A framework for automated distributed implementation of component-based models[END_REF]. We have proposed an optimization of the conflict resolution algorithm from [START_REF] Bagrodia | Process synchronization: Design and performance evaluation of distributed algorithms[END_REF] that takes into account the fact that an observed component does not participate in the observing interaction. Preliminary experiments compare the performance and communication volume of the implementation obtained with various optimization levels. They show significant performance improvement when using the optimized conflict resolution algorithm.

Figure 1 :

 1 Figure 1: Possible paths to generate a distributed implementation from a model encompassing multiparty interactions and priorities.

Figure 2 :

 2 Figure 2: A BIP component. Initial state is (off, dwn).

Figure 3 :

 3 Figure 3: A component with Restriction.

Definition 1 (

 1 Priority Restriction). Let πγ(B 1 , . . . , B n ) be a prioritized BIP component. The priority Restriction ρ π associates to each interaction a ∈ γ the predicate ρ π a = a <π b ¬EN b .

Proposition 1 .

 1 Given a component with Priority πγ(B 1 , . . . , B n ) and the component with Restriction ρ π γ(B 1 , . . . , B n ), where ρ π is constructed from π as specified in Definition 1, we have -→ πγ = -→ ρ π γ . Proof. For each interaction a, the predicate ρ π a = a <π b ¬EN b is equivalent to ∀b ∈ γ.(a < π b =⇒ q b γ ). Thus the rules [prio] and [restr] define exactly the same set of transitions.

Figure 5 :

 5 Figure 5: Global states of the example from Figure 3, assuming that the component M is observed.

Algorithm 1

 1 Pseudo-code of Simulated AnnealingInput: An initial solution init, a cost function, an alter function, temperature bounds Θ max and Θ min . Output: A solution with a minimized cost.1: sol:=init 2: Θ:=Θ max 3: while Θ > Θ min do 4:sol := alter(sol)5:∆ := cost(sol )cost(sol)6:if ∆ < 0 or random() < e

Algorithm 3 1 : 5 : 6 :

 3156 Function alter for ensuring basic detectionInput: A component ργ(B 1 , . . . , B n ), a solution {L a } a∈γ , Output: A solution {L a } a∈γ that is a neighbor of {L a } a∈γ . {L a } a∈γ :={L a } a∈γ 2: choose b in γ and B i in L b \ participants(b) 3: L b :=L b \{B i } //perturbation 4: while a∈γ (EN a ∧ K B L a ρ a ) = a∈γ (EN a ∧ ρ a ) do choose b in γ and B i in {B 1 , . . . , B n } \ L b L b :=L b ∪ {B i } //completion 7: end while 8: choose b in γ and B i in L b \ participants(b) 9: while a∈γ (EN a ∧ K B L a ρ a ) = a∈γ (EN a ∧ ρ a ) do 10: L b :=L b \ {B i } //reduction 11:if ∀a ∈ γ, L a = participants(a) then 12:

Figure 6 :

 6 Figure 6: A composite component with Restriction.

  B 2 is observed by a and b and is a participant in c. With the Multiparty-based implementation, the observation is treated as a participation. Both execution of a and b trigger the emission of a notification (obs) to B 2

Figure 8 :

 8 Figure 8: Exchanges of messages to execute the sequence a, b, c in the model of Figure 6, for the two implementations.

Figure 9 : 3 -

 93 Figure 9: 3-layer distributed implementation of component from Figure 2.

  Transform the component with Restriction into a component with only interactions as explained in Subsection 2.4. Then generate a 3-layer distributed model embedding original embedding the

Figure 10 :

 10 Figure 10: Fragment of the dining philosopher component. Braces indicate how interactions are grouped into interaction protocols.

Figure 11 :

 11 Figure 11: Boolean invariant for the Dining Philosophers example with N = 3.

(

  at(P0.thinking) + at(P0.eating) + at(P0.cleaning) = 1) (13) ∧ ∀i ∈ {0, 1, 2}(at(Fi.free) + at(Fi.used) = 1) (14) ∧ (at(P1.eating) + at(P0.eating) + at(P0.cleaning) + at(F1.free) = 1) (15) ∧ (at(P1.thinking)at(P0.eating)at(P0.cleaning) + at(F1.used) + at(P1.cleaning) = 1) (16) ∧ (at(P2.eating)at(P0.eating)at(P0.cleaning) + at(F1.used) + at(P1.cleaning)at(F2.used) = 0) (17) ∧ (at(P2.cleaning) + 2 * at(P0.eating) + at(P0.cleaning)at(F1.used)at(P1.cleaning) + at(F2.used)at(F0.used) = 0) (18) ∧ (at(P2.thinking)at(P0.eating) + at(F0.used) = 1) (19)

Figure 12 :

 12 Figure 12: Linear invariant for the Dining Philosophers example with N = 3.

Figure 13 :

 13 Figure 13: Number of interactions executed in 60s for different implementations of the dining philosophers example. MB: Multiparty-based. RA: Restriction-aware. More interaction = better performance.

Figure 14 :

 14 Figure 14: Number of messages exchanged in 60s for different implementations of the dining philosophers example. MB: Multiparty-based. RA: Restriction-aware. Less message = more efficient implementation.

4 Figure 15 :

 415 Figure 15: Jukebox component with 3 discs.

Figure 16 :Figure 17 :

 1617 Figure 16: Number of interactions executed in 60s for the jukebox example. More interaction = better performance.

Table 1 :

 1 Minimal number of observations for ensuring completeness in the interaction protocol C 0 .

		Size true BI	LI optimal
	Philo3	6	3	3	1	1	Component Size true BI LI
	Philo4	8	5	5	2	2	Philo3	6	9	9	0
	Philo5	10	7	7	3	3	Philo4	8	20	20	4
	Philo10	20	17	17	8	8	Philo5	10	35	35	6
	Philo20	40	37	37	18	18	Philo10	20	170 170 23
	Philo100	200	197	197 108	98

Table 2 :

 2 Minimal number of observations for ensuring baseness in the whole model.

Table 3 :

 3 Minimal observation cost to ensure baseness or completeness.

p-→⊥ q that goes from a stable to a busy state and executes the transition from the original component.

Future work includes further optimization of the conflict resolution protocol through Knowledge, as in [11]. It also includes generating distributed model with timing constraints as in [1]. In particular, the multi-threaded implementation in [46], where all timing constraints are handled by a single thread, could be extended to a fully distributed implementation. Furthermore, Knowledge could be applied as well to determine for instance whether an interaction protocol has to wait for a particular message.

has received funding from the European Community's Seventh Framework Programme [FP7/2007-2013] under grant agreement no. 248776 (PRO3D) and no 257414 (ASCENS) and from ARTEMIS JU grant agreement ARTEMIS-2009-1-100230 (SMECY)

Conflict resolution for Multiparty Interactions. Distributed conflict resolution boils down to solving the committee coordination problem [START_REF] Chandy | Parallel program design: a foundation[END_REF], where a set of professors organize themselves in different committees. A meeting requires the presence of all professors to take place and two committees that have a professor in common cannot meet simultaneously. Different solutions have been provided, using managers [START_REF] Chandy | Parallel program design: a foundation[END_REF][START_REF] Bagrodia | Process synchronization: Design and performance evaluation of distributed algorithms[END_REF][START_REF] Parrow | Multiway synchronizaton verified with coupled simulation[END_REF][START_REF] Pérez | An order-based algorithm for implementing multiparty synchronization[END_REF], a circulating token [START_REF] Kumar | An implementation of n-party synchronization using tokens[END_REF], or a randomized algorithm without managers [START_REF] Joung | Strong interaction fairness via randomization[END_REF].

The solutions provided by Bagrodia [START_REF] Bagrodia | Process synchronization: Design and performance evaluation of distributed algorithms[END_REF] relies on counters to ensure mutual exclusion of conflicting interactions, as explained in Section 4. The token ring and dining philosopher-based solutions allow the designer to use an arbitrary partitions of the interaction for building the different managers. Our solution differ as we separate the conflict resolution from the execution of the interactions.

The α-core protocol [START_REF] Pérez | An order-based algorithm for implementing multiparty synchronization[END_REF] build one manager (called coordinator) per interaction. Contrarily to Bagrodia's solution, this solution does not rely on counters. The principle of the protocol is that each coordinator locks sequentially the components according to a global order. Each component can be locked by only one coordinator. If the coordinator manages to lock all components of the interaction, it executes the interaction. Otherwise, the coordinator frees all components locked so far. As there are no counters, every component must explicitly withdraw all unsuccessful offers when executing an interaction. Furthermore, it must wait for an acknowledgement of the withdrawal before resuming execution, which may incur an overhead compared to a counter-based solution. In [START_REF] Bensalem | Knowledge-based transactional behavior[END_REF], knowledge is used to optimize the conflict resolution protocol α-core [START_REF] Pérez | An order-based algorithm for implementing multiparty synchronization[END_REF].

The solution by Kumar [START_REF] Kumar | An implementation of n-party synchronization using tokens[END_REF] implements an idea similar to the α-core protocol, without managers. Each interaction is represented by a token. There is a global order on the components, and to execute an interaction, the token must traverse (and lock) all the components according to the global order. If a token arrives in a component that has already been locked by another token (i.e. a conflicting interaction), it waits until the interaction either succeeds or fail. If the conflicting interaction fails, the token is propagated. If the conflicting interaction succeeds, the token is stopped and all components it already traversed are unlocked.

The solution provided by Joung and Smolka in [START_REF] Joung | Strong interaction fairness via randomization[END_REF] mainly focus on ensuring fairness between interaction. This algorithm relies on randomization: each component picks an interaction and send a message to all participants. If one of the participants detects that at a given point all participants agree on the interaction, the latter is executed. Otherwise, each component picks another interaction.

Other Frameworks for Process Coordination. Although we use multiparty interactions to describe communication between processes, many solutions enhancing message-passing exist. The MPI framework [START_REF] Gropp | Using MPI-2: Advanced Features of the Message Passing Interface[END_REF] provides collective operations such as MPI Barrier() that implements strong synchronization between a set of processes. However, conflicting interactions are not handled, the programmer has to ensure that all involved processes commit to the same synchronisation.