Arnaud Lanoix
email: arnaud.lanoix@univ-nantes.fr

Olga Kouchnarenko
email: olga.kouchnarenko@univ-fcomte.fr

Component Substitution through Dynamic Reconfigurations

Component substitution has numerous practical applications and constitutes an active research topic. This paper proposes to enrich an existing component-based framework-a model with dynamic reconfigurations making the system evolve-with a new reconfiguration operation which "substitutes" components by other components, and to study its impact on sequences of dynamic reconfigurations. Firstly, we define substitutability constraints which ensure the component encapsulation while performing reconfigurations by component substitutions. Then, we integrate them into a substitutabilitybased simulation to take these substituting reconfigurations into account on sequences of dynamic reconfigurations. Thirdly, as this new relation being in general undecidable for infinite-state systems, we propose a semi-algorithm to check it on the fly. Finally, we report on experimentations using the B tools to show the feasibility of the developed approach, and to illustrate the paper's proposals on an example of the HTTP server.

Introduction

Dynamic reconfigurations [START_REF] Cornejo | Specification and Verification of a Dynamic Reconfiguration Protocol for Agent-Based Applications[END_REF][START_REF] Aguirre | A Temporal Logic Approach to the Specification of Reconfigurable Component-Based Systems[END_REF][START_REF] Léger | Reliable Dynamic Reconfigurations in a Reflective Component Model[END_REF] increase the availability and the reliability of component-based systems by allowing their architecture to evolve at runtime. In this paper, in addition to dynamic evolution reconfigurations, possibly guided by temporal patterns [START_REF] Dormoy | Using Temporal Logic for Dynamic Reconfigurations of Components[END_REF][START_REF] Lanoix | Combining Proof and Model-checking to Validate Reconfigurable Architectures[END_REF][START_REF] Dormoy | Runtime Verification of Temporal Patterns for Dynamic Reconfigurations of Components[END_REF], we consider reconfigurations bringing into play by component substitutions. These reconfigurations by substitution may change the model's behaviour. The questions we are interested in are: How are such model transformations represented? What aspects of the model's behaviour can be changed? Can new behaviour be added, can existing behaviours be replaced or combined with new behaviours? More precisely, in our previous works [START_REF] Dormoy | Using Temporal Logic for Dynamic Reconfigurations of Components[END_REF][START_REF] Lanoix | Combining Proof and Model-checking to Validate Reconfigurable Architectures[END_REF][START_REF] Dormoy | Runtime Verification of Temporal Patterns for Dynamic Reconfigurations of Components[END_REF], a component-based framework has been developed: an component architecture with dynamic reconfigurations has been defined and shown consistent, a linear temporal pattern logic allowing expressing properties over sequences of dynamic reconfigurations has been defined. Component substitution reconfigurations being motivated by numerous practical applications, this paper proposes to enrich the existing component-based framework with a notion of component substitutability. Since the model is formulated as a theory in FOL, this is achieved by introducing a new relation over components, and a set of logical constraints. Then, the paper presents a notion of simulation between dynamic reconfigurable systems wrt. a given component substitution relation, and addresses the checking of this relation, which is known to be, in general, undecidable.

Figure 1 displays two kinds of considered reconfigurations: Horizontal reconfigurations represent the dynamic architecture's evolution whereas vertical substitutions lead to different implementations. As the model and its implementations must remain consistent through evolution, we study the impact of reconfigurations by substitution on sequences of dynamic reconfigurations.

The main purpose of the present paper consists in studying the impact of reconfigurations by substitution on sequences of dynamic reconfigurations. To this end, we propose to extend the previous work in [START_REF] Lanoix | Combining Proof and Model-checking to Validate Reconfigurable Architectures[END_REF] on the verification of the architectural consistency using the B tools by, first, evaluating component substitutability and, second, by evaluating sequences of reconfigurations-and, consequently, the substitutability-based simulation. For this we propose to use the B 4 = {⊥, ⊥ p , ⊤ p , ⊤} truth domain which is suitable to evaluate the substitution relation on the fly. Using B 4 is in line with the work in [START_REF] Dormoy | Runtime Verification of Temporal Patterns for Dynamic Reconfigurations of Components[END_REF] on the runtime verification of linear temporal logic properties.

Layout of the paper. In Sect. 2 we recall the main features of the architectural reconfiguration model introduced in [START_REF] Dormoy | Using Temporal Logic for Dynamic Reconfigurations of Components[END_REF][START_REF] Lanoix | Combining Proof and Model-checking to Validate Reconfigurable Architectures[END_REF] and illustrate them on an example of the HTTP server. In Sect. [START_REF] Aguirre | A Temporal Logic Approach to the Specification of Reconfigurable Component-Based Systems[END_REF], a new reconfiguration operation by component substitution is introduced and substitutability constraints are defined to ensure component encapsulation. In Sect. 4 component substitutability is integrated into a substitutability-based simulation relation. This relation being undecidable in general, a semi-algorithm is proposed to evaluate on the fly dynamic reconfiguration sequences and, consequently, the component substitutability-based simulation. Section 5 explains how to use the B tools for dealing with component substitutability through dynamic reconfigurations, and describes experiments on the HTTP server example. Finally, we conclude in Sect. 6.

Background: Architectural Reconfiguration Model

The reconfigurations we consider here make the component-based architecture evolve dynamically. They are combinations of primitive reconfiguration operations such as instantiation/destruction of components; addition/removal of components; binding/unbinding of component interfaces; starting/stopping components; setting parameter values of components. In general, system configuration is the specific definition of the elements that define or prescribe what a system is composed of. We define a configuration to be a set of architectural elements (components, required or provided interfaces and parameters) together with relations to structure and to link them, as depicted in Fig. 2 1 .

Components

Given a set of configurations C = {c, c 1 , c 2 , . . .}, we introduce a set CP of configuration properties on the architectural elements and the relations between them. These properties are specified using first-order logic formulas. The interpretation of functions, relations, and predicates is done according to basic definitions in [START_REF] Hamilton | Logic for mathematicians[END_REF] and in [START_REF] Dormoy | Runtime Verification of Temporal Patterns for Dynamic Reconfigurations of Components[END_REF] 1 . We now define a configuration interpretation function l : C → CP which gives the largest conjunction of cp ∈ CP evaluated to true on c ∈ C 2 .

Among all the configuration properties, we consider the architectural consistency constraints CC which express requirements on component assembly common to all the component architectures. They allow defining consistent configurations which notably respect the following rules. Their intuition is as follows, together with a formal description for several constraints3 :

• a component supplies one provided interface, at least;

• the composite components have no parameter;

• a sub-component must not be a composite including its own parent component; • two bound interfaces must have the same interface type; they are not supplied by the same component, but their containers are sub-components of the same composite;

∀ip ∈ ProvInter f aces, ∀ir ∈ ReqInter f aces .

    Binding(ip) = ir ⇒ Inter f aceType(ip) = Inter f aceType(ir) ∧ Container(ip) = Container(ir) ∧ ∃ c ∈ Components. (Container(ip), c) ∈ Parent ∧(Container(ir), c) ∈ Parent    
• when binding two interfaces, there is a need to ensure that they have not been involved in a delegation yet; similarly, when establishing a delegation link between two interfaces, the specifier must ensure that they have not been involved in a binding yet;

• a provided (resp. required) interface of a sub-component is delegated to at most one provided (resp. required) interface of its parent component; the interfaces involved in the delegation must have the same interface type;

• a component is started only if its mandatory required interfaces are bound or delegated.

Definition 1 (Consistent configuration) Let c = Elem, Rel be a configuration and CC the architectural consistency constraints. The configuration c is consistent, written consistent(c), if l(c) ⇒ CC.

Let R be a finite set of reconfiguration operations. The possible evolutions of the component architecture via the reconfiguration operations are defined as a transition system over R. To illustrate our model, let us consider an example of the HTTP server 4 . The architecture of this server is depicted in Fig. 3. The RequestReceiver component reads HTTP requests from the network and transmits them to the RequestHandler component. In order to keep the response time as short as possible, RequestHandler can either use a cache (with the component CacheHandler) or directly transmit the request to the RequestDispatcher component. The number of requests (load) and the percentage of similar requests (deviation) are two parameters defined for the RequestHandler component. The CacheHandler component is used only if the number of similar HTTP requests is high. The memorySize for the CacheHandler component depends on the overall load of the server. The validityDuration of data in the cache also depends on the overall load of the server. The number of used file servers (like the FileServer1 and File-Server2 components) used by RequestDispatcher depends on the overall load of the server. On this example, the considered reconfiguration operations are:

• AddCacheHandler and RemoveCacheHandler which are used to add and remove CacheHandler;

• AddFileServer and removeFileServer which are used to add and remove FileServer2;

• MemorySizeUp and MemorySizeDown which are used to increase and to decrease the MemorySize value;

• DurationValidityUp and DurationValidityDown which are used to increase and to decrease the ValidityDuration value. A possible evolution path of the HTTP server architecture is given in Fig. 4. In this section we enrich our componentbased framework with a new kind of reconfigurations allowing a structural substitution of the components with respect the component encapsulation. In fact, we want the substituted component to supply the same interfaces of the same types as before. This way the other components do not see the difference between the component and its new "substituted" version, and thus there is no need to adapt them. As the substitution of a component should not cause any changes outside of this component, only the two following kinds of component substitutions are allowed:

New Reconfigurations by Component Substitution

mandatory optional stopped started State R Parameters R Container A Value R Contingency A Container Type R Binding R Delegate R Provided Interfaces R Required Interfaces R Binding A Delegate A Provided Interfaces A Required Interfaces A Contingency R Components R Parent A Components A Parent R State A Container Type A Parameters A Container R Value A PTypes R PTypes A ITypes A ITypes R
• either a component can be replaced by a new version of itself, or

• a component can be replaced by a composite component which encapsulates new sub-components providing at least the same functionalities as before substitution.

For the allowed substitution cases, Figure 5 displays how the architectural elements and relations are defined at two pre-and post-substitution levels. Let c A and c R be two architectural configurations at respectively a pre-substitution and a post-substitution levels. The substitute reconfiguration is then expressed by a partial function Subst : Components A → Components R that gives how the components are substituted in c A to obtain c R . Let us illustrate our proposal on the example of the HTTP server. For the configuration in Fig. 6, we apply the following substitute reconfiguration: We have

Subst(CacheHandler) = CacheHandler_R Subst(RequestHandler) = RequestHandler_R
as substitute reconfiguration function.

In order to ensure that proposed substitutions respect the requirements on components and their assembly, we now introduce architectural constraints on both replaced (or old) and substituted (or new) components. These architectural constraints, named SC Subst , describe which changes are allowed or prescribed by a substitute reconfiguration. Their intuition is as follows, together with a formal description for several constraints5 :

• In the system parts not concerned by the component substitution, all the core entities and all the relations between them remain unchanged through the substitution process:

the old parameters and the associated types remain unchanged in the substitutes; the old components remain unchanged;

∀c ∈ Components A ∩Components R , ∀x ∈ Inter f aces A ⊎ Parameters A . (Container A (x) = c ⇒ Container R (x) = c)
the old interfaces and their types are not changed; the old connections between component's interfaces are kept as well.

• For the old components impacted by the components substitution, the constraints are as follows:

an old component completely disappears only if it is substituted by a new version for itself;

∀c A . c A ∈ Components A \Components R ⇒ ∃c R ∈ Components R \Components A . (Subst(c A ) = c R )
Component Substitution through Dynamic Reconfigurations the substituted components are in the same state as the old ones, and either they have the same parent component as before substitution, or the old parent component has been substituted as well; the interfaces of the replaced components are supplied by the substituted components; the parameters of the replaced components are defined either on the substituted components, or on their subcomponents.

• The new elements introduced during the substitution process cannot impact the old conserved architecture:

the newly introduced components must be subcomponents of some substituted components;

∀c R ∈ Components R \Components A , ∀c A ∈ Components A \Components R . Subst(c A ) = c R ⇒ ∃c ′ R ∈ Components R \Components A . ((c R , c ′ R ) ∈ Parent R )
the newly introduced interfaces must be associated with the new components;

∀i. i ∈ ProvInter f aces R \ProvInter f aces A ⇒ Container R (i) ∈ Components R \Components A
the newly introduced parameters are associated with the new components; the new connections are used to connect the new components.

Definition 3 (Structural substitutability) Let c A and c R be two consistent configurations, Subst the substitution function, and SC Subst the architectural substitutability constraints. The configuration c R is

substitutable to c A , written subst(c R , c A ), if l(c R ) ∧ SC Subst ⇒ l(c A ).

Component Substitution through Dynamic Evolution

The new reconfigurations by component substitution defined in Sect. 3 must be taken into account in evolutions of component-based architectures. Indeed, as the substituted or the newly introduced components may introduce new dynamic reconfigurations, the architectures with substituted components may evolve by the old reconfigurations as well as by new reconfigurations. We want these reconfigurations to be consistent with the reconfigurations by substitution.

To this end, we integrate the architectural substitutability constraints from Sect. 3 into a simulation relation linking dynamic reconfigurations of a system after component's substitutions with their old counterparts that where possible before the component substitution. We then define a substitution relation ρ in the style by Milner-Park [START_REF] Milner | Communication and Concurrency[END_REF] as a simulation having the following properties, which are common to other formalisms like action systems [START_REF] Butler | Stepwise Refinement of Communicating Systems[END_REF] or LTL refinement [START_REF] Kesten | Temporal Verification of Simulation and Refinement[END_REF]:

1. Adding the new dynamic reconfiguration actions should not introduce deadlocks 6 .

2. Moreover, the new dynamic reconfiguration actions should not take control forever: the livelocks formed by these actions are forbidden.

Definition 4 (Substitutability-based simulation)

Let S A = C A , C 0 A , R A , → A and S R = C R , C 0 R , R R , → R be two reconfiguration models. Let σ R be a path of S R . A relation ⊑ subst ⊆ C R ×C A is
the substitutabilitybased simulation iff whenever c R ⊑ subst c A then it implies: structural substitutability (i), strict simulation (ii), stuttering simulation (iii), non introduction of divergence (iv), and non introduction of deadlocks (v), defined as follows: 6 We write c R → to mean that ∀ope, c ′ .

c ope → c ′ ∈→. subst(c R , c A ) (i) ∀c ′ R ∈ C R , ope ∈ R R ∩ R A .(c R ope → c ′ R ⇒ ∃c ′ A ∈ C A .(c A ope → c ′ A ∧ c ′ R ⊑ subst c ′ A )) (ii) ∀c ′ R ∈ C R , ope ′ ∈ R R \ R A .(c R ope ′ → c ′ R ⇒ c ′ R ⊑ subst c A ) (iii) ∀c ′ R ∈ C R , ope ′ ∈ R R \ R A , k.(k ≥ 0 ∧ c R = σ R (k) ∧ c R ope ′ → c ′ R ⇒ ∃k ′ , ope ∈ R R ∩ R A . (k ′ > k ∧ σ R (k ′ ) ope → σ R (k ′ + 1))) (iv) ∀c A ∈ C A , ∀c R ∈ C R .(c R ⊑ subst c A ∧ c R → ⇒ c A →) (v)
We call the substitutability-based simulation (or the substitutability for short) the greatest binary relation over the configurations of S R and S A satisfying the above definition. We say that S R is simulated by S A wrt. the component substitutability, written The substitutability-based simulation defined above can be viewed as a divergence sensitive stability respecting completed simulation in van Glabbeek's spectrum [START_REF] Van Glabbeek | The Linear Time -Branching Time Spectrum II[END_REF]. Since the models are infinite state, the problem to know whether the substitutabilitybased simulation holds or not is undecidable in general. Consequently, we provide a semialgorithm to check the substitutability-based simulation on the fly.

S R ⊑ subst S A , if ∀c R .(c R ∈ C 0 R ⇒ ∃c A .(c A ∈ C 0 A ∧ c R ⊑ subst c A )). 1 Data: c 0 R ∈ C 0 R , c 0 A ∈ C 0 A , R R and R A 2 Result: res ∈ {⊥, ⊤}, if terminates 3 c R ← c 0 R ; 4 c A ← c 0 A ; 5 while ⊤ do 6 if subst(c R , c A ) then 7 E R ← enabled(c R , R R ) ; 8 E A ← enabled(c A , R A ) ; 9 if E R = / 0 then 10 if E A = / 0 then
The substitutability-based simulation cannot be evaluated to true or false during the system's execution: actually, as the clauses of the substitutability relation ⊑ subst depend not only on the current configurations but also on the target configurations, and even more on sequences of future configurations as in (iv), in general they cannot be evaluated to true or false on the current pair of configurations. But, on the other hand, if one of the clauses of Def. 4 is evaluated to false on finite parts of the reconfiguration sequences, then obviously the whole relation does not hold. So, instead of considering the whole transition systems, let us consider a sequence of reconfigurations before substitutions and its counterpart obtained by applying reconfigurations by substitution.

We propose a semi-algorithm displayed in Fig. 7 to evaluate the substitutability-based simulation starting from the initial configurations c 0 R ∈ C 0 R , c 0 A ∈ C 0 A . This semi-algorithm uses the following auxiliary functions:

• consistent(c ∈ C ) ∈ {⊥, ⊤} -to determine whether the configuration c is consistent (cf. Def. 1);

• subst(c R ∈ C R ,c A ∈ C A )
∈ {⊥, ⊤} -to determine whether the configuration c R is substitutable to c A (cf. Def 3) ;

• enabled(c ∈ C , R ⊆ R) ⊆ R -to determine the subset of reconfigurations in R which can be enabled from c;

• pick-up(E ⊆ R) ∈ R -to choose an operation among reconfigurations in E ;

• apply(c ∈ C ,ope ∈ R) ∈ C -to compute the target configuration when applying ope to c.

Let us have a close look at the semi-algorithm. When it terminates and returns ⊤ (line 9), finite paths have been considered, no more reconfiguration can be fired at both pre-and post-substitution levels, and all clauses of Def. 4 are satisfied on these finite paths. The semi-algorithm returns ⊥ in the following three cases.

• Either Line 25 indicates that clause (i) of Def. 4 concerning the structural substitutability from Def. 3 is broken.

• Or Line 10 indicates that there is a deadlock at the level after substitutions but not at the level before components substitutions. In this case clause (v)-the non-introduction of deadlocks-of Def. 4 is broken.

• Or Line 21 indicates that clause (ii)-the strict simulation-of Def. 4 is broken.

Otherwise, we cannot conclude because the semi-algorithm can choose reconfigurations to be applied, and the substitution verification goes on, possibly over infinite paths. Nevertheless, even in this inconclusive case, the semi-algorithm can provide some indications on the current status of the substitutability. Let us consider the set B 4 = {⊥, ⊥ p , ⊤ p , ⊤} where ⊥, ⊤ stand resp. for false and true values where as ⊥ p , ⊤ p stand resp. for potential false and potential true values. Like for evaluating temporal properties at runtime as in [START_REF] Dormoy | Runtime Verification of Temporal Patterns for Dynamic Reconfigurations of Components[END_REF], potential true and potential false values are chosen whenever an observed behaviour has not yet lead to a violation of the substitutability-based simulation. With this in mind, when a new reconfiguration is applied, ⊥ p in Line 15 indicates

• either a potential trouble with the stuttering simulation: clause (iii) of Def. 4 may be broken if, on the next iteration of the semi-algorithm, the structural substitutability-clause (i)-does not hold between the configuration reached on the path with substitutions and the old configuration on the path before component substitutions;

• or a potential divergence: clause (iv) of Def. 4 may be broken if no old reconfiguration occurs in the future.

Finally, when the semi-algorithm indicates ⊤ p , at Line 18, it means that the clauses of Def. [START_REF] Aldric | Using Types to Enforce Architectural Structure[END_REF] have not yet been violated, and the verification of the substitutability-based simulation must continue.

Proposition 1 Given S A and S R , if the substitutability semi-algorithm terminates by providing the ⊥ value then one has S R ⊑ subst S A .

The idea behind Proposition 1 is as follows: if there are two sequences of dynamic reconfigurations on which one of the substitutability relation clauses is violated then it does imply the substitutabilitybased simulation violation.

Let us illustrate the evaluation of the substitutability relation on the example displayed in Fig. 8. As new dynamic reconfigurations introduced by the component substitution, we consider AddLogger and RemoveLogger which consist respectively in adding or removing the newly introduced Logger component (see Fig. 6). When a new reconfiguration is executed (leading for example to 14 linked to 02), the evaluation gives ⊥ p , although the structural substitutability holds. It is due to the fact that the new reconfigurations may take control forever, depending of course on future reconfigurations. In contrast, when an

Experiments

This section provides a proof of concept by reporting on experiments using the B tools to express and to check the consistency and substitutability constraints, and to implement the substitutability semialgorithm.

A Formal Toolset: the B Method

B is a formal software development method used to model systems and to reason about their development [START_REF] Kouchnarenko | The B Book -Assigning Programs to Meanings[END_REF]. When building a B machine, the principle is to express system properties-invariants-which are always true after each evolution step of the machine, the evolution being specified by the B operations. The verification of a machine correctness is thus akin to verifying the preservation of these properties, no matter which step of evolution the system takes. The B method is based on set theory, relations and first-order logic. Constraints are specified in the INVARIANT clause of the machine, and its evolution is specified by operations in the OPERATIONS clause. Let us assume here that the initialisation is a special kind of operation. In this setting, the consistency checking of a B machine consists in verifying that each operation satisfies the INVARIANT assuming its precondition and the invariant hold.

Tool supports, such as B4free or AtelierB7 , automatically generate proof obligations (POs) to ensure the consistency in sense of B [START_REF] Kouchnarenko | The B Book -Assigning Programs to Meanings[END_REF]. Some of them are obvious POs whereas the other POs have to be proved interactively if it was not done fully automatically by the different provers embedded into AtelierB. Another tool, called ProB8 , allows the user to animate B machines for their debugging and testing. On the verification side, ProB contains a constraint-based checker and a LTL bounded model-checker with particular features; Both can be used to validate B machines [START_REF] Leuschel | ProB: A Model Checker for B[END_REF][START_REF] Leuschel | Seven at one stroke: LTL model checking for High-level Specifications in B, Z, CSP, and more[END_REF].

Consistency Checking by Proof and Model Animation

This section summarises the work in [START_REF] Lanoix | Combining Proof and Model-checking to Validate Reconfigurable Architectures[END_REF] on specifications in B of the proposed component-based model with reconfigurations, and on verification process using the B tools, by combining proof and modelchecking techniques. Let us consider the B machines which, for readability reasons, are simplified versions of the "real" B machines.

MACHINE

Archi VARIABLES Components, Interfaces , ProvInterfaces , ReqInterfaces , Supplier , Parent, Binding, ...

INVARIANT ProvInterfaces ⊆ Interfaces ∧ ReqInterfaces ⊆ Interfaces ∧ ProvInterfaces ∪ ReqInterfaces = Interfaces ∧ ProvInterfaces ∩ ReqInterfaces = ∅ ∧ Supplier ∈ Interfaces → Components ∧ Parent ∈ Components ↔ Components ∧ Binding ∈ ProvInterfaces → ReqInterfaces ∧ closure1 (Parent) ∩ id (Components) = ∅ / * CC.3 * / ∧ ∀ ( ip , ir ).( ip → ir ∈ Binding ⇒ Provider ( ip ) = Requirer( ir ) ∧ Parent( Supplier ( iprov )) = Parent(Supplier( ireq )) ) / * CC.4 + CC.5 * / ∧ ... OPERATIONS bind( ip , ir ) = PRE ip ∈ ProvInterfaces ∧ ir ∈ ReqInterfaces ∧ ip →ir / ∈ Binding ∧ ip / ∈ dom(Binding) ∧ ip / ∈ dom(Delegate) ∧ ir / ∈ dom(Delegate) THEN Binding( ip ) := ir END ;
.

.. END

The configuration model given in Def. 5 can be easily translated into a B machine Archi ((1) in Fig. 9). In this machine, the sets as Components or Interfaces , and relations as Parent or Binding are defined into the VARIABLES clause; the architectural consistency constraints CC are defined into the INVARIANT clause; the basic reconfigurations operations as bind(ip, ir) or start(compo) are also defined here as B operations. Then, we use the AtelierB tool to interactively demonstrate the consistency of the architectural constraints ((2) in Fig. 9) through the basic reconfiguration operations.

Afterwards, we use the ProB model-checker to animate the Substitutability machine and to exploresimultaneously-the two instantiated B models, i.e. the pre-/post-substitution component architectures ((6) in Fig. 9). This animation allows us to perform the evaluations needed for the semi-algorithm from Section 4: we choose the next dynamic reconfiguration to be applied on the "Enabled operations" windows of ProB (see Fig. 10); if it is an old reconfiguration operation, it is simultaneously executed into AA_Reconfig and RR_Reconfig, otherwise it is only run into RR_Reconfig; then, the INVARIANT checking corresponds to the validation of all the SC Subst constraints.

Discussion and Conclusion

Related work. For distributed components like Fractal, GCM and ProActive components, the role of automata-based analysis providing a formal basis for automatic tool support is emphasised in [START_REF] Barros | Behavioural models for distributed Fractal components[END_REF]. In the context of dynamic reconfigurations, ArchJava [START_REF] Aldric | Using Types to Enforce Architectural Structure[END_REF] gives means to reconfigure Java architectures, and to guarantee communication integrity at run-time. In [START_REF] Barringer | From Runtime Verification to Evolvable Systems[END_REF] a temporal logic based framework to deal with systems evolution is proposed.

To compare processes or components, the bisimulation equivalence by Milner [START_REF] Milner | A Calculus of Communicating Systems[END_REF] and Park [START_REF] Park | Concurrency and Automata on Infinite Sequences[END_REF] is widely used: It preserves branching behaviours and, consequently, most of the dynamic properties; there is a link between the strong bisimulation and modal logics [START_REF] Hennessy | Algebraic Laws for Nondeterminism and Concurrency[END_REF]; this is a congruence for a number of composition operators. There are numerous works dealing with component substitutability or interop-erability [START_REF]Component-Based Software Engineering, 10th International Symposium, CBSE 2007[END_REF][START_REF] Cerná | Component Substitutability via Equivalencies of Component-Interaction Automata[END_REF][START_REF] Brada | Practical Verification of Component Substitutability Using Subtype Relation[END_REF]. Our work is close to that in [START_REF] Cerná | Component Substitutability via Equivalencies of Component-Interaction Automata[END_REF], where a component substitutability is defined using equivalences between component-interaction automata wrt. a given set of observable labels. In the present work, in addition to a set of labels, divergency, livelocks are taken into account when comparing execution paths. As KLAPER [START_REF] Grassi | KLAPER: An Intermediate Language for Model-Driven Predictive Analysis of Performance and Reliability[END_REF], Palladio [START_REF] Becker | Model-Based performance prediction with the palladio component model[END_REF] and RoboCop [START_REF] Fioukov | Evaluation of Static Properties for Component-Based Architectures[END_REF] component models do not define any refinement/substitution notion, they are clearly distinguishable form our work.

Let us remark that the substitutability-based simulation in this paper is close to the refinement relation in [START_REF] Dormoy | When Structural Refinement of Components Keeps Temporal Properties Over Reconfigurations[END_REF]. However, as [START_REF] Dormoy | When Structural Refinement of Components Keeps Temporal Properties Over Reconfigurations[END_REF] focuses on a linear temporal logic property preservation, no method is given in [START_REF] Dormoy | When Structural Refinement of Components Keeps Temporal Properties Over Reconfigurations[END_REF] to verify the structural refinement.

Conclusion. This paper extends the previous work on the consistency verification of the componentbased architectures by introducing a new reconfiguration operation based on components substitutions, and by integrating it into a simulation relation handling dynamic reconfigurations. A semi-algorithm is proposed to evaluate on the fly the substitutability relation and its partial correctness is established. As a proof of concept, the B tools are used for dealing with the substitutability constraints through dynamic reconfigurations. As the ProB tool can deal with a dialect of linear temporal logic, we intend to accompany the present work on component substitutability with a runtime (bounded) model-checking of linear temporal logic patterns. Further, we plan to combine our results with adaptation policies: the partial evaluations ⊥ p and ⊤ p could be informations taken into account into the adaption policies framework to choose the most appropriate reconfiguration that will be applied.

A Architectural Configuration Definition [START_REF] Dormoy | Runtime Verification of Temporal Patterns for Dynamic Reconfigurations of Components[END_REF] Definition 5 (Configuration) A configuration c is a tuple Elem, Rel where

(ip) = c))) (CC.1) ∀c, c ′ ∈ Components.(c = c ′ ∧ (c, c ′ ) ∈ Parent ⇒ ∀ p.(p ∈ Parameters ⇒ Container(p) = c ′ )) (CC.2) ∀c, c ′ ∈ Components.((c, c ′ ) ∈ Parent + ⇒ c = c ′ ) (CC.
(i) = ir) (CC.7) ∀i, i ′ ∈ Inter f aces.(Delegate(i) = i ′ ∧ i ∈ ProvInter f aces ⇒ i ′ ∈ ProvInter f aces) (CC.8) ∀i, i ′ ∈ Inter f aces.(Delegate(i) = i ′ ∧ i ∈ ReqInter f aces ⇒ i ′ ∈ ReqInter f aces) (CC.9) ∀i, i ′ ∈ Inter f aces. Delegate(i) = i ′ ⇒ Inter f aceType(i) = Inter f aceType(i ′ ) ∧ (Container(i),Container(i ′ )) ∈ Parent (CC.10) ∀i, i ′ , i" ∈ Inter f aces. (Delegate(i) = i ′ ∧ Delegate(i) = i" ⇒ i ′ = i") ∧(Delegate(i) = i" ∧ Delegate(i ′ ) = i" ⇒ i = i ′ ) (CC .
∀c A ∈ Components A \Components R , ∀c R ∈ Components R \Components A , ∀c ′ A ∈ Components A .       Subst(c A ) = c R ∧ (c A , c ′ A ) ∈ Parent A ⇒       c ′ A ∈ Components R ∧ (c R , c ′ A ) ∈ Parent R ∨ c ′ A / ∈ Components R ∧ ∃c ′ R ∈ Components R \Components A . ((c R , c ′ R ) ∈ Parent ∧ Subst(c ′ A ) = c ′ R )             (SC.11) ∀c R ∈ Components R \Components A , ∀c A ∈ Components A \Components R .   Subst(c A ) = c R ⇒ ∃c ′ R ∈ Components R \Components A . ((c R , c ′ R ) ∈ Parent R )
  (SC.12)

ITypes A ⊆ ITypes R ∧

Figure 1 :

 1 Figure 1: Different kinds of reconfigurations

Figure 2 :

 2 Figure 2: Configurations = architectural elements and relations

Definition 2 (

 2 Reconfiguration model) The operational semantics of component systems with reconfigurations is defined by the labelled transition system S = C, C 0 , R, → where C = {c, c 1 , c 2 , . . .} is a set of consistent configurations, C 0 ⊆ C is a set of initial configurations, R is a finite set of reconfigurations, → ⊆ C × R × C is the reconfiguration relation. Let us write c ope → c ′ when a target configuration c ′ is reached from a configuration c by a reconfiguration operation ope ∈ R. Given the model S = C, C 0 , R, → , an evolution path σ (or a path for short) in S is a (possibly infinite) sequence of configurations c 0 , c 1 , c 2 , . . . such that ∀i ≥ 0 . (∃ ope i ∈ R.(c i ope i → c i+1 ∈→)). We write σ (i) to denote the i-th configuration of a path σ . Let Σ denote the set of paths, and Σ f (⊆ Σ) the set of finite paths.

Figure 3 :

 3 Figure 3: HTTP server architecture

Figure 4 :

 4 Figure 4: Part of a path of the HTTP server architecture

Figure 5 :

 5 Figure 5: Architectural elements and relations before(grey) and after(black) reconfiguration by substitution

Figure 6 :

 6 Figure 6: Applying a reconfiguration by substitution on the HttpServer example

Figure 7 :

 7 Figure 7: Semi-algorithm on the substitutability

Figure 8 :

 8 Figure 8: Substitutability evaluation at runtime

Figure 10 :

 10 Figure 10: The ProB tool: invariant broken illustrating substitutability constraints broken

11 )C 6 )

 116 ∀ir ∈ ReqInter f aces.   State(Supplier(ir)) = started ∧Contingency(ir) = mandatory ⇒ ∃i ∈ Inter f aces. Architectural Substitutability Constraints SC Subst Parameters A ⊆ Parameters R ∧ PTypes A ⊆ PTypes R (SC.1) ∀p.(p ∈ Parameters A ⇒ (ParamType A (p) = ParamType R (p) ∧Value A (p) = Value R (p))) (SC.2)∀p.  p ∈ Parameters R \Parameters A ⇒ Container R (p) ∈ Components R \Components A ∧ ∀c A . c A ∈ Components A \Components R ⇒ Subst(c A ) = Container R (p)   (SC.3) ∀c.(c ∈ Components A ∩Components R ⇒ State A (c) = State R (c)) (SC.4) ∀c ∈ Components A ∩Components R , ∀x ∈ Inter f aces A ⊎ Parameters A . (Container A (x) = c ⇒ Container R (x) = c) (SC.5) ∀c ∈ Components A ∩Components R , ∀c ′ ∈ Components A . c ′ ) ∈ Parent A ⇒ Components R ∧ (c, c ′ ) ∈ Parent R ∨ c ′ / ∈ Components R ∧ ∃c" ∈ Components R \Components A . (Subst(c ′ ) = c" ∧ (c, c") ∈ Parent R ) ∀c A . c A ∈ Components A \Components R ⇒ ∃c R ∈ Components R \Components A . (Subst(C A ) = c R ) (SC.7) ∀c A ∈ Components A \Components R , ∀c R ∈ Components R \Components A . (Subst(c A ) = c R ⇒ State A (c A ) = State R (c R )) (SC.8) ∀c A ∈ Components A \Components R , ∀c R ∈ Components R \Components A . (Subst(c A ) = c R ⇒ (∀i ∈ Inter f aces A .Container A (i) = c A ⇒ Container R (i) = c R )) (SC.9) ∀c A ∈ Components A \Components R , ∀c R ∈ Components R \Components A , ∀p ∈ Parameters A . A ) = c R ∧ Container A (p) = c A ⇒     Container R (p) = c R ∨ ∃c ′ R ∈ Components R \Components A . ((c ′ R , c R ) ∈ Parent + ∧Container R (p) = c ′ R )

HttpServer Request Receiver Request Handler Request Dispatcher File Server1 HttpServer Request Receiver Request Handler Request Dispatcher Cache Handler File Server1 File Server2 HttpServer Request Receiver Request Handler Request Dispatcher Cache Handler File Server1

		Remove		Add		Memory		Add		Duration		Remove
	00	CacheHandler	01	CacheHandler	02	SizeUp	03	FileServer	04	ValidityUp	05	CacheHandler	06

HttpServer Request Receiver Request Handler Request Dispatcher Cache Handler File Server1 HttpServer Request Dispatcher Cache Handler_R File Server1 Request Receiver Logger Request Handler RequestHandler_R HttpServer Request Receiver Request Handler Request Dispatcher Cache Handler File Server1 File Server2 HttpServer Request Dispatcher Cache Handler File Server1 File Server2 Request Receiver Logger Request Handler RequestHandler_R c A c R HttpServer Request Dispatcher Cache Handler_R File Server1 File Server2 Request Receiver RequestHandler_R Request Handler

						Remove		Add		Memory		Add			Duration		Remove
					00	CacheHandler	01	CacheHandler	02	SizeUp	03	FileServer	04	ValidityUp	05	CacheHandler	06
		> p	? p		> p		> p		? p		> p	> p		? p		> p	? p
	10	Remove	11	Remove	12	Add	13	Add	14	Memory	15	Add		16	Remove	17	Duration	18	Add	19
		Logger		CacheHandler		CacheHandler		Logger		SizeUp		FileServer		Logger		ValidityUp	Logger

•

  Elem = Components ⊎ Inter f aces ⊎ Parameters ⊎ Types is a set of architectural elements, such that ITypes ⊎ PTypes is a finite set of the interface types and the parameter data types; Inter f aces ⊎ Parameters → Components is a total function giving the component which supplies the considered interface or the component of a considered parameter; -ContainerType : Inter f aces ⊎ Parameters → Types is a total function that associates a type with each required/provided interface, or with a parameter; -Parent ⊆ Components × Components is a relation linking a sub-component to the corresponding composite component 9 ; -Binding : ProvInter f aces → ReqInter f aces is a partial function which binds together a provided interface and a required one; -Delegate : Inter f aces → Inter f aces is a partial function which expresses delegation links; -State : Components → {started, stopped} is a total function giving the status of instantiated components; -Contingency : ReqInter f aces → {mandatory, optional} is a total function to characterise the required interfaces; -Value : Parameters → ptype∈PType ptype is a total function which gives the current value of each parameter.

	-Components is a non-empty set of the core entities, i.e components;
	-Inter f aces = ReqInter f aces ⊎ ProvInter f aces is a finite set of the (required and provided)
	interfaces;
	-Parameters is a finite set of component parameters;
	Container ⊎ ContainerType ⊎ Parent -Types = • Rel = ⊎ Binding ⊎ Delegate ⊎ State ⊎ Value
	is a set of architectural relations which link architectural elements, such that
	-Container :

B Architectural Consistency Constraints CC ∀c.(c ∈ Components ⇒ (∃ip.(ip ∈ ProvInter f aces ∧Container

  Inter f aces A ⊆ Inter f aces R ∧ProvInter f acesA ⊆ ProvInter f aces R ∧ ReqInter f aces A ⊆ ReqInter f aces R (SC.13) ∀i. (i ∈ Inter f aces A ⇒ Inter f aceType A (i) = Inter f aceType R (i)) (SC.14) ∀i. (i ∈ ReqInter f aces A ⇒ Contingency A (i) = Contingency R (i)) (SC.15) ProvInter f aces A , ∀ri ∈ ReqInter f aces A . (Binding A (pi) = ri ⇒ Binding R (pi) = ri) (SC.18) ∀i, i ′ ∈ Inter f aces A .(Delegate A (i) = i ′ ⇒ Delegate R (i) = i ′ ) (SC.19) ∀pi ∈ ProvInter f aces R , ∀ri ∈ ReqInter f aces R . Binding R (pi) = ri ∧Binding A (pi) = ri ⇒ pi ∈ ProvInter f aces R \ ProvInter f aces A ∧ri ∈ ReqInter f aces R \ ReqInter f aces A

	∀i.	  i ∈ ReqInter f aces R \ReqInter f aces A	⇒	Container R (i) ∈ Components R \Components A	∧ ∀c A .	c A ∈ Components A \Components R ⇒ Subst(c A ) = Container R (i)	  (SC.16)
				∀i. i ∈	ProvInter f aces R \ProvInter f aces A	⇒ Container R (i) ∈	Components R \Components A	(SC.17)
				∀pi ∈

(SC.20) ∀i, i ′ ∈ Inter f aces R

The whole definition is available in Appendix B.

http://fractal.ow2.org/tutorial

The whole definition is available in Appendix C.

http://www.b4free.com / http://www.atelierb.eu

http://www.stups.uni-duesseldorf.de/ProB

For any (p, q) ∈ Parent, we say that q has a sub-component p, i.e. p is a child of q.

Then, the generic B machine Archi is instantiated as Reconfig to represent an architecture under consideration, particularly by giving values to all the sets and relations to represent the considered component architecture configuration and by implementing the non-primitive reconfiguration operations using the basic ones ((3) in Fig. 9). At this point, we can perform a (partial) validation of the instantiated B machine Reconfig through animations, thanks to the ProB model-checker features ((4) in Fig. 9).

Substitutability Checking by Model Animation

We exploit the work in [START_REF] Lanoix | Combining Proof and Model-checking to Validate Reconfigurable Architectures[END_REF] by considering two instantiated B models AA_Reconfig and RR_Reconfig which define two component architectures, wrt. the pre-/post-substitution levels. All the elements and relations are defined twice: AA.Components, RR.Components, AA. Interfaces , RR. Interfaces , AA.Parent or RR.Parent . . . A new machine Substitutability includes these two models ((5) in Fig. 9). It defines the substitute reconfiguration function Subst to link together the AA.Components to the substituted RR.Components. The architectural substitutability constraints SC Subst are defined into the INVARIANT clause of this machine; they are constraints between the elements and relations of AA_Reconfig, and the elements and relations of RR_Reconfig. For example, the reader can see some clauses expressed above as a part of the INVARIANT.

MACHINE