Joseph Sifakis

Saddek Bensalem

Simon Bliudze

Marius Bozga

A Theory Agenda for Component-Based Design

The aim of the paper is to present a theory agenda for component-based design based on results that motivated the development of the BIP component framework, to identify open problems and discuss further research directions. The focus is on proposing a semantically sound theoretical and general framework for modelling componentbased systems and their properties both behavioural and architectural as well for achieving correctness by using scalable specific techniques. We discuss the problem of composing components by proposing the concept of glue as a set of stateless composition operators defined by a certain type of operational semantics rules. We provide an overview of results about glue expressiveness and minimality. We show how interactions and associated transfer of data can be described by using connectors and in particular, how dynamic connectors can be defined as an extension of static connectors. We present two approaches for achieving correctness for component-based systems. One is by compositional inference of global properties of a composite component from properties of its constituents and interaction constraints implied by composition operators. The other is by using and composing architectures that enforce specific coordination properties. Finally, we discuss recent results on architecture specification by studying two types of logics: 1) interaction logics for the specification of sets of allowed interactions; 2) configuration logics for the characterisation of architecture styles.

Introduction

Component-based design is the process leading from given requirements and a set of predefined components to a system meeting the requirements.

Building systems from components is essential in any engineering discipline. Components are abstract building blocks encapsulating behaviour. They can be composed in order to build composite components. Their composition should be rigorously defined so that it is possible to infer the behaviour of composite components from the behaviour of their constituents as well as global properties from the properties of individual components.

The problem of building systems from components can be defined as follows. Given a set of components {C 1 , . . . , C n } and a property of their product state space Φ find a coordinator Co such that the coordinated behaviour Co(C 1 , . . . , C n ) meets the property Φ.

This problem can be studied as a synthesis problem [START_REF] Lustig | Synthesis from component libraries[END_REF]. The coordinator can be considered as a component that adequately restricts the behaviour of the components so that the resulting behaviour meets Φ. Synthesis techniques suffer from well-known complexity limitations. The coordinator is computed by (semi)-algorithms on the product space of the coordinated components.

System design pursues similar and even broader objectives than synthesis: incremental construction of systems meeting given requirements from a set of components. In contrast to synthesis, design lacks rigorous theoretical foundations. Existing frameworks are mostly informal. Designers use "ready-made" solutions to coordination problems, e.g. architectures, protocols, that have been proven correct practically or theoretically. In contrast to synthesis, design requires a variety of composition operators. It is based on the concept of architecture as a means to enforce specific characteristic properties by application of generic coordination principles. A key idea is to ensure correctness by construction by avoiding computationally expensive techniques implying state explosion.

Endowing component-based design with scientific foundations is a major scientific challenge. This requires:

1. A general concept of component. Currently there is no agreement on a single component model. System designers deal with heterogeneous components with different characteristics. One source of heterogeneity is the distinction between synchronous and asynchronous components. Hardware components as well as components in some data flow applications are synchronous. Another source of heterogeneity reflects the difference in programming styles. Thread-based programming allows for components to be accessed by an arbitrary number of threads sharing common data. It does not allow a strict separation between behaviour and coordination mechanisms as the programmer explicitly handles synchronisation primitives to ensure coherency of shared data, e.g. to avoid races. This style is hardly amenable to formalisation and analysis. On the contrary, actor-based programming assumes that each component has its own data transformed by a single local thread. Coordination is external to the atomic components of the application and can be ensured using general mechanisms such as protocols. 2. Theory for composing components. We need theory for describing and analysing the coordination between components in terms of tangible, well-founded and organised concepts. The theory should propose a set of composition operators meeting the following requirements:

-Orthogonality, meaning that composition operators are stateless to respect a clear separation between behaviour and coordination. Many component-based frameworks do not meet this requirement. Some allow arbitrary behaviour in coordination mechanisms. This which precludes rigorous mathematical treatment focusing on coordination. Others allow a limited number of types of behaviour such as buffers or queues to the detriment of mathematical elegance.

-Minimality, meaning that none of the coordination primitives can be expressed as the combination of others without using behaviour. -Expressiveness, meaning that the considered set of composition operators can be used to express any coordination problem. This requirement is further explained and formalised in the paper. Notice that most of the existing component composition frameworks fail to satisfy these requirements. Some are formal such as process algebras, e.g. CCS, CSP, π-calculus, and use single composition operators that are not expressive enough. Others are ad hoc such as most frameworks used in software engineering, e.g. architecture description languages [START_REF]Systems and software engineering -Architecture description[END_REF] which are not rooted in rigorous semantics and are hardly amenable to formalisation. 3. Theory for ensuring correctness of components. Being able to check or assert correctness of the built components using scalable techniques is an essential requirement. The idea is to avoid a posteriori verification and establish correctness incrementally by applying easy-to-check rules that follow the system construction.

A key concept in this approach is that of architectures as well-established coordination schemes enforcing given properties. The problem is then to decompose any component coordination property as the conjunction of predefined characteristic properties enforced by predefined architectures.

The aim of the paper is to propose a theory agenda for rigorous componentbased design. The agenda is built on existing results developed for the BIP framework [START_REF] Basu | Modeling heterogeneous real-time components in BIP[END_REF]. It identifies work directions addressing open problems and covering a good deal of the needs. The exposition of the results is mainly informal. We provide references to technical papers for the interested reader. One of the objectives is to show mathematical relations between three hierarchically structured domains encompassing the basic concepts:

-The domain of components offering the possibility of interaction through their ports p and associated variables X p through which they make available the data transferred when interactions occur. -The domain of connectors, used to model coordination between components.

Each connector is characterised by an interaction between ports and associated computation on the exported data. Interactions are arbitrary sets of ports. Their execution implies the atomic synchronisation of the involved components. Clearly if P is the set of the ports then the set of interactions I is a subset of 2 P . -The domain of configurations which are sets of connectors characterising architectures. Clearly if I is the set of interactions of an architecture then the set of configurations Γ is a subset of 2 I .

The paper is structured as follows. In Section 2, we discuss the problem of composing components by proposing the concept of glue. Glue is a set of stateless composition operators defined by a certain type of operational semantics rules. We provide an overview of results about expressiveness and minimality that led to the definition of the BIP component framework. In Section 3, we show how interactions and associated data transfer can be described by using connectors. We show in particular, how dynamic connectors can be defined as an extension of static connectors. Two approaches for achieving correctness for componentbased systems are presented in Section 4. One is by compositional inference of global properties of a composite component from properties of its constituents and synchronisation constraints implied by composition operators. The other is by using and composing architectures that enforce specific coordination properties. Section 5 discusses recent results on architecture specification by studying two types of logics: 1) interaction logics for the specification of sets of allowed interactions; 2) configuration logics for the characterisation of architectural styles. The last section concludes and discusses further research directions.

Composing Components

The Concept of Component

A component is a tuple C = (Σ, P, X, →), where -Σ is a set of control locations; -P is a set of ports; -X is a set of variables partitioned in two disjoint sets X L and X P of, respectively, local and port variables; the variables in X P are indexed by ports, that is

X P = {X p } p∈P ; -→ ⊆ Σ × P × G(X) × F (X) × Σ is a transition relation; transitions between
control locations are labeled by triplets (p, g, f ) where p is a port, g and f are, respectively, a guard Boolean expression and an update function on the variables in X.

A shorthand notation σ p,g,f ---→ σ is commonly used to denote (σ, p, g, f, σ ) ∈ →. Intuitively, a component can be considered as an open transition system, that is a system that performs coordination-driven computation. Coordination is defined by the environment of the component and involves two aspects: interaction (synchronisation) and data transfer. Denoting by X the set of all valuations of the variables in X, a state of the transition system is a pair s = (σ, v) where σ ∈ Σ is a control location and v ∈ X is a valuation of the component variables. Thus the state space of the transition system is S = Σ × X.

If σ p,g,f ---→ σ then the transition system has a transition from state s = (σ, v) to state s = (σ , v ) if g(v) = true and the external environment offers an interaction involving p. The execution of a transition consists in exporting the value v(X p ) of the variable X p3 associated with port p and receiving back a new value u p . The resulting valuation is v = f v[u p /X p ] where v[u p /X p ] is the valuation obtained by replacing, in v, the value of X p by u p .

Sometimes, for the sake of simplicity and when data treatment is irrelevant, we will use components without data, i.e. C = (Σ, P, →) with → ⊆ Σ × P × Σ. Notice that, since there are no data variables, X = X = ∅ and S = Σ, i.e. the notions of state and control location coincide. Therefore, in the rest of this section, we will use 's' to denote both.

The proposed concept of component does not distinguish between input and output ports. We consider that such a distinction is not specific to ports. It can be inferred from the data-flow relation between ports specified in the coordination mechanisms. Similarly, we do not distinguish between synchronous and asynchronous components. This distinction is also inferred from the context of use.

Glue Operators

The problem of component-based design can be understood as follows. Given a component framework and a property Φ, build a composite component C which satisfies Φ. A component framework comprises a set of components C, an equivalence relation ∼ = and a set G of glue operators on these components. The glue G includes general composition operators, i.e. behaviour transformers, such as parallel composition.

A general formalisation of the notions of component framework and glue is provided in [START_REF] Bliudze | Towards a theory of glue[END_REF]. Below, for the sake of simplicity, we assume that components are characterised by their behaviours specified directly as Labeled Transition Systems (LTS). In this context, a component framework can be considered as a term algebra equipped with an equivalence relation ∼ = compatible with strong bisimulation on transition systems. A composite component is any (well-formed) expression built from atomic components.

The meaning of a glue operator gl : C n → C can be specified by using a set of Structural Operational Semantics (SOS) rules [START_REF] Plotkin | A structural approach to operational semantics[END_REF], defining the transition relation of the composite component gl(C 1 , . . . , C n ) as a partial function of transition relations of the composed components C 1 , . . . , C n . A formal and general definition of glue operators on LTS components is provided in [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF]. Equation [START_REF] Allen | Specifying and analyzing dynamic software architectures[END_REF] shows a typical-although not general-form taken by SOS rules defining glue operators.

{s i pi -→ s i } i∈I {s j pj -→} j∈J {s i = s i } i ∈I s 1 . . . s n a -→ s 1 . . . s n . ( 1
)
Note 1. In the general case, as opposed to (1), several negative premises can apply to a single component. In any case, at most one positive premise can apply to a component.

The rule (1) has two parts: premises (above the line) and conclusion (below the line). Sets I, J ⊆ [1, n] (with I = ∅) index two subsets of components, which need not be disjoint: components {C i } i∈I contribute positive premises s i pi -→ s i , whereas components {C j } j∈J contribute negative premises s j pj -→.

The rule (1) is interpreted as follows. The state space Σ of the composite component is the Cartesian product of the state spaces of composed components: Σ = n i=1 Σ i . If 1) for each i ∈ I, component C i can execute a transition from the state s i to s i (with s i , s i ∈ Σ i ) labeled by the port p i ∈ P i and 2) for each j ∈ J, component C j cannot execute any transition from the state s j ∈ Σ j labeled by the port p j ∈ P j , then the composite component gl(C 1 , . . . , C n ) can execute a transition from the state s = s 1 . . . s n to s = s 1 . . . s n (with s, s ∈ Σ) labeled by an interaction a, where s i = s i , for all components that do not participate, i.e. C i with i ∈ I.

Notice that the negative premises play the role of priorities. A transition of the composite component can be executed only if a set of transitions of the constituent components are disabled.

An interaction a, in the conclusion of (1), corresponds to the atomic synchronous execution of transitions in the composed components. Depending on the component framework, the interaction label a is obtained by combining the ports {p i } i∈I in different manners.

Example 1. In CCS [START_REF] Milner | Communication and Concurrency[END_REF], ports are actions belonging to a given set L = A ∪ A ∪ {τ }, where actions in A = {a | a ∈ A} are complementary to those in A and τ ∈ A ∪ A is a special "silent" action. The binary parallel composition operator is defined by the following three rules:

s 1 p -→ s 1 s 1 s 2 p -→ s 1 s 2 , s 2 p -→ s 2 s 1 s 2 p -→ s 1 s 2 , for all p ∈ L , (2)
s 1 p -→ s 1 s 2 p -→ s 2 s 1 s 2 τ -→ s 1 s 2 , for all p ∈ A ∪ A (with p def = p). (3)
In the conclusion of the rule (3), the resulting interaction is the silent action τ , replacing the combination of two complementary actions p and p.

In [START_REF] Fares | Event algebra for transition systems composition -application to timed automata[END_REF], the authors propose a notion of label structures, providing a generic mechanism for defining interaction labels of the composite components. Below, for the sake of simplicity, we consider a in the conclusion of (1) to be the set of ports {p i } i∈I in the positive premises of the rule.

As shown above, positive premises in a rule of form (1) define interactions synchronising transitions of the constituent components. In a given global state of the system, several such interactions could be possible introducing nondeterminism in the composed behaviour. Negative premises define priority rules, which allow reducing this non-determinism.

Example 2. Consider the two components C 1 and C 2 shown in Figures 1a and1b. Let gl be a glue operator defined by the following three rules: Among the transitions labeled by q, only the transition 22 q -→ 32 is enabled and not 21 q -→ 31 (Figure 1c). Indeed, the negative premise in the third rule of (4) suppresses the interaction when a transition labeled r is possible in the second component. Here, this results in giving 21 qr -→ 32 "higher priority" over 21 q -→ 31. Notice that, in the state 22 of gl(C 1 , C 2 ), r is no longer possible, i.e. 2 r -→ in C 2 . Hence, the third rule of (4) applies and we have 22 q -→ 32.

s 1 p -→ s 1 s 1 s 2 p -→ s 1 s 2 , s 1 q -→ s 1 s 2 r -→ s 2 s 1 s 2 qr -→ s 1 s 2 , s 1 q -→ s 1 s 2 r -→ s 1 s 2 q -→ s 1 s 2 . ( 4
) C 1 p q 1 2 3 (a) C 2 r 1 2 (b) gl(C 1 , C 2 )
Priorities are presented in more detail in Section 2.5, below.

Properties of Glue

Glue operators must meet the following requirements.

Incrementality. If a composite component is of the form gl(C 1 , C 2 , . . . , C n ) for n ≥ 2, then there exist glue operators gl 1 and gl 2 such that

gl(C 1 , C 2 , . . . , C n ) ∼ = gl 1 C 1 , gl 2 (C 2 , . . . , C n ) .
Incrementality is a kind of generalised associativity 4 . It requires that coordination between n components can be expressed by first coordinating n -1 com- 4 Notice that, for any permutation σ : [1, n] → [1, n], one can define a glue operator glσ(C1, . . . , C2) def = gl C σ(1) , . . . , C σ(n) . Applying incrementality to glσ with the permutation σ = (2, 3, . . . , i, 1, i + 1, . . . , n), we conclude that there must exist glue operators gl1 and gl2 such that gl(C1, . . . , Ci, . . . Cn) = glσ(Ci, C1, . . . , Ci-1, Ci+1, . . . , Cn) = gl1 Ci, gl2(C1, . . . , Ci-1, Ci+1, . . . , Cn) , for any

i ∈ [1, n].
ponents and then by coordinating the resulting component with the remaining argument.

Flattening. Conversely, G must be closed under composition, i.e. if a composite component is of the form gl 1 (C 1 , gl 2 (C 2 , . . . , C n )) then there exists an operator gl such that

gl 1 C 1 , gl 2 (C 2 , . . . , C n ) ∼ = gl(C 1 , C 2 , . . . , C n ) .
This property is essential for separating behaviour from glue and treating glue as an independent entity that can be studied and analysed separately. Flattening enables model transformations, e.g. for optimising code generation or component placement on multicore platforms [START_REF] Bonakdarpour | From high-level component-based models to distributed implementations[END_REF][START_REF] Bozga | Source-to-source architecture transformation for performance optimization in BIP[END_REF].

Compositionality. The equivalence relation ∼ = must be a congruence with respect to the glue operators. For all gl ∈ G, all C, C 1 , . . . , C n ∈ C and i ∈ [1, n],

C i ∼ = C must imply gl(C 1 , . . . , C i , . . . , C n ) ∼ = gl(C 1 , . . . C, . . . , C n ) .
Compositionality is fundamental for reasoning about systems. It allows considering properties of components in isolation and separately from the properties of glue operators to infer global properties of the system by construction. Furthermore, compositionality allows component providers to protect their intellectual assets by providing only an abstract specification of a component-any observationally equivalent implementation can then be substituted without affecting the semantics of the system.

It can be shown that glue operators defined by SOS rules, as in [START_REF] Allen | Specifying and analyzing dynamic software architectures[END_REF], are always compositional if the equivalence relation ∼ = is compatible with strong bisimulation (recall the assumption of Section 2.2).

It should be noted that almost all existing frameworks fail to meet all three requirements. Process algebras are based on two composition operators (some form of parallel composition and hiding) which are orthogonal to behaviour, but fail to meet the flattening requirement as formulated above: in order to flatten a composite component, the operand components might have to be modified or additional components (e.g. context) might need to be introduced. General component frameworks, such as [START_REF] Arbab | Reo: a channel-based coordination model for component composition[END_REF][START_REF] Eker | Taming heterogeneity-The Ptolemy approach[END_REF], adopt more expressive notions of composition by allowing the use of behaviour for coordination between components and thus do not separate behaviour from interaction. Furthermore, most of these frameworks are hardly amenable to formalisation through operational semantics.

Expressiveness of Glue

Comparison between different formalisms and models is often made disregarding their structure and reducing them to behaviourally equivalent formalisms, such as Turing machine. This leads to a notion of expressiveness which is not adequate for the comparison of high-level languages. All programming languages are deemed equivalent (Turing-complete) disregarding their adequacy for solving problems. For component frameworks separation between behaviour and coordination mechanisms is essential.

A notion of expressiveness for component frameworks characterising their ability to coordinate components is proposed in [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF]. It allows the comparison of two component frameworks with glues G and G respectively, the same set of components and equipped with the same congruence relation ∼ =.

We say that G is more expressive than G-denoted G G -if, for any composite component gl(C 1 , . . . , C n ) obtained by using gl ∈ G, there exists

gl ∈ G , such that gl(C 1 , . . . , C n ) ∼ = gl (C 1 , . . . , C n ).
That is, any coordination expressed by using G can be expressed by using G .

Example 3. Let P be a set of ports and consider two glues Bin and T er generated respectively by families of binary and ternary rendezvous operators: rdv

(2)
a,b and rdv

(3)
a,b,c , defined by the following rules (for all interactions a, b, c ∈ 2 P ):

rdv (2)
a,b :

s 1 a -→ s 1 s 2 b - → s 2 s 1 s 2 ab -→ s 1 s 2 , rdv (3)
a,b,c :

s 1 a -→ s 1 s 2 b - → s 2 s 3 c - → s 3 s 1 s 2 s 3 abc --→ s 1 s 2 s 3 .
(5) Clearly, T er Bin. Indeed, for any a, b, c ∈ 2 P , and any

C 1 , C 2 , C 3 ∈ C, we have rdv (3) a,b,c (C 1 , C 2 , C 3 ) ∼ = rdv (2) a,bc C 1 , rdv (2)
b,c (C 2 , C 3 ) . On the contrary, Bin T er, since any two components at any given state can only perform two actions (one action each), whereas three are needed for a ternary synchronisation.

We call universal glue the set G univ , which contains all glue operators that can be defined by the rules similar to (1) in the general form defined in [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF] (see also Note 1). An interesting question is whether the expressiveness of G univ can be achieved with a minimal set of operators. Results in [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF] bring a positive answer to this question. It is shown that the glue of the BIP framework [START_REF] Basu | Modeling heterogeneous real-time components in BIP[END_REF] combining two classes of operators, interactions and priorities, is as expressive as G univ . Furthermore, this glue is minimal in the sense that it loses universal expressiveness if either interactions or priorities are removed.

A consequence of these results is that most existing formal frameworks using only interaction such as process algebras are less expressive. This comparison can be strengthened by using the following weaker notion of expressiveness.

Often component frameworks consider certain behaviours, such as, for instance, FIFO buffers, to be part of the coordination primitives. To address such cases, we introduce a weaker form of expressiveness comparison. We say that G is weakly more expressive than G-denoted G W G -if there exists a finite set of coordinating components D ⊆ C, such that, for any component

gl(C 1 , . . . , C n ) with gl ∈ G there exist gl ∈ G and D 1 , . . . , D k ∈ D, such that gl(C 1 , . . . , C n ) ∼ = gl (C 1 , . . . , C n , D 1 , . . . , D k ).
That is, to realise the same coordination as gl, additional behaviour is needed. The term "weakly more expressive" is justified by the observation that, taking Considering τ as the "silent" action, it is easy to see that, for all a, b ∈ 2 P and

D = ∅, G G clearly implies G W G .
C 1 , C 2 ∈ C, we have rdv (2) a,b (C 1 , C 2 ) ∼ = rdv (3) τ,a,b (D, C 1 , C 2 )
. Therefore, we say that Bin and T er are weakly equivalent.

It can be shown that glues including only interactions fail to match universal expressiveness even under this definition. Adding new atomic components does not suffice if the behaviour of the composed components is not modified.

Relations between the glues of BIP (see Section 2.5 below) and classical process algebras, namely CCS [START_REF] Milner | Communication and Concurrency[END_REF], SCCS [START_REF] Milner | Calculi for synchrony and asynchrony[END_REF] and CSP [START_REF] Hoare | Communicating Sequential Processes[END_REF], which were obtained in [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF], are summarised in Figure 2. BI denotes the BIP glue without priorities.

The BIP Component Model

In the light of the above results the BIP component model has been defined in [START_REF] Basu | Modeling heterogeneous real-time components in BIP[END_REF][START_REF] Bliudze | The algebra of connectors -Structuring interaction in BIP[END_REF]. BIP uses two types of glue. Given a set of atomic components C 1 , . . . , C n a composite component is modelled by an expression of the form πγ(C 1 , . . . , C n ) where γ is a set of interactions and π a priority relation.

Let

C i = (Σ i , P i , - →), for i ∈ [1, n],
with disjoint sets of ports, i.e. P i ∩ P j = ∅, for i = j and denote P = n i=1 P i . The glue operator corresponding to a set of interactions γ ⊆ 2 P is defined by the following set of rules in the format generalising (1) (see Note 1):

s i a∩Pi ---→ s i i∈I s i = s i i ∈I s 1 . . . s n a -→ s 1 . . . s n , for all a ∈ γ , (6)
where

I = {i ∈ [1, n] | a ∩ P i = ∅}
is the set indexing the components that participate in the interaction. Notice that (6) has only positive premises. Priority is a strict partial order relation π ⊆ 2 P × 2 P . For two interactions a, b ∈ 2 P , we write a ≺ b as a shorthand for (a, b) ∈ π. As described in Section 2.2, priority introduces negative premises in the derivation rules. Intuitively, for an interaction a to be executed, it has to be enabled (cf. ( 6)) and all interactions with higher priority than a must be disabled.

For an interaction a ∈ 2 P , denote by π(a) = b ∈ 2 P a ≺ b the set of interactions having higher priority than a. For an interaction b ∈ π(a) to be disabled, a corresponding transition must be disabled in at least one of the contributing components. To assign such a component to each b ∈ π(a) we use, in the derivation rules [START_REF] Bensalem | Incremental generation of linear invariants for component-based systems[END_REF] below, indexing functions j : π(a) → [1, n], such that, for all b ∈ π(a), we have b ∩ P j(b) = ∅. Thus the glue operator πγ is defined by the following set of rules:

s i a∩Pi ---→ s i i∈I s j(b) b∩P j(b) -----→ b∈π(a) s i = s i i ∈I s 1 . . . s n a -→ s 1 . . . s n ,
for all a ∈ γ and j :

π(a) → [1, n] such that ∀b ∈ π(a), b ∩ P j(b) = ∅ , (7)
where

I = {i ∈ [1, n] | a ∩ P i = ∅}
is the set indexing the components that participate in the interaction a. In [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF], we have shown that any operator of the universal glue G univ can be obtained in such manner by combining a priority π and a set of interactions γ.

Besides meeting the universal expressiveness property, BIP meets the incrementality, flattening and compositionality requirements discussed in Section 2.3 (see the detailed discussion in [START_REF] Baranov | Offer semantics: Achieving compositionality, flattening and full expressiveness for the glue operators in BIP[END_REF]). Glue is a first class entity that can be analysed and composed.

The BIP model is implemented by the BIP language and an extensible toolbox. The BIP language can be considered as a general component coordination language. It leverages on C++ style variables and data type declarations, expressions and statements, and provides additional structural syntactic constructs for defining component behaviour, describing connectors and priorities. Moreover, it provides constructs for dealing with parametric and hierarchical descriptions as well as for expressing timing constraints associated with behaviour. The BIP toolbox includes tools for checking correctness, for source-to-source transformations and for code generation. Correctness can be either formally proven using invariants and abstractions, or tested by using simulation. For the latter case, simulation is driven by a specific middleware, the BIP engine, which allows exploration and inspection of traces corresponding to BIP models. Source-to-source transformations allow static optimizations as well as specific transformations towards implementation, i.e. distribution. Finally, code generation targets different platforms and operating systems support (e.g. distributed, multi-threaded, realtime, for single/multi-core platforms).

In the rest of the paper, we focus on modelling interactions by using connectors as well as the formalisation of architectures and their use for achieving correctness by construction.

Connectors and Their Properties

In this section we study connectors as a means for expressing coordination constraints between components. Connector descriptions involve a control part describing interactions and a data transfer part describing data transformations of the interacting components. We provide a principle for the hierarchical structuring of connectors and show how hierarchical connectors can be flattened into equivalent simple connectors. Finally, we propose a formalism for describing dynamic connectors that is currently under study.

Simple Connectors

We consider a set of components {C i } i∈I with disjoint sets of ports {P i } i∈I . We denote for a set of ports P by X P the associated set of variables. A connector γ is an expression of the form γ = (a). g(X a ) :

X a := f (X a ) ,
where a is an interaction, that is a set of ports such that |a ∩ P i | ≤ 1 for all i ∈ I.

The interaction describes the control part of the connector. It is an n-ary atomic strong synchronisation between ports specified by the set of the synchronised ports. The term in brackets consists of a guard on the exported variables followed by an assignment. It describes the data transfer part of the connector. The execution of a connector is possible only if ports involved in the interaction a are enabled in the components and the guard g evaluates to true for the exported values. It consists in modifying the exported variables as specified by the assignment and letting the involved components complete the synchronised transitions.

The figure below depicts a connector between ports p, q and r with associated exported variables X p , X q and X r . An interaction can occur only when at least two of the exported values differ (the guard is true). It is completed by assigning the maximum of their values to the port variables. p X p q X q r X r (pqr). (X p = X q ) ∨ (X p = X r ) : X p , X q , X r := max(X p , X q , X r ) Fig. 3: Simple connector

The effect of the application of connectors on a set of components is formally defined in [START_REF] Bliudze | Architecture internalisation in BIP[END_REF].

Hierarchical Connectors

Hierarchical connectors are useful when we want to build systems incrementally. The idea is to equip each connector with a port and an associated variable. The port can be then used further in other connectors, and hence lead to a hierarchical structuring of connectors. Syntactically, a hierarchical connector γ is an expression of the form

γ = (w ← a). g(X a ) : (X w , X L ) := f up (X a ) // X a := f down (X w , X L ) .
As for simple connectors, the coordination in hierarchical connectors involves two parts. The control part w ← a defines a dependency relation between the connector port w and its interaction a. That is, w is enabled if and only if the interaction a is enabled. The data part g(X a ) : (X w , X L ) := f up (X a ) // X a := f down (X w , X L ) defines the computation realised on local variables X L and data associated to ports. The interaction is enabled and the computation is performed only if the guard g(X a ) evaluates to true. In this case, computation involves two steps. First, an up function f up is used to compute X w and X L depending on interaction variables X a . Second, if an (upper) interaction involving w takes place, the down function f down is used to update X a based on X w and X L . Moreover, in an hierarchical connector, execution of up and down steps is coordinated: first, all up steps are performed bottom-up (as long as guards are satisfied), then, if a top-level interaction is executed, all down steps are performed top-down.

As an example, the coordination enforced by the simple connector presented in Figure 3 can be equally obtained by using the hierarchical connector depicted in Figure 4. The ternary connector and its associated data transfer is split in two binary connectors, glued together by the port w.

p X p q X q r X r u X u w X w , Y w (w ← pq).
[true : X w := max(X p , X q ), Y w := (X p = X q ) // X p , X q := X w ] (u ← wr).[Y w ∨ (X w = X r ) : X u := max(X w , X r ) // X w , X r := X u ] Fig. 4: Hierarchical connector Hierarchical connectors can be statically flattened, that is, transformed into functionally equivalent simple connectors. For the control part, flattening amounts to substituting the inner connector ports by the associated interactions. For the data part, it reduces to static composition of up and down functions together with propagation of the guards. Flattening has been formally defined as a rewriting system on hierarchical connectors and proven confluent and terminating [START_REF] Bliudze | Architecture internalisation in BIP[END_REF]. As an example, flattening of the connector from Figure 4 transforms it back into the simple connector from Figure 3.

Dynamic Connectors

How can we reason about architectures whose structure changes dynamically? There exists a variety of paradigms dealing with dynamic change in coordination. One is based on the use of process algebras such as the π-calculus [START_REF] Milner | Communicating and Mobile Systems: The π-calculus[END_REF].

Nonetheless, there is no clear distinction between behaviour and coordination and thus it is hard to come up with a concept of architecture in this context.

Another considers architectures as graphs and studies their possible configurations by using graph grammars. Technically architecture styles and possible configurations are described by context-free graph grammars [START_REF] Metayer | Describing software architecture styles using graph grammars[END_REF][START_REF] Papadopoulos | Configuration and dynamic reconfiguration of components using the coordination paradigm[END_REF]. This approach implicitly assumes the existence of a global coordinator. Furthermore, the focus is on changing structure and it is not easy to account for data transfer. Other more ad hoc techniques consider that dynamic architectures are just coordinators between components that can modify the architecture connectivity [START_REF] Allen | Specifying and analyzing dynamic software architectures[END_REF]. The approach closest to the one presented below is explored in [START_REF] Bruni | Behaviour, interaction and dynamics[END_REF], where dynamic BI(P) (BIP without priorities) allows spawning new components and interactions during execution.

We show below how dynamic connectors can be defined as a direct extension of connectors in BIP. We assume that system models are built using arbitrary numbers of typed components. The type T of a component defines its set of ports and associated exported variables. Two kinds of variables can be used in descriptions: 1) component variables c i with an associated component type T , denoted c i : T ; 2) variables U i representing sets of components of the same type T , denoted U i : T . We denote by c.p the port p of component c.

A connector description consists of a set of initialisation statements followed by a set of rules. The initialisation statements define initial values of the variables U representing sets of components. The rules define sets of dynamic connectors. The format for the description is the same as for static connectors. The main difference is that the rules may involve guards and computation that modifies the sets of components.

The following example models a ring architecture composed of n elements

U := {c i : T, for 0 ≤ i < n} , (8)
r i := (c i .out, c (i+1)%n .in).[true : X c (i+1)%n .in := X ci.out ], for 0 ≤ i < n . (9)
Line ( 8) initialises a variable U with an array of component instances by using the iterator primitive for 0 ≤ i < n. Line [START_REF] Bensalem | D-Finder: A tool for compositional deadlock detection and verification[END_REF] gives a set of n rules for specifying connectors transferring data from outputs to inputs.

The following example models a set of n components that must strongly synchronise through their port p, with the possibility of disconnecting a component when it detects a failure and the possibility to rejoin the group in case of recovery. The first line creates an array of n instances of components c of type T . The description uses two variables U and U act representing sets of components. The former is used to record the universe of the created components and the latter to record the set of the active components.

The configurations are described by three rules. Rule [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF] involves an interaction requiring the synchronisation of all the active components. The corresponding computation consists in assigning to the synchronised port variables the maximum of the exported values. Rule [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF] describes disconnection of the i-th component c i when it detects a failure. Rule [START_REF] Bensalem | Efficient deadlock detection for concurrent systems[END_REF] describes insertion of a component after recovery.

U := {c i : T, for 0 ≤ i < n} , U act := U , r := (c.p, for c ∈ U act ). true :

x c.p := max{x c.p | c ∈ U act }, for c ∈ U act , (10)
r f ail c := (c.f ail).[true : U act := U act -c], for c ∈ U act , (11)
r join c := (c.join).[true : U act := U act + c], for c ∈ U \ U act . ( 12
)
As a final illustration, consider the Master-Slave example presented in [START_REF] Bozga | Modeling dynamic architectures using Dy-BIP[END_REF]. Systems are constructed from two types of components, respectively masters (M ) and slaves (S). Every master m i requests sequentially two distinct slaves s j , s k (rules 13, 14) and then interacts with both of them (rule 15 above). The rules are graphically depicted in Figure 5.

U := {m i : M, s j : S, for 0 ≤ i < n, 0 ≤ j < m} , req 1 ij := (m i .req s j .get)[x mi.req = ∅ : x mi.req := x mi.req ∪ s j ], ( 13
)
for 0 ≤ i < n, 0 ≤ j < m req 2 ik := (m i .req s k .get)[s k ∈ x mi.req : x mi.req := x mi.req ∪ s k ], (14)
for 0 ≤ i < n, 0 ≤ k < m comp ijk := (m i .comp s j .work s k .work)[s j , s k ∈ x mi.req : x mi.req := ∅], (15)
for 0 ≤ i < n, 0 ≤ j, k < m

Achieving Correctness

We present two approaches for achieving correctness for component-based systems. The first is by compositional inference of global properties of a composite component from properties of its constituents and synchronisation constraints implied by composition operators. The second is by using and composing architectures that enforce specific coordination properties.

Compositional Verification

Compositional verification techniques are used to cope with state explosion in concurrent systems. The idea is to apply divide-and-conquer approaches to infer global properties of complex systems from properties of their components. Separate verification of components limits state explosion. Nonetheless, components mutually interact in a system and their behaviour and properties are inter-related. This is a major difficulty in designing compositional techniques.

We developed for BIP a compositional verification method [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF][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] for safety properties (invariants) based on the following rule:

C i |= Φ i i Ψ ∈ II γ, (C i ) i Φ i ∧ Ψ ⇒ Φ γ((C i ) i ) |= Φ . ( 16
) ψ φ2 φ1
Fig. 6: Rule illustrated This rule allows one to prove invariance of Φ for systems γ((C i ) i ) constructed by using a parallel composition operation parameterised by a set of connectors γ on a set of components (C i ) i . It relies on computing auxiliary invariants as the conjunction of component invariants Φ i and an interaction invariant Ψ . Component invariants Φ i are computed locally for components C i , hence, they satisfy C i |= Φ i , for all is. Interaction invariants Ψ expresses constraints on the global state space induced by interactions between components. They are obtained automatically from finitestate abstractions of the system to be verified and without explicitely constructing the product space, that is, denoted by Ψ ∈ II γ, (C i ) i . Finally, if the implication i Φ i ∧Ψ ⇒ Φ holds, i.e. can be effectively proven by using a SAT/SMT solver, then Φ is an invariant of the composed system.

The principle of the rule is graphically illustrated in Figure 6 for two components C 1 , C 2 assuming that each dimension corresponds to the state space of each component. Component invariants define restrictions represented as a vertical and a horizontal strip. The intersection of component invariants is a rectangular area including all the states of the Cartesian product of the sets of states meeting each invariant. The restriction induced by interaction invariants is an oblique strip that removes states of the rectangular area that are forbidden by the interactions.

As a concrete illustration, let us consider a simple benchmark example from [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF]. The Temperature Control System models the control of the coolant temperature in a reactor tank by moving two independent refrigerating rods. The goal is to maintain the coolant between the temperatures θ m = 100 • C and θ M = 1000 • C. When the temperature reaches its maximum value θ M , the tank must be refrigerated with one of the rods. The temperature rises at a rate v r = 1 • C/s and decreases at rate v d = 2 • C/s. A rod can be moved again only if T = 3600s has elapsed since the end of its previous movement. If the temperature of the coolant cannot decrease because there is no available rod, a complete shutdown is required. A discretised time model of the Temperature Control System in BIP is provided in Figure 7. The model consists of three atomic components, a Controller handling the temperature and two components Rod 1 , Rod 2 modelling the rods. The variable θ within the Controller stores the temperature of the reactor. Its evolution depends on the state respectively, at l 5 (heating) it increases by one every time unit and at l 6 (cooling) it decreases by 2 every time unit. The transitions between states depend on the value of θ, as explained earlier. The Rod 1,2 components are identical. The t 1,2 variables are discrete clocks measuring the resting time. They increase by one every time unit. A rod can be used for cooling only when the resting time is greater than 3600. The Controller and the Rods are interconnected by five connectors (tick tick 1 tick 2 ), (cool cool 1 ), (cool cool 2 ), (heat rest 1 ), (heat rest 2 ) modelling respectively, the discrete time progress and the usage/releasing of the rods. In the BIP model, complete shutdown corresponds to a deadlock situation, henceforth, checking for functional correctness amounts to checking deadlock-freedom. The invariants computed on Φ Controller = (at l 5 ∧ 100 ≤ θ ≤ 1000) ∨ (at l 6 ∧ 100 ≤ θ ≤ 1000)

θ := θ + 1 cool θ > 100 θ := θ -2 θ = 1000 t 1 := t 1 + 1 tick 1 tick 1 cool 1 t 1 := 0 rest 1 l1 l2
Φ Rod1 = (at l 1 ∧ t 1 ≥ 0) ∨ (at l 2 ∧ t 1 ≥ 3600) Φ Rod2 = (at l 3 ∧ t 2 ≥ 0) ∨ (at l 4 ∧ t 2 ≥ 3600) Ψ = (at l 2 ∨ at l 4 ∨ at l 5 ) ∧ (at l 1 ∨ at l 3 ∨ at l 6 )
As explained in [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF], deadlock-freedom of BIP models can be characterised as an invariant state property. For our example, potential deadlocks states include, e.g.

D 1 = (at l 1 ∧ t 1 < 3600) ∧ (at l 3 ∧ t 2 < 3600) ∧ (at l 6 ∧ θ = 100) D 2 = (at l 1 ∧ t 1 < 3600) ∧ (at l 3 ∧ t 2 < 3600) ∧ (at l 5 ∧ θ = 1000)
Proving deadlock-freedom amounts to checking that no states within D 1 or D 2 are reachable, or equivalently, that both Φ 1 = ¬D 1 and Φ 2 = ¬D 2 are invariants.

Using a SAT solver it can be checked that the following assertion holds

(Φ Controller ∧ Φ Rod1 ∧ Φ Rod2 ∧ Ψ ) ⇒ Φ 1
therefore Φ 1 is a system invariant and all deadlock states within D 1 are unreachable. But, the implication above does not hold when Φ 2 is considered instead of Φ 1 . This means that Φ 2 cannot be proven invariant and hence deadlock states in D 2 are potentially reachable. In this case, complementary verification techniques, e.g. backward reachability analysis, can be used to confirm/infirm their reachability in the model. Table 1 taken from [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF] provides an overview of experimental results obtained for several benchmarks. For the columns: n is the number of BIP components in the example, q is the total number of control locations, x is the total number of boolean and integer variables, D provides, when possible, the estimated number of deadlock configurations, D c (resp. D ci ) is the number of deadlock configurations remaining once component respectively interaction invariants are used and t is the total time for computing invariants and checking for satisfiability. The original method from [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF] has been extended in several directions. Incremental extensions, where invariants and properties are established along the model construction, have been studied in [START_REF] Bensalem | Incremental component-based construction and verification using invariants[END_REF][START_REF] Bensalem | Incremental generation of linear invariants for component-based systems[END_REF]. Moreover, it has been combined with backward reachability analysis and automatic strengthening of invariants for elimination of false positives [START_REF] Bensalem | Efficient deadlock detection for concurrent systems[END_REF]. More recently, the method has been extended to timed models and timed properties [START_REF] Astefanoaei | Compositional invariant generation for timed systems[END_REF].

Property Enforcement-Architectures

Property enforcement consists in applying architectures to restrict the behaviour of a set of components so that the resulting behaviour meets a given property. Depending on the expressiveness of the glue operators, it may be necessary to use additional components to achieve a coordination to satisfy the property.

Architectures depict design principles, paradigms that can be understood by all, allow thinking on a higher plane and avoiding low-level mistakes. They are a means for ensuring global properties characterising the coordination between components-correctness for free. Using architectures is key to ensuring trustworthiness and optimisation in networks, OS, middleware, HW devices etc.

System developers extensively use libraries of reference architectures ensuring both functional and non-functional properties, for example fault-tolerant architectures, architectures for resource management and QoS control, time-triggered architectures, security architectures and adaptive architectures. The proposed definition is general and can be applied not only to hardware or software architectures but also to protocols, distributed algorithms, schedulers, etc.

An architecture is a partial operator A : C n → C, imposing a characteristic property Φ and defined by a glue operator gl and a set of coordinating components D, such that: An architecture is a solution to a coordination problem specified by Φ, using a particular set of interactions specified by gl. It is a partial operator, since the interactions of gl should match actions of the composed components.

Application and platform restrictions entail reduced expressiveness of the glue operator gl that must be compensated by using the additional set of components D for coordination. For instance, glue operators defined by connectors (cf. Sections 3.1-3.3) are memoryless. Hence, they can only be used to impose state properties. Imposing more complex safety properties requires additional coordination behaviour. Similarly, for distributed architectures, interactions are point-to-point by asynchronous message passing. Synchronisation among the components is achieved by stateful protocols.

The characteristic property assigns a meaning to the architecture that can be informally understood without the need for explicit formalisation (e.g. mutual exclusion, scheduling policy, clock synchronisation).

In addition to imposing the characteristic property, an architecture must preserve essential properties of the composed components. In particular, any invariant of a component C i must be an invariant of A[C 1 , . . . , C n ]. In Section 4.3, we provide results about preservation of safety and liveness properties by architecture composition. Since there exists a unary identity architecture, which does not modify the behaviour of its operand, preservation of properties by architectures follows from that by architecture composition.

Architectures should, in principle, preserve deadlock-freedom: if components C i are deadlock-free then A[C 1 , . . . , C n ] should be deadlock-free too. However, in general, preservation of deadlock-freedom cannot be guaranteed by construction, since architectures restrict the behaviour of components they are applied to. Instead, deadlock-freedom has to be verified a posteriori using techniques such as the one presented in Section 4.1.

Property Composability

In a design process it is often necessary to combine more than one architectural solution on a set of components to achieve a global property. System engineers use libraries of solutions to specific problems and they need methods for combining them without jeopardising their characteristic properties.

For example, a fault-tolerant architecture combines a set of features building protections against trustworthiness violations. These include 1) triple modular redundancy mechanisms ensuring continuous operation in case of single component failure; 2) hardware checks to be sure that programs use data only in their defined regions of memory, so that there is no possibility of interference; 3) default to least privilege (least sharing) to enforce file protection. Is it possible to obtain a single fault-tolerant architecture consistently combining these features? The key issue here is feature interaction in the integrated solution. Noninteraction of features is characterised below as property composability based on our concept of architecture.

Consider two architectures A 1 , A 2 , enforcing respectively properties Φ 1 , Φ 2 on components C 1 , . . . , C n . That is, A 1 [C 1 , . . . , C n ] and A 2 [C 1 , . . . , C n ] satisfy respectively the properties Φ 1 , Φ 2 . Is it possible to find an architecture A[C 1 , . . . , C n ] that meets both properties? For instance, if A 1 ensures mutual exclusion and A 2 enforces a scheduling policy is it possible to find architectures on the same set of components that satisfies both properties?

A full, rigorous definition of the notions of architecture and property enforcement is provided in [START_REF] Attie | General framework for architecture composability[END_REF] alongside a constructive definition of an associative, commutative and idempotent architecture composition operator ⊕. An architecture is defined as a triple A = (D, P A , γ), where D is a finite set of coordinating components, P A is a set of ports and γ ⊆ 2 P A is an interaction model over P A . Noticing that the interaction model γ can be represented by the corresponding characteristic predicate ϕ γ on variables in P A , the composition of two architectures A 1 = (D 1 , P A1 , γ 1 ) and A 2 = (D 2 , P A2 , γ 2 ) is defined by putting

A 1 ⊕ A 2 def = (D 1 ∪ D 2 , P A1 ∪ P A2 , γ) where γ is such that ϕ γ = ϕ γ1 ∧ ϕ γ2 .
The properties of ⊕ are studied and applied for building correct-by-construction components incrementally. In particular ⊕ has a neutral element A id , which is the most liberal architecture enforcing no coordination constraints.

When applying an architecture A to enforce a property Φ on components C 1 , . . . , C n , the property Φ is expressed in terms of the states of C 1 , . . . , C n . The states of the coordinating components D (see Section 4.2) are irrelevant. Therefore, we say that an architecture A enforces a property Φ on components C 1 , . . . , C n if the projection of every trace of A[C 1 , . . . , C n ] onto the state space of A id [C 1 , . . . , C n ] satisfies Φ. In [START_REF] Attie | General framework for architecture composability[END_REF], we show that if two architectures A 1 and A 2 enforce the respective safety properties Φ 1 and Φ 2 on components C 1 , . . . , C n , then A 1 ⊕ A 2 enforces on these components the conjunction Φ 1 ∧ Φ 2 of the two properties.

γ 12 = {b 1 b 12 , b 2 b 12 , f 1 f 12 , f 2 f 12 } (see Section 2.5).
Assuming that the initial states of C 1 and C 2 are sleep, and that of D 12 is free, neither of the two states (free, work, work) and (taken, work, work) is reachable, i.e. the mutual exclusion property

Φ 12 holds in A 12 [C 1 , C 2 ].
Let C 3 be a third component, similar to C 1 and C 2 , with the set of ports {b 3 , f 3 }. We define two additional architectures A 13 and A 23 similar to A 12 : they consist, respectively, of coordinating components D 13 and D 23 , which, up to the renaming of ports, are the same as D 12 in Figure 8b, One can define a canonical lattice on the set of architectures. The lattice is induced by the partial order relation <, defined by putting A 1 < A 2 if and only if A 1 ⊕ A 2 ∼ = A 1 . The neutral architecture A id is the top element of the lattice; the bottom element is the "blocking" architecture, inhibiting all actions of the components, thus leading to a global deadlock. 5 The composition A 1 ⊕ A 2 is then the greatest lower bound of A 1 and A 2 with respect to <. It represents the most liberal architecture enforcing both Φ 1 and Φ 2 .

γ 13 = {b 1 b 13 , b 3 b 13 , f 1 f 13 , f 3 f 13 } and γ 23 = {b 2 b 23 , b 3 b 23 , f 2 f 23 , f 3 f 23 }.
In the above setting, interfering features of a system are translated as contradictory properties. For example, the following two features can be required from an elevator cabin [START_REF] Souza | Conflict-tolerant features[END_REF][START_REF] Plath | Feature integration using a feature construct[END_REF]:

1. If the elevator is full, it must stop only at floors selected from the cabin and ignore outside calls. 2. Requests from the second floor have priority over all other requests.

Clearly these two requirements are contradictory, since they cannot be jointly satisfied when the elevator is called from the second floor while it is full. Applying the composition of two architectures enforcing respectively these two properties on the components forming the elevator cabin would generate deadlocks.

Thus, although architecture composition ⊕ preserves safety properties, it does not preserve deadlock-freedom. Deadlock-freedom can be compositionally verified by techniques such as the one presented in Section 4.1.

The treatment of liveness properties is based on the idea that each coordinator must be "invoked sufficiently often" for the corresponding liveness properties to be imposed on the system as a whole. For each coordinator, one designates the set of its "idle states". It is then required that each coordinator be executed infinitely often, unless, from some point on, it remains forever in an idle state [START_REF] Attie | General framework for architecture composability[END_REF]. In [START_REF] Attie | General framework for architecture composability[END_REF], it is shown that this notion of liveness is preserved by the composition of architectures, provided that the composed system is deadlock-free and the composed architectures are pairwise non-interfering in the following sense. Architecture A 1 is non-interfering w.r.t. architecture A 2 and a set of components C 1 , . . . , C n , if each path in (A 1 ⊕ A 2 )[C 1 , . . . , C n ], which executes transitions of the coordinators of A 1 infinitely often, either executes transitions of the coordinators of A 2 or visits their idle states infinitely often. 6Example 6.

Consider the system (A 12 ⊕ A 23 ⊕ A 13 )[C 1 , C 2 , C 3 ], as in Example 5.
Let each coordinator have a single idle state free. Consider the applications of each pair of coordinators, i.e. (A

12 ⊕A 23 )[C 1 , C 2 , C 3 ], (A 23 ⊕A 13 )[C 1 , C 2 , C 3 ] and (A 12 ⊕ A 13 )[C 1 , C 2 , C 3 ]. For (A 12 ⊕ A 23 )[C 1 , C 2 , C 3 ],
we observe that along any infinite path, either D 12 executes infinitely often, or remains forever in its idle state after some point. Hence, A 23 is non-interfering w.r.t. A 12 and C 1 , C 2 , C 3 . Likewise for the five other ordered pairs of coordinators. It can be verified that (A 12 ⊕ A 23 ⊕ A 13 )[C 1 , C 2 , C 3 ] is deadlock-free. Hence, we conclude that (A 12 ⊕ A 23 ⊕ A 13 ) is live. Thus, verifying liveness in a composed system is reduced to checking the deadlock-freedom and pairwise non-interference of architectures, both of which can be performed compositionally.

To put the above vision for correctness into practice, we need to develop a repository of reference architectures. The repository should classify existing architectures according to their characteristic properties. There exists a plethora of results on distributed algorithms, protocols, and scheduling algorithms. Most of these results focus on principles of solutions and discard essential operational details. Their correctness is usually established by assume/guarantee reasoning: a characteristic global property is implied from properties of the integrated components. This is enough to validate the principle but does not entail correctness of particular implementations. Often, these principles of solutions do not specify concrete coordination mechanisms (e.g. in terms of operational semantics), and ignore physical resources as time, memory and energy. The reference architectures included in the repository, should be described as executable models in the chosen component framework; proven correct with respect to their characteristic properties; characterised in terms of performance, efficiency and other essential nonfunctional properties.

For enhanced reuse, reference architectures should be classified according to their characteristic properties. A list of these properties can be established; for instance, architectures for mutual exclusion, time-triggered, security, faulttolerance, clock synchronisation, adaptive, scheduling, etc. Is it possible to find a taxonomy induced by a hierarchy of characteristic properties? Moreover, is it possible to determine a minimal set of basic properties and corresponding architectural solutions from which more general properties and their corresponding architectures can be obtained?

The example of the decomposition of fault-tolerant architectures into basic features can be applied to other architectures. Time-triggered architectures usually combine a clock synchronisation algorithm and a leader election algorithm. Security architectures integrate a variety of mitigation mechanisms for intrusion detection, intrusion protection, sampling, embedded cryptography, integrity checking, etc. Communication protocols combine sets of algorithms for signalling, authentication and error detection/correction. Is it possible to obtain by incremental composition of features and their characteristic properties, architectural solutions that meet given global properties? This is an open problem whose solution would greatly enhance our capability to develop systems that are correct-by-construction and integrate only the features needed for a target characteristic property.

Architecture Specification

So far we have focused on modelling component-based systems and on methods for proving their behavioural correctness. In this section, we study logics for the specification of properties of architectures. Notice that the presented architecture modelling adopts an imperative description style: the coordination between components is given by a set of connectors. No interaction is allowed except the ones specified by connectors. In contrast, logics adopt a declarative style. A logical specification is the conjunction of formulas; meaning is the set of the models belonging to the intersection of the meanings of the formulas. Consequently, logical specifications characterise not a single model but a set of models that may be empty. In the latter case, the specification is inconsistent.

Typically, an architecture defines a set of interactions between types of components. On the contrary, a class of architectures, what is usually called an architecture style, is represented by a set of congurations. We propose two types of logics for architectures: 1) Interaction logics to specify a particular architecture as the set of the allowed interactions; 2) Configuration logics to specify families of architectures as the set of the allowed configurations of interactions.

Configurations are defined as follows. Given a set of ports P an interaction a is a subset of P ; there exist 2 |P | interactions on P . A configuration is a set of interactions a 1 , . . . , a n represented by a term of the form a 1 + • • • + a n where + is an associative commutative and idempotent operator. Notice that there exist 2 2 |P | configurations on the alphabet P . For instance, if P = {p, q} then the set of non-empty interactions is {p, q, pq} and the set of non-empty configurations is {p, q, pq, p + q, pq + p, pq + q, pq + p + q}.

For example, it is shown in the next subsection that the dynamic Master/Slave architecture presented in Section 3.3 can be specified in Interaction Logic. The class of Master/Slave architectures can be characterized by a formula of the configuration logic that specifies all the allowed configurations of interactions involving some master and slaves.

Interaction Logics

Let P be an alphabet of ports. The set of the formulas of the propositional interaction logic P IL(P ) is defined by the syntax:

f ::= true | p ∈ P | f ∧ f | f . ( 17
)
The models of the logic are interactions a on P . The semantics defined by the following satisfaction relation

a i |= p, if p ∈ a, a i |= f 1 ∧ f 2 , if (a i |= f 1 ) ∧ (a i |= f 2 ), a i |= f , if (a i |= f ) does not hold.
We use the logical connectives ∨ and ⇒ with the usual meaning. Notice that the formulas of the logic can be put in the form of the disjunction of monomials p∈I p ∧ p∈J p, such that I ∩ J = ∅. An interaction a is characterised by the monomial p∈a p ∧ p ∈a p. Propositional interaction logic has been extensively studied in [START_REF] Bliudze | Causal semantics for the algebra of connectors[END_REF] where it is shown that it can provide a basis for the efficient representation connectors. For example, the interaction between p 1 , p 2 and p 3 is defined by the formula f 1 = (p 1 ⇒ p 2 )∧(p 2 ⇒ p 3 )∧(p 3 ⇒ p 1 ). Broadcast from a sending port s towards receiving ports r 1 and r 2 is defined by the formula f 2 = (p 1 ⇒ s) ∧ (p 2 ⇒ s). Notice that the non-empty solutions are the interactions s, sp 1 , sp 2 , sp 1 p 2 .

In [START_REF] Bozga | Modeling dynamic architectures using Dy-BIP[END_REF], we have shown that P IL(P ) can be extended into a first order logic to represent architectures built from arbitrary numbers of components, instantiating a finite number of component types. We present a slightly different version of this logic. As in [START_REF] Bozga | Modeling dynamic architectures using Dy-BIP[END_REF], we assume that system specifications are built using arbitrary numbers of typed components. The type T of a component defines its set of ports and associated exported variables. Furthermore, we consider a set of component variables c i with associated component types T . The fact that the component variable c i is of type T is denoted by c i : T . The syntax of the formulas of the first order interaction logic is defined by:

f ::= true | c.p | c = c | f ∧ f | f | ∀c : T.f , (18)
where c and c are component variables.

In this definition, T denotes a component type. Each component type represents a set of component instances with identical interface and behaviour. The variables c and c range over component instances. They are strongly typed and, moreover, they can be tested for equality. The semantics of the logic can be derived from the semantics of the propositional logic as follows.

A formula of the logic defines the set of the interactions of a system built from known instances of typed components. Quantifiers can be eliminated by using the identity: ∀c : T.F (c) ≡ F (t 1 )∧• • •∧F (t k ), where t 1 , . . . , t k are the instances of components of type T in the model. After quantifier elimination, we get a formula of the propositional logic. This logic can be used to specify dynamic architectures. For instance the formula ∀c : Sender.∃c : Receiver.(c.send ∧ c .receive), means that for any Sender there exists a Receiver such that their ports send and receive, respectively, interact. Relevant specification examples using this logic are provided in [START_REF] Bozga | Modeling dynamic architectures using Dy-BIP[END_REF]. Furthermore, it is shown that for a given model the specified interactions can be computed efficiently by using a symbolic representation.

We provide logical specifications for the architecture of the Master-Slave example already seen in Section 3.3. Following the approach in [START_REF] Bozga | Modeling dynamic architectures using Dy-BIP[END_REF], we introduce some additional notations that prove to be very useful for writing specifications: Y.p requires R.q ≡ ∀c : Y. ∃c : R. (c.p ⇒ c .q) (every p port requires a q port for interaction) Y.p accepts R.q ≡ ∀c : Y. Notice the difference in the description styles for the same example. When connectors are used, the style is imperative. The set of the interactions is constructed by enumerating connectors. When formulas are used, the style is declarative. The set of the interactions is in the intersection of the meanings of formulas which express constraints on the interactions required and accepted by each component. It has been shown that the two approaches are equivalent as long as we deal with interactions without data transfer. The association of computation and data transfer with formulas is not as natural as for connectors and raises methodological and technical issues.

The two styles correspond to two different approaches for eliciting architectural knowledge [START_REF] Dhungana | Architectural knowledge in product line engineering: An industrial case study[END_REF]. One is bottom-up and is adopted for building architectural models in various architecture description languages [START_REF]Systems and software engineering -Architecture description[END_REF]. The other is top-down and is used to capture essential dependencies between features.

Configuration Logics

Let P be an alphabet on ports. The set of the formulas of the propositional configuration logic P CL(P ) is defined by the syntax:

f ::= true | m ∈ P IL(P ) | f ∧ f | ¬f | f + f , ( 19
)
where m is a monomial of the interaction logic. The models of the logic are configurations γ on P , of the form γ = a 1 +• • •+a n where the a i 's are interactions on P . The semantics is defined by the satisfaction relation |=.

γ = a 1 + • • • + a n |= m, if, for each a i , a i i |= m, γ = a 1 + • • • + a n |= f 1 + f 2 , if, for each a i , (a i |= f 1 ) or (a i |= f 2 ) ,
where m is a monomial of the interaction logic. For logical constants and connectives we take the standard meaning. Notice the overloading of the + operator. The meaning of the formula f 1 + f 2 is the set of the configurations obtained by combining some configuration f 1 with some configuration satisfying f 2 . In particular, we have the property:

f 1 + (f 2 ∨ f 3 ) = (f 1 + f 2 ) ∨ (f 1 + f 3 ).
A simple example illustrates the expressive power of this logic. Let P = {p, q, r, s} be an alphabet of ports. The monomial p ∧ q ∧ r specifies, in the interaction logic, the set of interactions pq and pqs. In the configuration logic, it specifies the set of configurations pq, pqs and pq+pqs. The formula p∧q∧r+true characterises all the configurations of the form γ = γ 1 + γ 2 , where γ 1 satisfies p ∧ q ∧ r and γ 2 is an arbitrary configuration. Notice, in particular, that true is not an absorbing element for +. Hence, γ 1 cannot be empty.

In general, a formula of the form f + true characterises all the configurations comprising the configurations satisfying f . This type of formulas is particularly useful for writing specifications. We write ∼ f = f + true for any formula f of the logic. The operator ∼ is idempotent and satisfies the following property: ∼f ∧ ∼g = ∼(f + g) for any formulas f and g.

We extend P CL(P ) into a second order logic. We assume that system models are built using arbitrary numbers of typed components. The type T of a component defines its set of ports and associated exported variables. We consider a set of component variables c i with an associated component type T . The fact that the component variable c i is of type T is denoted by c i : T . Furthermore, we consider a set of variables U i ranging over sets of components. This set includes a particular variable U representing the set of all the components of a model. We also adopt the notation U i : T to signify that all components in the set U i are of type T .

The syntax of the second order configuration logic formulas is defined by:

f ::= true | m ∈ P IL(P ) | c = c | c ∈ U | U ⊆ U | f ∧ f | ¬f | f + f | ∀U : T.f | ∀c : T.f , ( 20
)
where m is a monomial, c, c are component variables and U , U are variables over sets of components. The semantics can be derived from the semantics of the propositional logic. For a given model γ(C 1 , . . . , C n ), quantifiers can be eliminated in a formula to obtain a formula of the propositional logic.

The specification of a ring architecture composed of components c : T having ports c.in and c.out is the conjunction of the following formulas:

Formula ( 21) characterises all the configurations such that each output port c.out of a component c is connected to some input port c.in of some other component c and explicitly excludes connections of c.out with input ports of components other than c . Formula ( 22) requires symmetrically connectivity of each input port to a single output port. The two formulas guarantee cyclical connectivity. Formula [START_REF] Souza | Conflict-tolerant features[END_REF] requires that there exists a single (maximal) cycle. It says that any subset U components of the universal set U has a component that is connected to some component of its complement.

A comparison between the ring architecture model given in Section 3.3 and the above logical specification shows significant differences in both the style of expression (imperative vs. declarative) and the basic connectivity concepts. The model does not allow other configurations than the ones explicitly specified. Logical specifications characterise configurations that include token ring architectures without excluding other compatible connectivity properties.

Conclusion

The paper discusses research issues related to the design of component-based systems by distinguishing three main problems. The first problem is modelling composite components as the composition of atomic components characterised by their interface and behaviour. We propose a general framework for component composition and study expressiveness of families of operators. For universal expressiveness, it is necessary to combine multiparty interaction and priorities. We propose the concept of connector as a means for structuring interaction between components. So far, static connectors and their properties have been thoroughly studied. We present an extension for the description of dynamic connectors that needs to be further studied and validated through application.

The second problem is achieving correctness of component-based systems by application of scalable techniques. We identify two possible avenues. One relies on compositionality principles and proceeds by analysis of the composed components and their coordination. The other relies on enforcement of specific properties. A key problem in the application of this approach is composability: how to obtain a system meeting a given global property by composing architectures meeting specific properties? Existing results limit both approaches to particular classes of properties, e.g. deadlock-freedom and state invariants. We believe that a significant research effort is needed to overcome these limitations.

The third problem is using logics to characterise architectures and their properties. We show that two types of logics are needed for this purpose. Interaction logics characterise the possible interactions of a system, that is of a particular architecture. These logics have been studied to a large extent and applied in the BIP framework. In contrast, configuration logics can be used to characterise families of architectures, e.g. architecture styles. They are languages used for a feature-oriented analysis of architectures, such as OCL [START_REF]Information technology -Object Management Group -Object Constraint Language (OCL)[END_REF]. The relationships between configuration logic and other approaches for the description of architectures styles [START_REF] Allen | Specifying and analyzing dynamic software architectures[END_REF][START_REF] Koehler | Connector rewriting with high-level replacement systems[END_REF][START_REF] Kumar | Software architecture styles a survey[END_REF][START_REF] Metayer | Describing software architecture styles using graph grammars[END_REF] need to be investigated.

The paper clearly distinguishes between architecture models and two types of logic-based specification formalisms. It also establishes links between the two types of description through satisfaction relations. Table 2 depicts the main characteristics of each formalism and significant differences. Interestingly, static models correspond to propositional logics, while dynamic models to higher order logics. Both dynamic models and higher order logics share the same basic concepts, e.g. they are defined on a set of typed components by using variables ranging over components and sets of components. Notice that component variables are needed to describe generic models and properties, while variables over sets of components are needed to describe dynamic creation/deletion and dynamic configurations. These similarities should allow a tight comparison of the three proposed formalisms, that needs to be further investigated.

Fig. 1 :

 1 Fig. 1: Component behaviours for Example 2

Example 4 .Fig. 2 :

 42 Fig. 2: Summary of relations between glues

Fig. 5 :

 5 Fig. 5: Dynamic Connectors for the Master-Slave example

Fig. 7 :

 7 Fig. 7: Temperature Control System in BIP

-

  A transforms a set of components C 1 , . . . , C n into a composite component A[C 1 , . . . , C n ] = gl(C 1 , . . . , C n , D); -A[C 1 , . . . , C n ] meets the characteristic property Φ.

Fig. 8 : 5 Example 5 (

 855 Fig. 8: Components (a) and coordinator (b) for Example 5

  As above, A 13 and A 23 enforce on A 13 [C 1 , C 3 ] and A 23 [C 2 , C 3 ], respectively, the mutual exclusion properties Φ 13 = (s 1 = work ∨ s 3 = work) and Φ 23 = (s 2 = work ∨ s 3 = work). The composition of the three architectures A 12 ⊕ A 13 ⊕ A 23 , imposing the mutual exclusion property Φ 12 ∧ Φ 13 ∧ Φ 23 = (s 1 = work ∧ s 2 = work) ∨ (s 2 = work ∧ s 3 = work) ∨ (s 1 = work ∧ s 3 = work) on the three components C 1 , C 2 and C 3 , is given by the set of coordinating components {D 12 , D 13 , D 23 } and the set of interactions γ = {b 1 b 12 b 13 , f 1 f 12 f 13 , b 2 b 12 b 23 , f 2 f 12 f 23 , b 3 b 13 b 23 , f 3 f 13 f 23 } (see [4] for details).

(

  T,r) =(R,q) ∀c : T.((c.p = c .r) ⇒ c .r) p port can only interact with q ports) unique Y.p ≡ ∀c : Y. ∀c : Y.(c.p ∧ c .p ⇒ c = c ) (no interaction between ports p) Using the above abbreviations the architecture of the Master-Slave example is described by the following interaction logic formula: (M.req requires S.get) ∧ (M.req accepts S.get) ∧ (unique S.get) (S.get requires M.req) ∧ (S.get accepts M.req) ∧ (unique M.req) (M.comp requires S.work) ∧ (M.comp accepts S.work) (S.work requires M.comp) ∧ (S.work accepts M.comp) ∧ (unique M.comp)

  ∀c : T.∃c : T ∼(c.out = c .in) ∧ ∀c : T (c = c ).¬ ∼(c.out = c .in) ,(21)∀c : T.∃c : T ∼(c.in = c .out) ∧ ∀c : T (c = c ).¬ ∼(c.in = c .out) ,(22)∀U : T (U = U).∃c ∈ U , c ∈ U \ U . ∼(c.out = c .in) .

Table 1 :

 1 Checking deadlock-freedom on classical benchmarks

Table 2 :

 2 Architectures and Architectural Properties

	Formalism	Architecture	Architecture	Architecture Styles
	features	Modeling	Modeling	Specification -
		Connectors	Interaction Logics	Configuration Logics
		(Imperative)	(Declarative)
	Fixed set of	Static connectors	Propositional	Propositional
	components and	I(P )	interaction logic,	configuration logic,
	connectors	[g(XP ):XP := f (XP )]	e.g. causality rules	e.g. connectivity
				primitives ≈ a and ∼ a
	Typed components;	Generic connectors First-order	First-order
	variables over		interaction logic,	configuration logic
	components		e.g. Dy-BIP
	Variables over	Dynamic connectors Second-order	Second-order
	sets of components		interaction logic	configuration logic

For the sake of simplicity of notations, we consider that ports p have associated exactly one variable Xp. This restriction is, however, irrelevant and we'll consider later examples where any number of variables are associated to ports.

A deadlocked system trivially satisfies all safety properties.

Notice that the "non-interference w.r.t." relation is not commutative.


est destinée au dépôt

Mots-clés: systèmes hydrothermaux, interactions roche-fluide, systèmes de rift adriatique et pyrénéen

Seismic and drill hole data from deep-water distal rifted margins allow to understand the architecture and evolution of these yet little investigated domain. Nonetheless, the thermal evolution is poorly constrained even if hydrothermal systems play a key role in determining the heat fluxes. This Thesis aims to investigate breccias, cements, veins and replacement minerals within the pre-to post-rift sediments that could testify the space-time evolution of rock-fluid interactions. Two fossil analogues are studied: the Adriatic distal margin and the Pyrenean hyper-extended system. Field, petrography and geochemical analyses reveal a strong heterogeneity in the composition of the fluids as well as their hydrothermal features. Two main types of fluids occur: carbonate-rich fluids refer to early rifting phases dominated by high-angle normal faults; silica-rich fluids are related to the last rifting stages characterized by low-angle detachment faults exhuming upper crust and mantle-related rocks. The results of this Thesis highlight how specific changes in the chemistry of the fluid system are intimately linked to the tectonic evolution of rifted margins.

Key words: hydrothermal systems, rock-fluid interactions, Adriatic and Pyrenean rift systemsMotsclés: systèmes hydrothermaux, interactions roche-fluide, systèmes de rift adriatique et pyrénéen.

  Hydrothermal systems in distal rifted margins and their role in the thermal evolution of sedimentary successions : study of two fossil analogues in the Swiss Alps and Pyrenees Nicolo Incerpi To cite this version: Nicolo Incerpi. Hydrothermal systems in distal rifted margins and their role in the thermal evolution of sedimentary successions : study of two fossil analogues in the Swiss Alps and Pyrenees. Earth Sciences. Université de Strasbourg; Università di Torino (Turin, Italie), 2017. English. NNT : 2017STRAH005. me DELLA PORTA Giovanna] Prof., Università degli Studi di Milano [M. BOULVAIS Philippe] Prof., Université de Rennes 1 Hydrothermal systems in distal rifted margins and their role in the thermal evolution of sedimentary successions. Study of two fossil analogues in the Swiss Alps and Pyrenees.