Marius Bozga

Mohamad Jaber

Nikolaos Maris

Joseph Sifakis

Modeling Dynamic architectures using Dy-BIP

HAL is

Introduction

Architectures are essential for mastering the complexity of systems and facilitate their analysis and evolution. They allow a separation between detailed behavior of components and their overall coordination. Coordination is usually expressed by constraints that define possible interactions between components. There exists a large number of formalisms supporting a concept of architecture, including software component frameworks, systems description languages and hardware description languages. Despite an abundant literature and a considerable volume of research, there is no agreement on a common concept of architecture, while most definitions agree on the core e.g. diagrammatic representations by using connectors. This is due to two main reasons.

First, is the lack of rigorous operational semantics defining architectures as composition operators on components. That is the behavior of a composite component is inferred from the behavior of its constituent components by applying architectural constraints. For existing component frameworks, the definition of rigorous operational semantics runs into many technical difficulties. They fail to clearly separate between behavior of components and architecture. Connectors are not just memoryless switching elements. They can be considered as special types of components with memory e.g. fifo queues and specific behavior. Another difficulty stems from verbose architecture definitions e.g. by using ADLs [START_REF] Medvidovic | A framework for classifying and comparing architecture description languages[END_REF], that do not rely on a minimal set of concepts. Such definitions are hardly amenable to formalization. Finally, some frameworks [START_REF] Garlan | Acme: An architecture description interchange language[END_REF] use declarative languages e.g. first order logic to express global architecture constraints which are useful for checking correctness but as a rule do not provide a basis for defining operational semantics.

The second is the distinction between static and dynamic architectures. Usually, hardware and system description languages rely on static architecture models. The relationships between components are known at design time and are explicitly specified as a set of connectors defining possible interactions. Dynamic architectures are needed for modeling reconfigurable systems or systems that adapt their behavior to changing environments. They are defined as the composition of dynamically changing architecture constraints offered by their constituent components. Filling the gap between static and dynamic architecture models raises a set of interesting problems. In principle, dynamic architecture models are more general: each configuration corresponds to a static architecture model. Is it possible to define a dynamic architecture modeling language as an extension of a static architecture modeling language? Furthermore, if we restrict to systems with a finite -although potentially large -set of possible configurations, any dynamic architecture model can be translated into a static architecture model. Such a translation can yield very complex static architecture models. As a rule, using dynamic architectures may lead to more concise models. However, static architecture models can be executed more efficiently thanks to the global and static knowledge of connectors [START_REF] Allen | Specifying and analyzing dynamic software architectures[END_REF].

We propose the Dy-BIP component framework based on rigorous operational semantics for modeling both static and dynamic architectures. Dy-BIP can be considered as an extension of the BIP language [START_REF] Basu | Rigorous component-based system design using the bip framework[END_REF] for the construction of composite hierarchically structured components from atomic components. These are characterized by their behavior specified as automata extended with data and functions described in C. A transition of an automaton is labeled by a port name, a guard (boolean condition on local data) and an action (computation on local data). In BIP architectures are composition operators on components defining their interactions. An interaction is described as a set of ports from different components. It can be executed if there exists a set of enabled transitions labeled by its ports. The completion of an interaction is followed by the completion of the involved transitions: execution of the corresponding actions followed by a move to the target state. An operational semantics for BIP has been defined in [START_REF] Basu | Distributed semantics and implementation for systems with interaction and priority[END_REF]. It provides a basis for the implementation of an Engine that orchestrates component execution. The Engine knows the set of the interactions modeling the architecture. It executes cyclically and atomically the following three-step protocol: 1) from a state each component sends to the Engine the ports of its enabled transitions; 2) the Engine computes the set of feasible interactions (sets of received ports corresponding to some interaction); 3) the Engine chooses non-deterministically one interaction amongst the feasible interactions by sending back to the components the names of their ports involved in this interaction. Figure 1(a) shows a static architecture defined by interactions pq and qr. Its consists of three components offering communications through ports p, q and r. In contrast to BIP, the set of interactions characterizing architectures in Dy-BIP changes dynamically with states. A port p has an associated architecture constraint C p which describes possible sets of interactions involving p. Feasible interactions from a state are computed as maximal solutions of constraints obtained as the conjunction of constraints offered by enabled transitions. Figure 1(b) illustrates a dynamic architecture with three components offering ports p, q and r with associated constraints C p , C q and C r . As for the static architecture, the possible interactions are pq and qr. p q q r q r p p q r p q r p q q r (a) Static architecture We provide operational semantics for Dy-BIP implemented by an Engine which as for BIP, orchestrates components by executing atomically a three-step protocol. The protocol differs in that components send not only port names of enabled transitions but also their associated architecture constraints.

r p[C p ] q[C q ] p q r[C r ] r p q p q q r q (b) Dynamic architecture
Dy-BIP is an extension of BIP. A BIP model with a global architecture constraint C, can be represented as a Dy-BIP model such that the constraint C p associated with a port p is the set of the interactions of C involving p.

Dy-BIP allows modeling dynamic architectures as the composition of instances of component types. For the sake of simplicity, we assume that there is no dynamic creation/deletion of component instances. The main contributions are the following:

-Definition of a logic for the description of architecture constraints. The logic is expressive and amenable to analysis and execution. It encompasses quantification over instances of component types. Formulas involve port names used as logical variables and characterise sets of interactions. Given a formula, a feasible interaction is any set of ports assigned true by a valuation which satisfies the formula. -Study of a semantic model and a modeling methodology for writing architecture constraints associated with ports. For a port p, the associated constraint is decomposed into three types of constraints characterizing interaction between ports [START_REF] Bliudze | Causal Semantics for the Algebra of Connectors[END_REF]: "causal constraint", "acceptance constraint", "filter constraint". Causal constraint defines the ports required for interaction. Acceptance constraint defines optional ports for participation. Filter constraints are invariants used to discriminate undesirable configurations of a component's environment. -Implementation principles for Engines handling symbolic architecture constraints.

The proposed implementation is based on the resolution of architecture constraints on-the-fly. The Engines use efficient constraint resolution techniques based on BDDs. For a given model, quantifiers over components can be eliminated and formulas become boolean expressions on ports. -Experimental results and benchmarks showing benefits from using dynamic architectures compared to static architectures. We consider several examples showing that compositional modeling of dynamic architectures allows enhanced conciseness and rigorousness. In particular, it is possible to master complexity of intricate dynamic interactions by compositional specification of interactions of individual components.

The paper is structured as follows. Section 2 presents related work. Section 3 describes the semantic model for Dy-BIP. Section 4 presents the dynamic architecture description language and the methodology for writing constraints. Section 5 is dedicated to examples and experimental results. Section 6 concludes and discusses future work directions.

Related work

In contrast to other frameworks [START_REF] Inverardi | Formal specification and analysis of software architectures using the chemical abstract machine model[END_REF][START_REF] Métayer | Describing software architecture styles using graph grammars[END_REF] Dy-BIP relies on a clear distinction between behavior and architecture as a set of stateless architecture constraints characterizing interactions. Architecture constraints are specified compositionally as the conjunction of individual architecture constraints of components. Existing frameworks usually describe dynamic architectures as a set of global transitions between configurations. Only process algebras adopt a compositional approach e.g. pi-calculus [START_REF] Milner | Communicating and mobile systems -the Pi-calculus[END_REF]. Nonetheless, they do not encompass a concept of architecture as behavior and composition operators are intermingled. Dy-BIP differs from other formalisms such as [START_REF] Magee | Dynamic structure in software architectures[END_REF] in that it has rigorous operational semantics. In [START_REF] Garlan | Acme: An architecture description interchange language[END_REF], a first order logic extended with architecture-specific predicates is used. However, there is no clear methodology on how to express synchronisation protocols (e.g., rendezvous, broadcast) whose combination is expressive enough to represent any kind of interaction and avoids the exhaustive enumeration of all possible interactions [START_REF] Bliudze | The algebra of connectors: structuring interaction in bip[END_REF]. In [START_REF] Kim | Analyzing architectural styles[END_REF], a dynamic architecture is defined as a set of global transitions between global configurations. These transitions are expressed in a first order logic extended with architecture-specific predicates. The same logic is used in [START_REF] Kacem | Evaluation and comparison of adl based approaches for the description of dynamic of software architectures[END_REF][START_REF] Georgiadis | Self-organising software architectures for distributed systems[END_REF] but global configurations are computed at runtime from the local constraints of each component. Dy-BIP follows the same approach but constraints are stateless (they are based on the boolean representation of causal rules [START_REF] Bliudze | Causal Semantics for the Algebra of Connectors[END_REF]) and take advantage of the stateful behavior of the components by eliminating some of the undesirable global configurations implicitly. [START_REF] Belguidoum | Dependency management in software component deployment[END_REF] provides an operational semantics based on the composition of global configurations from local ones. These express three forms of dependencies between services (mandatory, optional and negative). Nonetheless, dynamism is supported only at the installation phase.

In BIP [START_REF] Basu | Rigorous component-based system design using the bip framework[END_REF], coordination between components is modeled by using connectors [START_REF] Bliudze | Causal Semantics for the Algebra of Connectors[END_REF]. A simple (or flat) connector is an expression of the form p ′ 1 . . . p ′ k p k+1 . . . p n where primed p ′ i ports are triggers, and unprimed ports p j are synchrons. For a flat connector involving the set of ports {p 1 , . . . , p n }, interaction semantics defines the set of its interactions γ by the following rule: an interaction is any non-empty subset of {p 1 , . . . , p n } which contains some port that is trigger; otherwise (if all ports are synchrons), the only possible interaction is the maximal one, that is p 1 . . . p n . Connectors, representing these two protocols for a sender s and receivers r 1 ; r 2 ; r 3 , are shown in 2-(a,b). Triangles represent triggers, whereas bullets represent synchrons. Hierarchical connectors are expressions composed of types ports and/or typed sub-connectors. Figure 2-c shows a connector realizing an atomic broadcast from a port s to ports r 1 , r 2 , r 3 . The sending port s is trigger, and the three receiving ports are strongly synchronized in a sub-connector itself typed as a synchron. The connector shown in Figure 2-d is a causal chain of interactions initiated by the port s, the possible interactions are s, sr 1 , sr 1 r 2 , sr 1 r 2 r 3 . Connectors can be used to define easily any type of coordination between components. However, in this case connectors and their interactions are defined statically, and this leads to inefficiency for systems with dynamically changing architecture.

✉ ✉ ✉ ✉ s r1 r2 r3 ✉ ✉ ✉ s r1 r2 r3 γ = {sr1r2r3} γ = {s, sr1, sr2, sr3, sr1r2, sr2r3, sr1r2r3} (a) Rendezvous (b) Broadcast ✉ ✉ ✉ ✉ s r1 r2 r3 ✉ ✉ ✉ s r1 r2 s3 γ = {s, sr1r2r3} γ = {s, sr1, sr1r2, sr1r2r3} (

The Dynamic-BIP model

Dy-BIP offers primitives for dynamic architecture modeling. Atomic components are transition systems. Transitions are labeled with ports, that is, action names, and constraints for interaction with other components.

Ports are used to define interactions between atomic components. Henceforth P is a universal set of ports. An interaction is a non empty subset a ⊆ P. To simplify notation, an interaction a = {p 1 , p 2 , . . . p n } is simply denoted by p 1 p 2 . . . p n .

Interaction constraints

To introduce dynamic architectures, we consider that each atomic component provides its own interaction constraints at each computation step. A global interaction is defined as a solution of the set of interaction constraints offered by components. As the interactions at some state may depend on interactions in the past, it is necessary to parametrize interaction constraints by history variables which keep track of the interactions already executed. For example, in a protocol, if A sends a message to B, then A can record the identity of B in a history variable to remember that an acknowledgement is expected from B. If A does not use history variables then it is necessary to encode the identity of the receiver in control locations and this may result in an explosion of the number of its control locations.

Definition 1 (Interaction Constraint). Given a set of history variables H, an interaction constraint C is defined by the following grammar:

C ::= true | p ∈ h | p | ¬C | C ∧ C (1)
where p ∈ P is a port, and h ∈ H is a history variable.

The syntax of interactions constraints is tacitly extended for all boolean operators e.g., false, ⇒, ∨ in the usual way. To simplify notation, we overload the meaning of a port symbol p: within p ∈ h it denotes the port itself whereas p alone denotes a boolean variable. This ambiguity is removed in the two-step definition of semantics given below. We denote by C the set of all interaction constraints and by C b the subset of boolean constraints, that is, without history variables. Given a valuation of history variables µ : H → 2 P , an interaction constraint C ∈ C defines a boolean interaction constraint [[C]] µ by the following rules:

[[true]] µ = true [[p ∈ h]] µ = true if p ∈ µ(h) false otherwise [[p]] µ = p [[¬C]] µ = ¬[[C]] µ [[C 1 ∧ C 2 ]] µ = [[C 1 ]] µ ∧ [[C 2 ]] µ (2)
That is, the terms of the form p ∈ h are replaced by true or false as the case may be: true if port p belongs to the stored interaction and false otherwise. All the other terms of the interaction constraint remain unchanged.

An interaction a ⊆ P satisfies a boolean constraint C ∈ C b (denoted by a |= C), as defined by the following rules:

a |= true a |= p ⇔ p ∈ a a |= ¬C ⇔ ¬(a |= C) a |= C 1 ∧ C 2 ⇔ (a |= C 1 ) ∧ (a |= C 2 ) (3)
We denote with I(C) and I max (C) the set of interactions and respectively maximal interactions satisfying C, formally:

I(C) = {a | a |= C} I max (C) = {a ∈ I(C) | ∄a ′ ∈ I(C) . a ′ ⊃ a} (4)
For example, we can specify interaction constraints for: (1) rendez-vous between p 1 , p 2 , p 3 by

C 1 = (p 1 ⇒ p 2 ) ∧ (p 2 ⇒ p 3 ) ∧ (p 3 ⇒ p 1
), the only possible interaction is the maximal one, that is

I(C 1 ) = I max (C 1 ) = {p 1 p 2 p 3 };
(2) broadcast where s is the sending port and r 1 , r 2 , r 3 are the receiving ports by

C 2 = (true ⇒ s) ∧ (r 1 ⇒ s)∧(r 2 ⇒ s)∧(r 3 ⇒ s), the possible interactions are I(C 2 ) = {s, sr 1 , sr 1 r 2 , sr 1 r 2 r 3 } and I max (C 2 ) = {sr 1 r 2 r 3 };
(3) the constraint p ⇒ false means absence of p from any interaction; (4) p ⇒ true allows inclusion of p in any interaction.

Atomic components

An atomic component is an automaton extended with history variables. Transitions represent relations on control locations (local states). Each transition is labeled by a port, an interaction constraint and a set of history variables to be updated. • p ∈ P , the port offered for interaction • C ∈ C, the interaction constraint on P and H • h ⊆ H, the set of history variables to be updated Given µ : H → 2 P a valuation of the history variables H, the state of an atomic component B = (L, P, H, T ) is a pair (ℓ, µ), where ℓ ∈ L is a control location. Q = L × µ is the set of states ot the atomic component B, where µ denotes the set of valuations on H. For each state (ℓ, µ) ∈ Q, we define its associated state constraint SC(ℓ, µ) as follows:

SC(ℓ, µ) =       ℓ p, C, h -----→ℓ ′   p ∧ [[C]] µ ∧ p ′ ∈P \{p} ¬p ′         ∨ p∈P ¬p (5)
The state constraint characterizes the set of possible contributions of the component to a global interaction at state (ℓ, µ). Either the component executes some transition ℓ p, C, h -----→ ℓ ′ and offers interactions (1) involving p and excluding all other ports labeling transitions from this state, that is, p ∧ p ′ ∈P \{p} ¬p ′ holds and (2) involving ports which satisfy the constraint C for the valuation µ, that is, [[C]] µ . Or, the component does not interact, if none of its ports is used, that is p∈P ¬p.

Composition

A system S = B 1 . . . B n is defined as the composition of a set of atomic components

B i = (L i , P i , H i , T i ) i=1,n .
We assume that the sets of locations, ports and history variables are pairwise disjoint. The semantics of the composition is provided by the following definition.

Definition 3 (Composition). The behavior of a system S = B 1 . . . B n is a labeled transition system (Q, Σ, -→), where,

-Q = n i=1 Q i is the set of states, where Q i is the set of states of component B i ; -Σ = 2 P is the set of interactions, where P = ∪ n i=1 P i ; -- →⊆ Q × Σ × Q
is the set of transitions, defined by the following rule:

{µ i : H i → P } n i=1 a = {p j } j∈J ∈ I max ( n i=1 SC(ℓ i , µ i )) ∀j ∈ J. ℓ j p j , C j , h j -------→ ℓ ′ j j∈J [[C j ]] µj µ ′ j = µ j [a/h j ] ∀j ∈ J. ℓ ′ j = ℓ j µ ′ j = µ j ((ℓ 1 , µ 1 ), . . . , (ℓ n , µ n )) a -→ ((ℓ ′ 1 , µ ′ 1 ), . . . , (ℓ ′ n , µ ′ n ))
Intuitively, system transitions are taken for maximal interactions a that satisfy all state constraints defined by atomic components n i=1 SC(ℓ i , µ i ). The components participating in the interaction change their location according to the selected transition and update their local valuation of history variables. The components which do not participate keep their state unchanged.

The composition semantics has been implemented by using a centralized execution Engine. The Engine gathers current state interaction constraints from all atomic components. Then, it builds the overall system of constraints and solves it, that is, finds the set of maximally satisfying interactions. One maximal interaction is then selected and executed atomically by all involved components. This operation is repeated by the Engine on-the-fly, at every state reached at execution. More formally, atomic components interact and coordinate their execution through the Engine according to the following protocol:

1. Each component B i , computes its state constraint SC(ℓ i , µ i ) and sends it to the Engine. 2. The Engine computes the global constraint GC as the conjunction of state constraints defined by atomic components GC = n i=1 SC(ℓ i , µ i ). 3. The Engine picks some maximal interaction a on P, such that a |= GC. That is, a ∈ I max (GC). 4. The Engine notifies the selected interaction a to all participating components, that is, all B j such that a ∩ P j = ∅. 5. Each notified component B j executes its local transition labeled by p j = a ∩ P j and updates its history variables.

Example 1. Figure 3 shows an example of a composite component consisting of three atomic components B 1 , B 2 , and B 3 . Component B 1 requests synchronization with either B 2 or B 3 , and then performs some computation with the synchronized component.

To do so, we model component B 1 as follows. It has two control locations l 1 , l 2 , two ports s, r, and a history variable h. From control location l 1 , the transition labeled by the port s requests synchronisation with ports b 1 or b 2 (s ⇒ b 1 ∨ b 2 ), forbids the synchronisation with b 1 and b 2 at the same time (¬(b 1 ∧ b 2 )), and forbids the synchronisation with f 1 and f 2 (¬f 1 ∧ ¬f 2 ). After executing this transition, the executed interaction is stored in the history variable h (Update h), to store the identity of the synchronized component. From control location l 2 , the transition labeled by the port r, depending on the value of the history variable h, it either (1) requests synchronisation with port f 1 and forbids the synchronisation with port f 2 ; or (2) requests synchronisation with port f 2 and forbids the synchronisation with port f 1 . In both cases, it forbids the synchronisation with ports b 1 and b 2 (¬b 1 ∧ ¬b 2 ).

From location l 1 the state constraint is SC(l 1 , µ 1 ) = (s ∧ C s ∧ ¬r) ∨ (¬s ∧ ¬r) regardless of the value of µ 1 . This is due to the fact that constraint C s does not depend on

b 1 ⇒ s h Cr = (b1 ∈ h) ⇒ [(r ⇒ f1) ∧ ¬f2] ∧ (b2 ∈ h) ⇒ [(r ⇒ f2) ∧ ¬f1] ∧ ¬b1 ∧ ¬b2 l 1 l 2 s r r s C s Update h C r B 1 l 3 b 1 f 1 B 2 l 5 b 2 f 2 B 3 l 6 l 4 Cs = (s ⇒ b1 ∨ b2) ∧¬(b1 ∧ b2) ∧(¬f1 ∧ ¬f2) f 2 ⇒ r f 2 b 2 b 2 ⇒ s f 1 ⇒ r f 1 b 1
Fig. 3. An example of a composite component in Dy-BIP.

history variables. For this constraint, the possible interactions are I max (SC(l 1 , µ)) = {sb 1 , sb 2 }. From location l 2 , if the history variable h contains the interaction sb 2 , then the state constraint is

SC(l 2 , µ 1 ) = (r ∧ [[C r ]] µ1 ∧ ¬s) ∨ (¬s ∧ ¬r), where [[C r ]] µ1 = false ⇒ [(r ⇒ f 1 ) ∧ ¬f 2 ] ∧ true ⇒ [(r ⇒ f 2 ) ∧ ¬f 1 ] ∧ ¬b 1 ∧ ¬b 2 .
For this constraint, the only possible interaction is I max (SC(l 2 , µ 1 )) = {rf 2 }. Initially, components B 1 , B 2 , and B 3 are in locations l 1 , l 3 , and l 5 , respectively. Starting from these locations, the Engine coordinates execution of these components as follows: (1) Components B 1 , B 2 , and B 3 compute their state constraints SC(l 1 , µ 1 ), SC(l 3 , µ 2 ), and SC(l 5 , µ 3 ), respectively, where, SC(l 1 , µ 1 ) = (s ∧ C s ∧ ¬r) ∨ (¬s ∧ ¬r), SC(l 3 , µ 2 ) = (b 1 ∧(b 1 ⇒ s)∧¬f 1 )∨(¬b 1 ∧¬f 1 ), and SC(l 5 , µ 3 ) = (b 2 ∧(b 2 ⇒ s) ∧ ¬f 2 ) ∨ (¬b 2 ∧ ¬f 2 ); (2) The Engine picks any interaction from I max (SC(l 1 , µ 1 ) ∧ SC(l 3 , µ 2 ) ∧ SC(l 5 , µ 3 )) = {sb 1 , sb 2 }; (3) If the Engine selects the interaction sb 2 , it notifies components B 1 and B 3 ; (4) Components B 1 and B 3 execute their transitions labeled by s and b 2 , respectively. Moreover, component B 1 sets its history variable h to sb 2 .

Methodology for writing interaction constraints

Writing interaction constraints associated with transitions of atomic components, in the proposed declarative language may be error-prone or may lead to incomplete specifications. We provide a methodology based on a classification of constraints and on a set of macro-notations for enhancing soundness and completeness. The classification distinguishes between interactions in which a port p must, may or must not be involved. It allows a systematic analysis of interaction capabilities of components to make sure that no essential properties are omitted. Macro-notations allow a compact and high-level expression of the most commonly used constraints, thus avoiding specification errors.

We extend the interaction constraint language towards a first order logic with quantification over component instances. This extension is useful because in practice, systems are built from multiple, replicated instances of components of different types. The formulas of the logic interaction constraints are therefore defined as follows:

C ::= true | x.p ∈ h | x.p | x = y | x = self | ¬C | C ∧ C | ∀x : T.C(x) (6)
In this definition, T denotes a component type. Each component type represents a set of component instances with identical interfaces and behavior. The variables x, y range over component instances. These variables must occur in the scope of a quantifier, e.g. ∀x : T.C(x). They are strongly typed and moreover, they can be tested for equality. Additionally, self represents a fixed component instance, that is, the (context) component where the constraint belongs. The remaining syntactic constructs are directly lifted from the propositional case: h ∈ H denotes a history variable and x.p denote the port p belonging to component instance x. As previously, we consider the standard extension of this logic for all boolean operators and existential quantification.

In the sequel, we consider systems consisting of finitely many instances for each component type. Under this restriction, an interaction constraint written in the logic above boils down into a propositional interaction constraint by (1) substituting self by the current component instance, (2) elimination of universal quantifiers and (3) evaluation of equality constraints. For example, for a component type T with instances t 1 , . . . t k , universal quantifiers of the form ∀x : T can be eliminated:

∀x : T.C(x) ≡ C(t 1 ) ∧ . . . ∧ C(t k ) (7)
In the rest of this section, we provide guidelines for writing interaction constraints in this logic. Consider a fixed transition in some component (type) which is labeled by a port p. The associated interaction constraint C p is a conjunction of three types of constraints, respectively causal, acceptance and filtering, as explained below.

Causal constraints

These constraints are used to specify the ports required for interactions of p. At propositional level, they can be reduced to the one of the two following forms, either true ⇒ p or p ⇒ C, where C is a boolean interaction constraint without negated ports. To express such constraints in practice, we provide hereafter few useful abbreviations:

-Trigger ≡ true ⇒ self.p. This constraint specifies that port p is a trigger, that is, the transition labeled by Trigger does not require synchronization with transitions of other components to occur. -Require T.q ≡ ∃x : T.(self.p ⇒ x.q). This constraint specifies that an arbitrary instance of component type T must participate with the port q in the interaction involving p. -Require

x 1 .q 1 ...x n .q n [x 1 : T 1 . . . x n : T n |C 1 (x 1 , ..., x n )] ≡ ∃x 1 : T 1 ...∃x n : T n . C 1 (x 1 , ..., x n )∧self.p ⇒ (x 1 .q 1 ∧. . .∧x n .q n )
. This is the most general type of require constraint. It specifies that a set of component instances x 1 , . . . x n satisfying the constraint C 1 (x 1 . . . x n ) must jointly participate with respectively ports q 1 , . . . q n in the interaction involving p. Usually, the constraint C 1 is used to check previous participation of x 1 . . . x n in interactions recorded into history variables.

Acceptance constraints

These constraints define optional ports for participation used to define the boundary of interactions. They are expressed by excluding explicitly from interactions all the ports that are not optional. At propositional level, they are of the form r ⇒ false where port r is excluded from interaction. In practice, we use the following abbreviations:

-Accept T.q ≡ (T ′ ,q ′ ) =(T,q) ∀x : T ′ . x.q ′ = self.p ⇒ (x.q ′ ⇒ false) . This constraint accepts only ports q of component instances of type T .

-Accept x.q[x : T |x.r ∈ h] ≡ Accept T.q ∧ ∀x : T. x.r ∈ h ⇒ (x.q ⇒ false) .
This constraint restricts participation to ports of component instances x that had participated in the interaction stored in h.

Filtering constraints

These constraints are used to exclude some of interactions allowed by causal and acceptance constraints. At propositional level, filter constraints are of the form p ⇒ C where each monomial in C has at least one negated port. In practice, we are commonly requiring unicity constraints of the form:

-Unique T.q ≡ ∀x : T.∀y : T. (x.q ∧ y.q ⇒ x = y). This constraint forbids the participation of p with more than one instance of component type T with the port q.

Experimental results

The operational semantics of Dy-BIP has been implemented using the CUDD BDD package 1 . We compare execution times for Dy-BIP and BIP (where we define architecture statically) for a Master-Slave example. Two other non-trivial examples, Fault-Tolerant Servers, and Tracker and Peers are provided. Static architecture modeling for these examples in BIP leads to complex descriptions and may be error-prone. Dy-BIP models are concise and can be efficiently implemented. We present below the three examples and the simulation results. Execution times are provided for executing 1000 interactions of the Engine running on PC Quad-Xeon 2.67HGz with 6GB RAM.

Masters and Slaves

In this example, we consider two scenarios. In the first scenario, is a system consisting of M Masters and S Slaves. Each Master sends requests sequentially to two Slaves, and then performs some computation involving both of them. The model of the Master component type is shown in Figure 4(a). Initially, from location 0, a Master requests synchronization with some Slave. To do so, it must synchronize his request port with the get port of any Slave (Require Slave.get). As it requires one and only one Slave, we add a Unique constraint. When a Master instance m 1 synchronizes with some Slave instance, say s 1 , interaction m 1 .req s 1 .get is chosen. Then, the Master m 1 has to keep track of the identity of the synchronized Slave (s 1 ) by saving the interaction m 1 .req s 1 .get to the history variable h 1 (Update h 1 ). From location 1 the Master requires another Slave to synchronize with it, and keeps again track of its identity. Finally, from location 2, the Master establishes a ternary interaction with the two Slaves recorded in its history variables. The Slave component type is shown if Figure 4(b). It accepts a request and provides a response. In order to allow participation in ternary interactions, the Accept clause includes the port of one Master and the work port of another Slave. Notice that, the statically predefined connector structure (using BIP) needs M × S + M × S × (S -1) interactions. Figure 5

Fault-Tolerant Servers

This example is inspired from the Fault-Tolerant Client-Server System presented in [START_REF] Allen | Specifying and analyzing dynamic software architectures[END_REF]. We consider a system consisting of a fixed number of available Servers and a pool of alternative Servers used in case of crash. When a Server crashes, another Server is turned on to preserve availability of the service, and so on. After successive crashes, we get a chain of Servers s 1 . . . s t where s 1 . . . s t-1 are crashed and s t is available.

Crashes in this example are software crashes like a memory error, so turning off and on a crashed Server is also a way of repairing it through an action called softrepair.

Additionally, whenever a crashed Server s i gets repaired, then the running Server in the chain should turn off s t and all crashed Server that replaced the repaired Server (s j , i + 1 < j < t) provide a softrepair. example with four Servers: (1) the first Server is turned on while all the others are turned off; (2) the first Server crashes and turns on the second Server; (3) the second Server crashes and turns on the third Server; (4) the first Server gets repaired. In this case, the third Server must be turned off and the crashed Server (the second one) has to turn off by executing softrepair. Notice that, the decision of turning off a running Server has to be propagated from the repaired Server. Also, Servers have to change state synchronously to keep constant the number of available Servers.

The model of a Server component is shown in Figure 8. Moreover, we use the plus symbol "+" to denote logical disjunction of require constraints involving several ports determined by the same expression. For instance, Require x.repair+x.sof trepair[x :

Server | x.crash ∈ h 2 ] ≡ Require x.repair[x : Server | x.crash ∈ h 2 ] ∨ Require x.sof trepair[x : Server | x.crash ∈ h 2 ].
A turnoff requires a repair or a softrepair from any Server that has crashed.

Notice that, statically predefined connector structure (using BIP) leads to more than N N interactions, where N is the total number of Servers. For this reason, modeling statically this architecture is practically impossible even for a relatively small number of Servers. Figure 9 Servers with 13 available Servers, executing 1000 interactions requires only 8 seconds. Notice that, using BIP we have to statically define more than 27 27 interactions!

Trackers and Peers

As third benchmark, we consider a simplified wireless audio protocol for reliable multicast communication. The protocol allows an arbitrary numbers of participants (named Peers) to dynamically connect and communicate along an arbitrary number of wireless communication channels (managed by dedicated Trackers).

In this protocol, Peers are allowed to use at most one communication channel at a time. The access to channels is subject to an explicit registration mechanism. Dynamically, every Peer selects and registers to the channel it wants to use. Once registered, Peers can either speak, that is, send data over the channel, or listen, that is, receive data sent by others. For every channel, its associated Tracker ensures for any communication that (1) exactly one registered peer (on that channel) is speaking and (2) all other registered peers are listening. That is, data is delivered atomically to all potential receivers. Finally, Peers can dynamically de-register, then register to other channels, etc.

The Dy-BIP model is depicted in Figure 10. As for the previous example, we use the "+" abbreviation for disjunction of require constraints applied to several ports. Notice that, a statically predefined connector structure is exponentially complex and the model explodes rapidly. We need P × T × (3 + 2 P -1 ) connectors, where P is the total number of Peers and T is the total number of Trackers.

Conclusion

The paper provides a simple modeling language for compositional description of dynamic architectures. The language as a straightforward extension of a static architecture modeling language, bridges the gap between static and dynamic description styles. It is simple but expressive enough as illustrated by non-trivial examples. Its associated modeling methodology leads to concise and intelligible models obtained as the composition of components. Global architecture constraints can be synthesized by composing architecture constraints of individual components. Using history variables in components avoids state explosion and duplication of ports.

This work contrasts with existing approaches for dynamic architectures which lack clear semantics and are not compositional. It proposes a rigorous methodology for writ-ing architecture constraints of components. In particular, the distinction between different types of constraints provides guidance for their soundness and completeness. The choice between different implementations permits exploration efficiency trade-offs. Onthe-fly computation seems more adequate for architectures with a large number of configurations while regular BIP execution is more advantageous for systems with a small number of configurations.

Further developments will focus on integrating data transfer, priorities, as well as creation and deletion of components.

Fig. 1 .

 1 Fig. 1. Static and dynamic architecture.

Fig. 2 .

 2 Fig. 2. Graphic representation of connectors

Fig. 4 .Fig. 5 .

 45 Fig. 4. Masters and Slaves in Dy-BIP.BIP, as a function of the number of components in the system. Dy-BIP considerably outperforms BIP. Figure5(b)shows the number of the interactions created dynamically for Dy-BIP along the evolution of the system for 20 Masters and 40 Slaves. Notice that, for BIP the number of the interactions created is 32000 regardless of the system state.

Fig. 6 .

 6 Fig. 6. Simple Master-Slave in Dy-BIP.

Figure 5 .Fig. 7 .

 57 Fig. 7. Possible scenario for Fault-Tolerant Client-Server.

Fig. 8 .

 8 Fig. 8. Fault-Tolerant Servers in Dy-BIP.

Fig. 9 .

 9 Fig. 9. Execution times for Fault-Tolerant Servers and Trackers and Peers.

Fig. 10 .

 10 Fig. 10. Trackers and Peers in Dy-BIP.

Figure 9 (

 9 Figure 9(b) shows execution times for 1000 interactions for a Dy-BIP model where there are four times more Peers than Trackers.

  (a) shows execution times of 1000 interactions for BIP and Dy-

	req	req		get
	Require Slave.get	Require x.get[x : Slave | x.get / ∈ h1]	Require M aster.req
	Accept Slave.get	Accept x.get[x : Slave | x.get / ∈ h1]	Accept M aster.req
	Unique Slave.get	Unique Slave.get		Unique M aster.req
	Update h1	Update h2		Update h
	req	req		get
	0	1	2	0	1
	compute			work
	compute			work
	Require x.work y.work[x : Slave | x.get ∈ h1]		Require x.compute
		[y : Slave | y.get ∈ h2]		[x : M aster | x.req ∈ h]
	Accept x.work y.work[x : Slave | x.get ∈ h1]		Accept Slave.work x.compute
		[y : Slave | y.get ∈ h2]		[x : M aster | x.req ∈ h]
	(a) Master type

  (a) depicts execution time for Dy-BIP. For a total number of 27 Accept Server.repair Server.sof trepair Server.turnof f Require x.repair + x.sof trepair Accept Server.repair Server.sof trepair Server.turnof f Require x.turnof f + x.sof trepair[x : Server | x.turnon ∈ h1]

	turnof f		repair
	[x : Server | x.crash ∈ h2]
	Accept Server.repair Server.sof trepair	Unique Server.turnof f
		turnof f			repair
	of f	turnon turnon	on	crash	crash	crash
		Require Server.crash		Require Server.turnon
		Accept Server.crash		Accept Server.turnon
		Unique Server.crash		Unique Server.turnon
		Update h2		Update h1
	sof trepair

Require x.repair y.turnof f + x.repair y.sof trepair + x.sof trepair y.sof trepair + x.sof trepair y.turnof f [x : Server | x.crash ∈ h2][y : Server | y.turnon ∈ h1]

⋆ This work is partially supported by the FP7 IP ASCENS.

CUDD: CU decision diagram package (http://vlsi.colorado.edu/˜fabio/CUDD/)


Joseph Sifakis

Saddek Bensalem

Marius Bozga

Jean Quilbeuf

Knowledge-based Distributed Conflict Resolution for Multiparty Interactions and Priorities

Keywords: Saddek Bensalem, Marius Bozga, Jean Quilbeuf, Distributed System, Priorities, Knowledge, Partial Observation, Multiparty Interactions

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Systems of communicating processes are a very common model for concurrent systems. Processes have their own data space and can interact by executing interactions, which are atomic synchronization operations involving a simultaneous state change of the set of the processes involved. The meaning of interactions can be specified compositionally by using operational semantics. Specifications are given in the form of rules. The premises include facts about the capabilities of individual processes to execute an action. The conclusion describes interactions, that is, transitions of the system obtained as the composition of actions executed by individual processes. In addition to interactions, operational semantics rules can be used to express priorities between interactions. These are parameterized by a priority order between interactions. They express the fact that some interaction may be executed only if interactions of higher priority are disabled. Priorities are instrumental for specifying scheduling policies [START_REF] Gössler | Priority systems. In: Formal Methods for Components and Objects[END_REF].

The distributed implementation of systems of communicating processes raises several non trivial problems. It should be consistent with the operational semantics of multiparty interaction which assumes knowledge of the global system states. Furthermore, multiparty interactions should be replaced in distributed implementations by protocols based on asynchronous message passing.

The BIP component framework [START_REF] Basu | Modeling heterogeneous real-time components in BIP[END_REF] allows the construction of composite components from a set of atomic components by using layered parameterized composition of two types of operators: 1) operators parameterized by a set of interactions which are sets of ports of the atomic components that must synchronize; 2) operators parameterized by priorities between interactions. We proposed a distributed implementation method involving a set of transformations from the initial global state model with multiparty interactions to a distributed model that can be directly implemented [START_REF] Bonakdarpour | From high-level component-based models to distributed implementations[END_REF][START_REF] Bonakdarpour | A framework for automated distributed implementation of component-based models[END_REF]. This method has been extended to handle priorities [START_REF] Bonakdarpour | Automated distributed implementation of component-based models with priorities[END_REF]. The target model consists of components representing processes and interactions representing asynchronous message passing. Correct coordination is achieved through additional components implementing conflict resolution protocols that resolve two types of potential conflicts:

1. The first type of conflicts is symmetric conflicts between interactions. Such conflicts arise when two interactions a and b involve a common component. Since execution of interactions is atomic, execution of interaction a requires ensuring that b will not take place concurrently. Thus execution of a requires permission from some conflict resolution protocol. 2. The second type of conflicts is asymmetric conflicts between interactions related by priorities. Execution of interaction a dominated by interaction b is allowed only if some conflict resolution protocol ensures that b is not enabled.

Conflict resolution protocols are solicited for all potential statically computed conflicts according to a structural analysis of a BIP composite component. This may lead to huge implementation overhead for systems with large numbers of potentially conflicting interactions. Is it possible to reduce this overhead based on a priori knowledge of the system's dynamics and decide that some potential conflicts are not real conflicts?

We denote by a#b the fact that there is a potential conflict between interactions a and b. A false conflict state for interaction a is a state where a is enabled and all other interactions b such that a#b are disabled. In such a state, interaction a can be executed independently without arbitration by the conflict resolution protocol. States where a is in a false conflict are characterized by the predicate F C a = EN a ∧ a#b ¬EN b where EN x is the state predicate characterizing all the states from which interaction x can be executed.

The aim of the paper is to study whether partial knowledge of the system's state is sufficient for deciding when a potential conflict is a false conflict. In that case, execution of interactions can directly take place, without arbitration and thus, reduce communication with the conflict resolution protocol for a more efficient implementation. The concept of knowledge [START_REF] Fagin | Reasoning about Knowledge[END_REF] has been extensively studied for distributed systems in particular with respect to their ability to execute actions [START_REF] Halpern | Modelling knowledge and action in distributed systems[END_REF]. Distributed Knowledge [START_REF] Halpern | Knowledge and common knowledge in a distributed environment[END_REF] allows a set of components to "know" that an interaction is in a false conflict. We assume that each interaction a observes the states of a set of components L a . The knowledge predicate denoted K La F C a characterizes the states where observing only components in L a is sufficient to ensure that F C a holds. In other words, it characterizes states where the distributed knowledge of the set of components L a allows detection of false conflicts for a. We propose conditions for basic and complete implementation, respectively. In a basic implementation, it is possible to detect for each state at least one amongst the false conflicts of the global state model. In a complete implementation all false conflicts of the global state model are detected.

An interesting problem is to minimize the number of observed components, while achieving either basic or complete detection of false conflicts. To this end, we propose heuristics based on simulated annealing strategy [START_REF] Kirkpatrick | Optimization by simulated annealing[END_REF].

A predicate ϕ is known to be true for a partial state observed on components L, that is K L ϕ, if it holds in all reachable global states extending this partial state. However, computing the reachable states of a model is not always tractable. Therefore, we use invariants that over-approximate the set of reachable states. Depending on the invariant used, we obtain different results for the minimization heuristics and different performance for the implementation.

The paper is structured as follows: Section 2 provides a formal definition of the BIP global state semantics. In Section 3, we propose a definition of knowledge in the BIP context and we use it to formalize false conflict detection, and detection levels. We provide in Section 4, heuristics based on a simulated annealing strategy to minimize the number of observed components while ensuring a given detection level. In Section 5, we apply false conflict detection to implementation of priorities. We show results about both heuristics from Section 4 and an actual distributed implementation based on [START_REF] Bonakdarpour | From high-level component-based models to distributed implementations[END_REF][START_REF] Bonakdarpour | A framework for automated distributed implementation of component-based models[END_REF] that uses false conflicts to implement priority resolution. Finally, we present related work in Section 6, concluding remarks and future work in Section 7.

The BIP Framework

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. Atomic Components. An atomic component B is a labelled transition system represented by a tuple (Q, P, T ) where Q is a set of control locations or states, P is a set of communication ports and T ⊆ Q × P × Q is a set of transitions. Interactions. In order to compose a set of n atomic components {B i = (Q i , P i , T i )} n i=1 , 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. We denote a = {p i } i∈I with I ⊆ {1..n} and p i ∈ P i . If a is an interaction, we denote by support (a) the set of atomic components that participate in a. This notation is extended to sets of interactions γ, that is,

support (γ) def = a∈γ support (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 the fact 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 , P i , T i )} n i=1
composed by a set of interactions γ and a priority π ⊆ γ × γ. If π is the empty relation, then we may 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, γ, → πγ ), where Q = n i=1 Q i and → γ , → πγ
are the least set of transitions satisfying the rules: Example 1. A BIP component is depicted in Figure 1 using a graphical notation. It consists of two atomic components named M and S. Component S is a server, that may receive requests (req) and acknowledge them (ack). 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 lines connecting the interacting ports. There are 4 unary interactions and 2 binary interactions. The component goes up through the interaction on and down through off , which are both binary interactions. Priorities rb π req and rb π ack are used to prevent a reboot whenever a request or an acknowledgement are possible.

a = {p i } i∈I ∈ γ ∀i ∈ I. (q i , p i , q ′ i ) ∈ T i ∀i ∈ I. 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]
Invariants and reachable states.

Let B = πγ(B 1 , • • • , B n ) be a component.
We say that the state q is reachable from a fixed, 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(B) the set of reachable states of B. An invariant of B is a state predicate I(q) satisfied by all its reachable states, that is the characteristic set of I contains the set of the reachable states. For a control location q i ∈ Q i , we define the predicate at (q i ) which is true (or equal to 1) when the atomic component B i is at control location q i . We are interested in two types of invariants that can be generated automatically [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF], respectively:

-A boolean invariant is a conjunction of boolean constraints of the form j∈J at (q j ). For the example of Figure 1, at (on up ) ∨ at (on) ∨ at (dwn) is a boolean invariant. 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].

-A linear invariant is a conjunction of linear constraints of the form j∈J k j at (q j ) = k 0 , where each k j and k 0 are integer constants. For the example of Figure 1, at (on up ) + at (on) + at (dwn) = 1 is a linear invariant. Linear invariants are obtained using algebraic methods as described in [START_REF] Krckeberg | 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 and avoids state space exploration.

Knowledge-based Detection of False Conflicts

We propose a knowledge-based method for detecting false conflicts, that is states where an interaction is enabled and all conflicting interactions are disabled. The enabled interaction can be safely executed without any arbitration. In this section, we consider a component B = πγ(B 1 , . . . , B n ) and an invariant I of B.

Knowledge and Indistinguishability

The knowledge of a set of atomic components L ⊆ {B 1 , • • • , B n } is the set of the facts that are true by observing the states of these components. The subset L induces an equivalence relation on the global states satisfying I.

Definition 1 (Indistinguishability Equivalence for L). Given L, we define the indistinguishability equivalence ∼ L on global states satisfying I as q ∼ L q ′ iff ∀B j ∈ L. q j = q ′ j .

L P L I L K L ¬P L I L K L P L I Fig. 2.
Knowledge-based approximation of P for observation L, using invariant I.

Intuitively, two states are indistinguishable for L if their restrictions to the states of atomic components of L are identical. The equivalence classes of this relation correspond to sets of global states that can be distinguished by knowing only local states of atomic components satisfying L. Given an invariant I and an arbitrary state predicate P =⇒ I, we define the predicate "L knows P " as

K L P (q) = I(q) ∧ (∀q ′ I(q ′ ) ∧ q ′ ∼ L q =⇒ P (q ′ )).
Figure 2 illustrates K L P with respect to P and I. Each global state within I 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 P . In the middle, the gray region represents the characteristic set of "L knows P " that is the set of the global states where observation of their projection on the state space of L suffices to assert "P is true". On the right, the gray region represents the set of the states where "L knows not P " that is the set of the global states where observation on L suffices to assert "P is false".

Conflict-free Semantics

For an interaction a, we denote by EN a the predicate that characterizes the set of global states of I where a is enabled. Formally, if a = {p i } i∈I we define EN a def = pi∈a EN i pi ∧ I. By EN i pi we denoted the local enabling condition of the port

p i in atomic component B i = (Q i , P i , T i ) that is EN i pi def = (qi,pi,-)∈Ti at(q i ).
As pointed out in the introduction, we denote by # a conflict relation between interactions. False conflicts for a correspond to the states where the predicate F C a = EN a ∧ a#b ¬EN b holds, that is states where a is enabled and all interactions conflicting with a are disabled. We consider executions of the component where only non-conflicting interactions are allowed.

Definition 2 (Conflict-free Semantics). Given a component B = πγ(B 1 , . . . , B n ) and a conflict relation # , we define the conflict-free semantics of B as a transition system (Q, γ, → F C ), where → F C is the least set of transitions satisfying:

a ∈ γ F C a (q) q a → πγ q ′ q a → F C q ′
The conflict-free semantics → F C is clearly included in the original semantics → πγ of the component. The interest of this semantics is that it captures the set of executions that can be realized without any conflict resolution mechanism. Note that if we consider the priority conflict relation (i.e. we take # = π), then F C a (q) is true only when q a → πγ and q b πγ for all b with higher priority than a. Thus in this particular case → F C =→ πγ . The above semantic rule assumes knowledge of the global state.

Observational Conflict-free Semantics

We now propose to restrict the execution semantics presented above by using only a partial observation of the global state. We allow for each interaction a to "observe" a set of atomic components L a including the atomic components involved in a.

Definition 3 (Observation). Given an interaction a, an observation is a set of atomic components L a such that support(a) ⊆ L a .

Knowledge defines a natural way to describe the false conflicts that can be detected based on an observation. That is, K La F C a characterizes the set of the states where the observation L a detects that a is in false conflict.

Proposition 1 (Monotoncity). The predicate K La F C a is monotonic with re- spect to L a , i.e. L ′ a ⊆ L a implies K L ′ a F C a =⇒ K La F C a . Proof. First, remark that if L ′ a ⊆ L a , then {q ′ |q ′ ∼ La q} ⊆ {q ′ |q ′ ∼ L ′ a q}. Then, K L ′
a F C a (q) implies that ∀q ′ , q ′ ∼ L ′ a q, F C a (q ′ ) and by the above remark ∀q ′ , q ′ ∼ La q, F C a (q ′ ), that is, K La F C a (q). ⊓ ⊔ Notice that observing the whole system, that is for L a = {B 1 , . . . B n }, then it is possible to detect all false conflicts, i.e. K {B1,...Bn} F C a = F C a .

We define a new semantics that allows only interactions detected to be in a false conflict. In such a semantics, observation is used to decide whether a conflict-free move is allowed or not.

Definition 4 (Observational Conflict-free Semantics). Given a component B = πγ(B 1 , • • • , B n ), a conflict relation #, and a set of observations {L a } a∈γ , we define observational conflict-free semantics of B as a transition system (Q, γ, ), where is the least set of transitions satisfying:

a ∈ γ K La F C a (q) q a → πγ q ′ q a q ′
Again, we clearly have included in → πγ . However, depending on the observed atomic components, this semantics may not completely implement → F C . We define two criteria characterizing different levels of false conflict detection, namely basic and complete.

Definition 5 (Detection level). A set of observations {L

a } a∈γ is basic iff a∈γ K La F C a = a∈γ F C a . A set of observations is complete iff for each interaction a ∈ γ: K La F C a = F C a
Theorem 1 below, relates the detection levels and observational conflict-free semantics. Baseness ensures that observational conflicts-free semantics does not introduce deadlocks. Completeness ensures that observational conflict-free semantics corresponds exactly to the conflict-free semantics. This is particularly interesting for the case of priority conflict where the conflict-free semantics is the same as the original semantics of the component.

Theorem 1. Let πγ(B 1 , • • • , B n ) be a component, # a conflict
relation and {L a } a∈γ a set of observations. Then, ⊆→ F C and:

1. If {L a } a∈γ is basic, then q ∈ Q is a deadlock for only if q is a deadlock for → F C . 2. If {L a } a∈γ is complete, then =→ F C . Proof. Since K La F C a =⇒ K {B1,••• ,Bn} F C a (proposition 1) we have ⊆→ F C .
1. By contraposition, let q ∈ Q be a deadlock-free state for → F C , i.e. such that ∃a ∈ γ, F C a (q). Baseness ensures that a∈γ K La F C a holds and thus ∃b ∈ γ such that K L b F C b (q). Thus q b and q is a deadlock-free state for .

2. Assume that q a → F C q ′ . Then F C a (q) and completeness ensures K La F C a (q). Thus q a q ′ . ⊓ ⊔ These results characterize to what extent conflict-free semantics, can be captured through partial observation. They can be used in a distributed implementation where the process responsible for executing interaction a can only see the states of atomic components in L a . However, adding observation increases communication between processes, which may slow down execution. Therefore, we propose in the next section heuristics to minimize the number of observed atomic components, yet ensuring the required detection level.

Heuristics for Minimizing Observation

Given a BIP component and a conflict relation, we want to minimize the number of observed atomic components while ensuring either baseness or completeness. For practical reasons, we consider that a single process may coordinate the execution of several interactions. We call such a process an engine. All interactions managed by the same engine share a common set of observed atomic components. We consider that the mapping of interactions γ into engines is defined by an arbitrary, fixed partition of γ as 1≤j≤m γ j . An engine E j is used to execute interactions in γ j while observing a set of atomic components L j . With these notations, minimizing observation means minimizing the sum m j=1 |L j |. We propose a solution to the minimizing observation problem based on simulated annealing [START_REF] Kirkpatrick | Optimization by simulated annealing[END_REF]. A pseudo-code for the heuristic is shown in Algorithm 1. This heuristic allows on to search for optimal solutions to arbitrary cost optimization

Algorithm 1 Pseudo-code of Simulated Annealing

Input: An initial solution init, a cost function, an alter function. Output: A solution with a minimized cost.

1: sol:=init 2: T :=Tmax 3: while T > Tmin do 4: sol ′ := alter(sol) 5:

∆ := cost(sol ′ )cost(sol)

6:

if ∆ < 0 or random() < e -∆ T then 7:

sol:=sol ′ 8:

end if 9:

T := 0.99 × T 10: end while 11: return sol problems. The search through the solution space is controlled by a temperature parameter T . At every iteration, temperature decreases slowly (line 9) and the current solution 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 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. Now, 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 5, checking for completeness is performed interaction by interaction, Therefore, minimizing observation can be carried out independently for each engine. Given the set of interactions γ j we are seeking for a minimal set of atomic components L j , whose observation ensures complete detection of false conflicts for all interactions in γ j .

Algorithm 2 Function alter for ensuring complete detection of false conflicts

Input: A BIP component B, a subset of interactions γj , a conflict relation # and a solution Lj . Output: A solution L ′ j that is a neighbor of Lj . 1:

L ′ j :=Lj 2: choose Bi in L ′ j \ support(γj ) 3: L ′ j :=L ′ j \{Bi} //perturbation 4: while not complete(L ′ j , γj ) do 5: choose Bi in {B1, . . . , Bn} \ L ′ j 6: L ′ j :=L ′ j ∪ {Bi} //completion 7: end while 8: choose B ′ i in L ′ j \ support(γj ) 9: while complete(L ′ j \ {B ′ i }, γj ) do 10: L ′ j :=L ′ j \ {B ′ i } //reduction 11: choose B ′ i in L ′ j \ support(γj ) 12: end while 13: return L ′ j
The initial solution is obtained by taking the set of atomic components involved in interactions conflicting with those of γ j , that is init j = a∈γj (support(a) ∪ a#b support(b)). 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), possibly breaking completeness. Then, new atomic components are added randomly until the solution ensures complete detection again (completion). Finally, atomic components are removed randomly (reduction).

After completion and during reduction steps, completeness is ensured by checking the condition complete(L j , γ j ) ≡ a∈γj F C a = K Lj F C a . On termination, this ensures that the solution returned by the heuristic is complete.

The cost of the solution is obtained by counting the number of atomic components additionally observed by each engine. That is, for an engine E j the cost of solution L j is cost(L j ) = |L j \ support(γ j )|. Ensuring Baseness. Baseness is achieved if for every state which contains false conflicts, at least one engine detects one of them. Baseness is a global property that can be ensured by cooperation between engines. On one hand, allowing an engine E j to observe additional atomic components may extend the set of false conflicts detected by E j . On the other hand, reducing observation of E j , while restricting the set of false conflicts detected, might not necessarily break the baseness. Therefore, the solution L 1 , • • • , L m to the minimizing observation ensuring baseness cannot be built independently for each engine. Given a partition γ 1 , • • • , γ m of the interactions, we build a tuple of sets of atomic components

L = (L 1 , • • • , L m ) ensuring baseness.
L ′ k :=L ′ k ∪ {Bi} //completion 7: end while 8: choose k in 1, m and B ′ i in L ′ k \ support(γ k ) 9: while basic((L ′ 1 , . . . , L ′ k \ {B ′ i }, . . . , L ′ m ), {γ1, . . . , γm}) do 10: L ′ k :=L ′ k \ {B ′ i } //reduction 11: choose k in 1, m and B ′ i in L ′ k \ support(γ k ) 12: end while 13: return L ′
The initial solution assumes that each engine E j observes all atomic components involved in interactions conflicting with those of γ j , that is init = (init 1 , . . . , init m ). 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 tuple of sets of observed atomic components, instead of a single set.

After completion and during reduction steps, baseness is ensured by the condition basic (L, {γ 1 , . . . , γ m }) ≡ a∈γ F C a = m j=1 a∈γj K Lj F C a . This guarantees that the returned solution is basic.

Here the cost of the solution is the sum of the number of additional atomic components observed by each engine. Thus, we define the cost function as

cost(L) = m j=1 |L j \ support (γ j )|.

Implementation and Experiments

In this section, we provide experiments related to detection of false priority conflicts. We apply our simulated annealing heuristics to compute minimal basic or complete solutions for two examples. Then we provide performance gains for the corresponding distributed implementations.

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 3. 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. We evaluate two different partitions. In Partition 1, there is one engine E i for every eat i interaction and one engine C i for every pair cleanright i-1 , cleanleft i . Only the latter deals with low priority interactions and therefore may need to observe additional atomic components. Partition 2 is coarser. One engine E i manages all interactions involving philosopher P 2i or P 2i+1 , for 0 ≤ i < ⌈N/2⌉. Thus, for N philosophers, there are ⌈N/2⌉ engines. Computing complete solutions is done independently for each engine. number of atomic components in the composite component is indicated in Column Size. Columns true, BI and LI provide the cost of the solutions obtained when using respectively true, the boolean invariant and the linear invariant as invariant I. The column optimal indicates the cost of an optimal solution. ∀i ∈ {0, 1, 2} (at(Fi.f ree) ∨ at(Fi.used))

eat i eat i-1 E i eat i+1 cleanlef t i cleanright i cleanright i-1 cleanlef t i+1 C i C i+1
∧ ∀i ∈ {0, 1, 2} (at (Pi.thinking) ∨ at (Pi.eating) ∨ at(Pi.cleaning)) (1)
∧ (at(P1.eating) ∨ at (P0.eating) ∨ at (P0.cleaning) ∨ at(F1.f ree)) (2)
∧ (at(P2.eating) ∨ at (P1.eating) ∨ at (P1.cleaning) ∨ at(F2.f ree)) (3)
∧ (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.f ree) ∨ at (P2.eating) ∨ at (P0.eating))

∧ (at (F1.f ree) ∨ at (F2.f ree) ∨ at(F0.f ree) ∨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.f ree) ∨ at (P0.eating)) ( 10)

∧ (at(F1.f ree) ∨ at(P1.eating) ∨ at (F0.used) ∨ at(P0.cleaning) ∨ at(P2.thinking)) (11)
∧ (at(P0.thinking) ∨ at(F2.f ree) ∨ at(F1.used) ∨ at (P2.eating) ∨ at(P1.cleaning))

Fig. 4. Boolean invariant for the Dining Philosophers example with N = 3.

Here, the linear invariant gives better results than the boolean invariant, which does not give enough information about the system to reduce observation comparatively to the true invariant. For N = 3, we provide the boolean and linear invariants respectively in Figures 4 and5. In this case, the linear constraint [START_REF] Bagrodia | Process synchronization: Design and performance evaluation of distributed algorithms[END_REF] in linear invariant 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] Bagrodia | Process synchronization: Design and performance evaluation of distributed algorithms[END_REF] would be equal to 2.

(at (P0.thinking) + at (P0.eating) + at (P0.cleaning) = 1) (13)

∧

∀i ∈ {0, 1, 2} (at (Fi.f ree) + at (Fi.used) = 1) ( 14) 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.

∧
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 atomic component), therefore the cost is 0.

Performance Evaluation. We used the tool-chain described in [START_REF] Bonakdarpour | From high-level component-based models to distributed implementations[END_REF][START_REF] Bonakdarpour | A framework for automated distributed implementation of component-based models[END_REF] to generate automatically distributed code from the component. The generated code consists of a set of C++ programs communicating through Unix sockets. We generate one program for each atomic component, one program for each engine and one program for conflict resolution between engines (CRP). We executed these programs in a distributed setting (on a UltraSparcT1 with 24 parallel threads) during 60 seconds and counted the number of "eat" interactions.

Performance for Partition 1 (resp. Partition 2) is depicted in Figure 6 (resp. 7). We do not show performance for the boolean invariant because it falls back to observing all components, as for the true invariant. Since Partition 2 is coarser than Partition 1, it allows less parallelism as shown by comparing performance of execution without priority. Priority limits the number of executions as it enforces a particular scheduling policy and reduces parallelism. For both partitions, the fastest prioritized implementation is the complete one obtained by using the linear invariant. When we observe all involved atomic components (i.e. the invariant is true), performance is worse because the lack of knowledge about the reachable states entails more synchronization overhead. Finally, basic solutions are slow because, while restricting the communication, they also restrict the parallelism.

Jukebox

The second example is a jukebox depicted in Figure 8. It represents a system, where a set of readers R 1 . . . R 4 access data located on 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. Interactions load i,k and unload i,k allows to load and unload 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 3 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}. We use a partition assigning one engine per interaction. Results of the simulated annealing heuristic are presented in Table 3. Engines 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, the same level of detection is achieved with less observed atomic components. Performance Evaluation. We generate C++ code, as for the previous example. We count the number of "read" interactions that take place during 60 seconds of execution, for different settings. In Figure 9, we provide results for a version of the component without priorities, as well as results for the prioritized component for the trivial invariant true, the boolean invariant (BI) or the linear invariant (LI). For boolean and linear invariants, we provide performance for both complete and basic implementations.

Notice that adding priority increases the number of "read" interactions executed in 60 seconds. This is due to the fact that a disk is unloaded only if no read is possible, that is only when unload is necessary to progress. Solutions obtained for the boolean invariant require more observation than the ones obtained for the linear invariant, therefore corresponding implementations are slower. More interesting, the best performance is obtained for basic solutions. In that particular case, fewer atomic components are observed which allows more parallelism in the composite component. This parallelism compensates the fact that the detection of false conflicts is not complete.

Related Work

Distributed resource 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] 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]. Solutions using managers typically rely on a conflict resolution protocol, such as a solution to the dining philosophers problem [START_REF] Chandy | The drinking philosophers problem[END_REF].

Similarly, implementation of priorities needs resolution of asymmetric conflicts. This can be achieved by direct observation as in [START_REF] Ben-Hafaiedh | Building distributed controllers for systems with priorities[END_REF] or [START_REF] Bonakdarpour | Automated distributed implementation of component-based models with priorities[END_REF] where managers observe higher priority interactions to ensure their disabledness. Knowledge is often used to drive action execution in distributed systems. Halpern and Moses [START_REF] Halpern | Knowledge and common knowledge in a distributed environment[END_REF] defined a logic to reason about the knowledge of system processes. Knowledge is used to control distributed discrete event systems [START_REF] Ricker | Know means no: Incorporating knowledge into discrete-event control systems[END_REF] and build distributed controllers for executing multiparty interactions with priorities [START_REF] Bensalem | Methods for knowledge based controlling of distributed systems[END_REF].

In most papers, computing knowledge requires exact computation of reachable states [START_REF] Ricker | Know means no: Incorporating knowledge into discrete-event control systems[END_REF][START_REF] Bensalem | Methods for knowledge based controlling of distributed systems[END_REF][START_REF] Halpern | Knowledge and common knowledge in a distributed environment[END_REF]. Our method overcomes this difficulty by using invariants which are over-approximations of the reachability set. Another common assumption is that the partial state observed by a manager is limited to a neighborhood determined by the architecture of the system [START_REF] Bensalem | Methods for knowledge based controlling of distributed systems[END_REF]. We propose a framework where observation can be adjusted for achieving a certain detection level.

Conclusion

Implementing multiparty interactions scheduled by using priorities requires efficient conflict resolution techniques. Most implementations do not distinguish between real and false conflicts to reduce overhead due to conflict resolution.

Dynamic knowledge-based computation of false conflicts based on invariants allows more efficient implementations. We provided simple criteria to define the correctness of the obtained implementation. Baseness ensures preservation of deadlock-freedom and completeness ensures equivalence with the fully-observed model. Finally, the proposed heuristics allow minimization of the number of components to observe and enhanced performance. Heuristics have been applied to non-trivial examples, where the optimal is known, and gave satisfactory results. These have been used for distributed implementation. Experiments show significant performance improvement. However, depending on the model, best performance is achieved either for basic or complete observation.

Future work includes several directions. First, we plan to study in depth how choices of detection levels affect performance of the obtained implementation. We can also consider intermediate levels between basic and complete observation. Such intermediate levels could, for instance, ensure complete detection of false conflicts for some interactions and avoid introduction of deadlocks for the others.

Another improvement is to use static analysis techniques in order to take into account parallelism. These techniques allow automatically computing a partition of the interactions that does not reduce the degree of parallelism by grouping possibly concurrent interactions. The allowed degree of parallelism can also be used to measure the utility of an additional observation, i.e. how observing an additional component can increase parallelism in the obtained implementation.

Algorithm 3

 3 Function alter for ensuring basic detection of false conflicts Input: A BIP component B, a partition of interactions γ = 1≤j≤m γj , a conflict relation # and a solution L = (L1, . . . , Lm), Output: A solution L ′ that is a neighbor of L. 1: L ′ :=L 2: choose k in 1, m and Bi in L ′ k \ support(γ k ) 3: L ′ k :=L ′ k \{Bi} //perturbation 4: while not basic(L ′ , {γ1, . . . , γm}) do 5: choose k in 1, m and Bi in {B1, . . . , Bn} \ L ′ k 6:

Fig. 3 .

 3 Fig. 3. Fragment of the dining philosopher component. Braces illustrates Partition 1.

  (at (P1.eating) + at (P0.eating) + at(P0.cleaning) + at (F1.f ree) = 1) (15)∧(at (P1.thinking) + at (P0.thinking) + at(F1.used) + at (P1.cleaning) = 2) (16)∧ (at (P2.eating) + at (P0.thinking) + at (F1.used) + at(P1.cleaning) + at (F2.f ree) = 1) (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)[START_REF] Chandy | The drinking philosophers problem[END_REF]

Fig. 5 .

 5 Fig. 5. Linear invariant for the Dining Philosophers example with N = 3.

Fig. 6 .Fig. 7 .

 67 Fig. 6. Performance for different detection levels, using Partition 1.

Fig. 9 .

 9 Fig. 8. Jukebox composite component.

  Intuitively, transitions → γ defined by rule [inter] express the behaviour 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 labelled 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 defined by transitions → πγ defined by rule[prio]. This rule restricts execution to interactions which are maximal with respect to the priority order. An enabled interaction a can execute only if no other one a ′ with higher priority is enabled.

				on
	π			off
	ack} off , req, upg, on, γ = {rb, rb π req rb π ack γ	off M rb upg	off up on up on M upg rb off M upg rb on M	M on M off M off on	dwn off S on S off S	req lst	S ack srv on S ack req
	Fig. 1. An example of BIP component. Initial state is (off, dwn).

Table 1 .

 1 Table1shows results of engine C 0 for Partition 1 and engine E 0 for Partition 2. The total Minimal observation for completeness.

	Eng. Comp./Part. Size true BI LI optimal
	C0 E0	Philo3 / 1 Philo4 / 1 Philo5 / 1 Philo10 / 1 Philo20 / 1 Philo100 / 1 200 197 197 108 6 3 3 1 8 5 5 2 10 7 7 3 20 17 17 8 40 37 37 18 Philo3 / 2 6 1 1 0 Philo4 / 2 8 3 3 1 Philo5 / 2 10 5 5 2 Philo10 / 2 20 15 15 7	1 2 3 8 18 98 0 1 2 7	Comp./Part. Size true BI LI Philo3 / 1 6 9 9 0 Philo4 / 1 8 20 20 4 Philo5 / 1 10 35 35 6 Philo10 / 1 20 170 170 23 Philo3 / 2 6 4 4 0 Philo4 / 2 8 6 6 1 Philo5 / 2 10 17 17 3 Philo10 / 2 20 75 75 14
		Philo20 / 2	40	35 35 18	17
		Philo100 / 2 200 195 195 106	97

Table 2 .

 2 Minimal observation for baseness.

Table 3 .

 3 Minimal observation cost to ensure baseness or completeness.

	Interaction true	BI(basic)	BI(complete) LI(basic) LI(complete)
	unload i,k 5 3(k = 1) or 5(k = 2)	5	2	2
	load i,k	1	0	1	0	1

⋆ The research leading to these results 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)