Olga Kouchnarenko
email: okouchnarenko@femto-st.fr

Jean-François Weber
email: jfweber@femto-st.fr

Adapting Component-based Systems at Runtime via Policies with Temporal Patterns

Dynamic reconfiguration allows adding or removing components of component-based systems without incurring any system downtime. To satisfy specific requirements, adaptation policies provide the means to dynamically reconfigure the systems in relation to (events in) their environment. This paper extends event-based adaptation policies by integrating temporal requirements into them. The challenge is to reconfigure component-based systems at runtime while considering both their functional and non-functional requirements. We illustrate our theoretical contributions with an example of an autonomous vehicle location system. An implementation using the Fractal component model constitutes a practical contribution. It enables dynamic reconfigurations guided by either enforcement or reflection adaptation policies.

Introduction

Dynamic reconfiguration is a mechanism that allows components of componentbased systems to be added to or removed without incurring any system downtime. The challenge is to build or maintain trustworthy systems which satisfy both functional and non-functional requirements.

Let us illustrate the adaptation and reconfiguration needs on a characteristic example inspired from a real case study in the land transportation domain. The example concerns the Cybercar concept, a public transport system with automated driving capabilities. Within the autonomous vehicle case study, a location composite component -a critical part of land transportation systems -is made up of different positioning systems, like GPS or Wi-Fi. Thanks to adaptation policies, the location composite component architecture can be modified to use either GPS, Wi-Fi, or GPS+Wi-Fi positioning systems, depending on some non-functional properties, such as available energy.

Recent implementations to support the development of component-based systems, like those for the Fractal reference implementation Julia 3 or for GCM 4 , tend to provide mechanisms for the execution of high-level adaptation policies.

Adaptation polices implemented in Tangram4Fractal [START_REF] Chauvel | Composition et expression qualitative de politiques d'adaptation pour les composants Fractal[END_REF], triggered by qualitative expressions of fuzzy logic (e.g., "power is low"), do not allow expressing temporal constraints. In [START_REF] Dormoy | Event-based Adaptation Policies for Fractal Components[END_REF][START_REF] Dormoy | Using temporal logic for dynamic reconfigurations of components[END_REF], the authors have introduced a component-based system model equipped with either a) adaptation policies using qMEDL5 logic [START_REF] Gonnord | Quantity of resource properties expression and runtime assurance for embedded systems[END_REF] or b) a linear temporal logic, called FTPL 6 , expressing architectural constraints, events, and temporal patterns [START_REF] Dormoy | Using temporal logic for dynamic reconfigurations of components[END_REF]. FTPL, based on Dwyer's work on patterns and scopes [START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF], and being more expressive than qMDEL at providing temporal schemas, this paper proposes to bridge the gap between [START_REF] Dormoy | Event-based Adaptation Policies for Fractal Components[END_REF] and [START_REF] Dormoy | Using temporal logic for dynamic reconfigurations of components[END_REF].

Our main contribution is the use of FTPL logic for triggering adaptation policies and specifying behaviours of the system under scrutiny. As a practical contribution, we have implemented these more expressive adaptation policies to guide and control dynamic reconfigurations via enforcement and reflection adaptation policies. When a violation of a property is detected, the reflection's purpose is to reconfigure the system to mitigate, if possible, the failure, whereas the enforcement aims to circumvent property violations.

Furthermore, as temporal properties often cannot be evaluated to true or false during the system execution, and so cannot, a fortiori, the extended policies, this paper addresses this question by evaluating at runtime, in a progressive manner, both temporal properties and extended policies. To this end, like in RV-LTL [START_REF] Bauer | Comparing LTL semantics for runtime verification[END_REF], in addition to true and false values, potential true and potential false values are used whenever an observed behaviour has not yet led to an acceptance or a violation of the property under consideration.

Layout of the paper. Section 2 introduces our motivating example, a component model, and its operational semantics, while Section 3 covers a temporal pattern logic over reconfiguration sequences. In Sect. [START_REF] Bauer | Comparing LTL semantics for runtime verification[END_REF], linear temporal patterns are integrated into adaptation policies. The evaluation at runtime of both temporal properties and extended-reflection and enforcement-adaptation policies is presented in Sect. [START_REF] Biere | Bounded model checking[END_REF]. We show that these mechanisms guarantee a system's behaviour allowed by the initial system specification (correctness result). Finally, an implementation allowing the user to deal with the Fractal component model is described in Sect. 6. Section 7 presents our conclusion.

Motivating Example and Background

Component models can be very heteregeneous. Most of them consider software components that can be seen as black boxes (or grey boxes if some of their inner features are visible) having fully described interfaces. Behaviours and interactions are specified using components' definitions and their interfaces. In this section, after introducing a motivating example, we revisit 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]. In general, the system configuration is the specific definition of the elements that define or prescribe what a system is composed of, while a reconfiguration can be seen a transition from a configuration to another. CyCab [START_REF] Baille | The INRIA Rhône-Alpes CyCab[END_REF] or Cristal7 aimed at replacing the private car, are a challenging issue. These distributed and embedded systems require the expression of functional as well as non-functional properties, for example time-constrained response, QoS, and availability of required services.

Location

A positioning system is a critical part of a land transportation system. Many positioning systems have been proposed over the past few years. Among them, we can mention GPS, GALILEO or GLONASS positioning systems which belong to the Global Navigation Satellite Systems (GNSS, for short). Other localisation systems have been designed using various technologies, like Wireless personal networks such as Bluetooth, sensors, GNSS repeaters, or visual landmarks.

Figure 1 gives an abstract view of a composite location component developed within the Fractal component framework. This component includes several positioning systems, like GPS or Wi-Fi, a controller, and a merger. Each positioning system is composed of an atomic positioning component and a software component to validate perceived data. The validation components transfer the positioning data to the merger if they are precise enough. The merger applies a particular algorithm to merge data obtained from positioning systems. Finally, the controller's purpose is to request and to acknowledge the receipt of positioning data.

Moreover, there is a need to make the system's architecture evolve at runtime. Reconfigurations, however, must not happen at any but suitable circumstances. The location composite component architecture can be modified to use, e.g., either GPS, or Wi-Fi, or GPS+Wi-Fi positioning systems, depending on some non-functional properties, such as available energy, and the events from the current indoor/outdoor environment. For example, the following requirement "After the GPS component has been removed, the level of energy has to be greater than 33% before this component is added back" makes use of temporal and architectural constraints to allow the "with GPS" reconfiguration. Then, thanks to adaptation policies, several possible reconfigurations can be determined, and the most suitable reconfiguration can be chosen. For example, when the available energy makes both reconfigurations "with GPS" and "with GPS+Wi-Fi" possible within an adaptation policy, this policy can be used to put system's priorities to the "with GPS+Wi-Fi" reconfiguration, for more reliability.

Configurations. Following [START_REF] Dormoy | Using temporal logic for dynamic reconfigurations of components[END_REF], 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. We also introduce a set CP of configuration propositions on the architectural elements and the relations between them. These properties are specified using first-order logic formulae [START_REF] Hamilton | Logic for mathematicians[END_REF]. The interpretation of functions, relations, and predicates over Elem is done according to basic definitions in [START_REF] Hamilton | Logic for mathematicians[END_REF] and Def. 1.

Definition 1 (Configuration

Let C = {c, c 1 , c 2 , . . .} be a set of configurations. We introduce an interpretation function l : C → CP which gives the largest conjunction of cp ∈ CP evaluated to true on c ∈ C. We say that a configuration c = Elem, Rel satisfies cp ∈ CP , written c |= cp = , when l(c) ⇒ cp. In this case, cp is valid on c. Otherwise, c does not satisfy cp, written c |= cp = ⊥. Among all the configuration propositions, there are constraints common to all the component-based system architectures. They define consistent configurations. For example, two bound interfaces must have the same interface type and their suppliers must be sub-components of the same composite. These consistency constraints are respectively expressed by ∀ ip ∈ P rovidedInts, ir ∈ RequiredInts. (Binding(ip) = ir ⇒ ContainerT ype(ip) = ContainerT ype(ir)), and

∀ ip ∈ P rovidedInts, ir ∈ RequiredInts. Binding(ip) = ir ⇒ ∃ c ∈ Components. (Container(ip), c) ∈ P arent ∧(Container(ir), c) ∈ P arent
The reader interested in consistency constraints is referred to [START_REF] Lanoix | Combining proof and model-checking to validate reconfigurable architectures[END_REF].

Reconfigurations. Reconfigurations make the component-based architecture evolve dynamically. They are combinations of primitive operations such as instantiation/destruction of components; addition/removal of components; binding/unbinding of component interfaces; starting/stopping components; setting parameter values of components. The normal running of different components also changes the architecture, e.g., by modifying parameter values or stopping components. Let R run = R ∪ {run} be a set of evolution operations, where R is a finite set of reconfiguration operations, and run is the name of a generic action used to represent all the running operations of the component-based system.

Definition 2 (Reconfiguration model). The operational semantics of component-based systems with reconfigurations is defined by the labelled transition system

S = C, C 0 , R run , →, l where C = {c, c 1 , c 2 , . . .} is a set of configurations, C 0 ⊆ C is a set of initial configurations, → ⊆ C × R run × C is
σ of S is a sequence of configurations c 0 , c 1 , c 2 , . . . such that ∀i ≥ 0. ∃ ope i ∈ R run .(c i opei → c i+1 ).
We write σ(i) to denote the i-th configuration of σ. The notation σ i denotes the suffix path σ(i), σ(i + 1), . . ., and σ j i denotes the segment path σ(i), σ(i + 1), . . . , σ(j -1), σ(j). Let Σ denote the set of paths, and Σ f (⊆ Σ) the set of finite paths. A configuration c is reachable from c when there is a path

σ = c 0 , c 1 , . . . , c n in Σ f s.t. c = c 0 and c = c n . An execution is a path σ in Σ s.t. σ(0) ∈ C 0 .

FTPL: a Temporal Logic for Dynamic Reconfigurations

In this section, we briefly recall the FTPL logic introduced in [START_REF] Dormoy | Using temporal logic for dynamic reconfigurations of components[END_REF]. Inspired by [START_REF] Bauer | Decentralised LTL monitoring[END_REF][START_REF] Bacchus | Planning for temporally extended goals[END_REF], we present a new progressive semantics for FTPL properties evaluation at runtime, where, unlike [START_REF] Dormoy | Runtime verification of temporal patterns for dynamic reconfigurations of components[END_REF], the evaluation of a trace or temporal property at any given state of a path σ is based on its evaluation at the previous state.

Syntax and Notations

Basically, constraints on the architectural elements and the relations between them are specified as configuration propositions defined in Sect. 2. In addition, the proposed logic contains external events, as well as events from reconfiguration operations, temporal properties, and, finally, trace properties embedded into temporal properties. Let P rop F T P L denote the set of the FTPL formulae obeying the FTPL grammar given below. Let us first give the FTPL syntax. In order to give the semantics for these formulae, we introduce the set B 4 = {⊥, ⊥ p , p , }, where ⊥, stand resp. for false and true values, and ⊥ p , p for potential false and potential true values. As in [START_REF] Bauer | Comparing LTL semantics for runtime verification[END_REF], we consider B 4 together with the truth non-strict ordering relation satisfying ⊥ ⊥ p p . On B 4 we define the unary operation ¬ as ¬⊥ = , ¬⊥ p = p , ¬ p = ⊥ p , ¬ = ⊥, and we define two binary operations , resp. as the minimum and maximum interpreted wrt. . Thus, (B 4 , ) is a finite de Morgan lattice but not a Boolean lattice.

FTPL Basic Semantics

FTPL semantics is basic for events and configuration propositions, and runtimeoriented for other properties. We write σ(i) |= cp to denote the evaluation of the configuration proposition cp in B 4 9 at the i-th configuration of the path σ. External events (like events in [START_REF] Kim | Monitoring, checking, and steering of real-time systems[END_REF]) occur instantaneously and can be seen as invocations of methods performed by (external) sensors when a change is detected in their environment. For each external event ext that may occur on a given execution path σ, we define a) a guard cp ext , which is a first-order logic formula over the parameters specified in the invocation of the method ext, and b) an assertion eval σ , valued in B 2 . Intuitively, if, at or before the i-th and after the i -1-th state (or, if i = 0, at the first state) of an execution path σ, there is at least one occurrence of ext s.t.

cp ext = then eval σ (cp ext , i) = , otherwise eval σ (cp ext , i) = ⊥.
The following definition present FTPL semantics for a) reconfiguration events -"ope normal" (resp. "ope exceptional") when a reconfiguration ope terminates normally (resp. abnormally) or "ope terminates" when ope terminates regardless of its result-, b) external events, and c) lists of events. We write σ(i) |= e to denote the evaluation of the event (resp. list of events) e in B 4 at the i-th configuration of the path σ.

Definition 3 (FTPL Events Semantics).

Let ope be a reconfiguration operation, ext an external event, e an event, and events a list of events.

The interpretation of the events at the i-th state of the path σ is defined by:

σ(i) |= ope normal = if i > 0 ∧ σ(i -1) = σ(i) ∧ σ(i -1) ope → σ(i) ⊥ otherwise. σ(i) |= ope exceptional = if i > 0 ∧ σ(i -1) = σ(i) ∧ σ(i -1) ope → σ(i) ⊥ otherwise. σ(i) |= ope terminates = σ(i) |= ope normal σ(i) |= ope exceptional σ(i) |= ext = evalσ(cpext, i) σ(i) |= e, events = σ(i) |= e σ(i) |= events

FTPL Progressive Semantics

Let σ ∈ Σ be a path. Given an FTPL property from P rop F T P L , its value on σ is given by the interpretation function _ |= _ : Σ × P rop F T P L → B 4 defined below by induction. In order to evaluate, in a progressive fashion, FTPL expressions at runtime, without consulting a complete history of FTPL properties' evaluation (like in [START_REF] Dormoy | Runtime verification of temporal patterns for dynamic reconfigurations of components[END_REF]), we introduce the following notations. Let φ σ = σ |= φ be the evaluation of an FTPL formula where φ is a list of events, a trace property, or a temporal property. We denote φ σ (i) the evaluation of φ on σ, at the i-th state of the path. Furthermore, following [START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF], if the scope of an FTPL property φ is restricted to the suffix path σ k , k ≥ 0, we write φ σ k = σ k |= φ for such a restriction, and φ σ k (i) for the evaluation in B 4 of this restriction at the i-th state of σ, where i ≥ k. Then, the evaluation of φ on the path σ (φ σ = σ |= φ ), is similar to the evaluation of φ on the suffix path σ 0 starting at the first configuration, wich is φ σ0 = σ 0 |= φ . For the sake of simplicity, we also write

cp σ k (i) = σ k (i) |= cp .

Definition 4 (FTPL Runtime Progressive Trace Properties Semantics).

Let cp be a configuration proposition, φ (resp. ϕ) a trace property of the form φ = always cp (resp. ϕ = eventually cp). We define

φ σ k (i) (resp. ϕ σ k (i)), the evaluation in B 4 of σ k |= φ (resp. σ k |= ϕ ) at the i-th state of σ when the scope is restricted to σ k , by: -for i = k, φ σ k (k) = p cp σ (k) ; ϕ σ k (k) = ⊥ p cp σ (k) -for i > k, φ σ k (i) = φ σ k (i -1) cp σ (i) ; ϕ σ k (i) = ϕ σ k (i -1) cp σ (i)
Furthermore, let ψ 1 and ψ 2 be two trace properties, then:

σ k |= ψ1 ∧ ψ2 = σ k |= ψ1 σ k |= ψ2 ; σ k |= ψ1 ∨ ψ2 = σ k |= ψ1 σ k |= ψ2
On the scope starting at the k-th state of σ, if at state k one has cp σ (k) = (resp. cp σ (k) = ⊥), the trace property always cp (resp. eventually cp) is evaluated to p (resp. ⊥ p ); otherwise, it is evaluated to ⊥ (resp. ). Then, for i > k, at the i-th state of σ, always cp (resp. eventually cp) is evaluated to the minimum (resp. maximum), interpreted wrt. , of a) its evaluation at the previous state and b) cp σ (i). Table 1 shows an example of the evaluation of such trace properties.

Table 1. Evaluation of trace properties

Let be φ = always ¬cp and ϕ = eventually cp

i k k + 1 k + 2 k + 3 k + 4 k + 5 k + 6 k + 7 k + 8 • • • cpσ(i) ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ ⊥ • • • φσ k (i) p p p p p ⊥ ⊥ ⊥ ⊥ ⊥ ϕσ k (i) ⊥ p ⊥ p ⊥ p ⊥ p ⊥ p

Definition 5 (FTPL Runtime Progressive Lists of Events Semantics).

Let e be a list of events. We define e σ k (i), the evaluation in B 4 of σ k |= e at the i-th state of σ when the scope is restricted to σ k , by:

-

for i = k, e σ k (k) = σ k (k) |= e -for i > k, e σ k (i) = σ k (i) |= e ( p e σ k (i -1))
Intuitively, the expression σ(i) |= e ( p e σ k (i -1)) evaluates to if there is an occurrence of e at configuration i, and to ⊥ (resp. p ) if there is no occurrence of e at configuration i and no (resp. at least one) occurrence of e happening before configuration i on the scope starting at configuration k.

Definition 6 (FTPL Runtime Progressive Temporal Properties Semantics).

Let tpp be a temporal property, trp a trace property, e a list of events, φ (resp. ϕ, ψ) a temporal property of the form φ = after e tpp (resp. ϕ = before e trp, ψ = trp until e). We define

φ σ k (i) (resp. ϕ σ k (i), ψ σ k (i)), the evaluation in B 4 of σ k |= φ (resp. σ k |= ϕ , σ k |= ψ )
at the i-th state of σ when the scope is restricted to σ k , by: for i ≥ k,

φσ k (i) = j∈I σ i k (e)
tppσ j (i) p where

I σ i k (e) = {j|k ≤ j ≤ i ∧ σ(j) |= e = }
represents the set of indexes for an occurrence of e.

ϕσ k (i) = p if eσ k (i) = ⊥ ∨ i = k ⊥ if eσ k (i) = ∧ trpσ k (i -1) ∈ {⊥, ⊥ p } ϕσ k (i -1) otherwise ψσ k (i) =    p if trpσ k (i) = ⊥ ∧ eσ k (i) = ∧ eσ k (i -1) = ⊥ ∧ trpσ k (i -1) ∈ { p , } ⊥ p if trpσ k (i) = ⊥ ∧ (eσ k (i) = ⊥ ∨ i = k) ⊥ if trpσ k (i) = ⊥ ∨ (eσ k (i) = ∧ trpσ k (i -1) ∈ {⊥, ⊥ p }) ψσ k (i -1) otherwise
By definition, the evaluation of φ = after e tpp is either a) p as long as e does not occur or if tpp is evaluated to p or on each suffix of the path starting at an occurrence of e, or b) ⊥ if on any of these suffixes tpp is evaluated to ⊥, or c) ⊥ p , otherwise.

For ϕ = before e trp, its evaluation is either a) p if e has not occurred yet, or b) ⊥ if for each occurrence of e, trp is evaluated to ⊥ or ⊥ p on the segment starting at the beginning of the considered scope and ending at the previous i -1-th configuration on the σ path. Otherwise, φ at the i-th configuration is evaluated to its value at the previous i -1-th configuration.

Intuitively, the ψ = trp until e property can be seen as being evaluated similarly to before e trp, but with the two following exceptions: a) when trp is evaluated to ⊥, ψ is evaluated to ⊥; otherwise, b) on the beginning part of the scope and as long as e has not occurred, ψ is evaluated to ⊥ p .

Finally, we say that a reconfiguration model S = C, C 0 , R run , →, l satisfies a property φ ∈ P rop

F T P L , written S |= φ, if ∀σ.(σ ∈ Σ(S) ∧ σ(0) ∈ C 0 ⇒ φ σ = ).
Table 2 shows the evaluation of the temporal property φ which is always ⊥ p except on and after the configuration when the event entry occurs until the configuration preceding the occurrence of the event exit where it is p . Note that the event entry occurs at both the j-th and the l-th configurations whereas the evaluation of e = start, exit is at configurations 0 and k, hence φ σ0 (i) = ϕ σ0 (i) for i < k, and φ σ0 (i) = ϕ σ0 (i) ϕ σ k (i) for i ≥ k.

FTPL Expressiveness

We should note that FTPL trace properties are either a) a subset of safety properties, as always cp, or, b) a subset of guarantee properties, as eventually cp, or c) conjunctions and disjunctions of properties from these subsets (safety and guarantee properties). Consequently, according to the safety-progress hierarchy [START_REF] Manna | A hierarchy of temporal properties[END_REF][START_REF] Chang | Characterization of temporal property classes[END_REF], they are included in obligation properties which represent a subset of response properties. In [START_REF] Falcone | Runtime verification of safety-progress properties[END_REF] the issue of enforceable properties, originally Let be e = start, exit, ϕ = p until entry, φ = after start, exit ( p until entry) = after e ϕ i 0 1

• • • j -1 j j + 1 • • • k -1 k k + 1 • • • l -1 l l + 1 • • • σ(i) |= start ⊥ • • • ⊥ ⊥ ⊥ • • • ⊥ ⊥ ⊥ • • • ⊥ ⊥ ⊥ • • • σ(i) |= entry ⊥ ⊥ • • • ⊥ ⊥ • • • ⊥ ⊥ ⊥ • • • ⊥ ⊥ • • • σ(i) |= exit ⊥ ⊥ • • • ⊥ ⊥ ⊥ • • • ⊥ ⊥ • • • ⊥ ⊥ ⊥ • • • σ(i) |= e ⊥ • • • ⊥ ⊥ ⊥ • • • ⊥ ⊥ • • • ⊥ ⊥ ⊥ • • • I σ i 0 (e) {0} {0} • • • {0} {0} {0} • • • {0} {0, k} {0, k} • • • {0, k} {0, k} {0, k} • • • entryσ 0 (i) ⊥ ⊥ • • • ⊥ p • • • p p p • • • p p • • • ϕσ 0 (i) ⊥ p ⊥ p • • • ⊥ p p p • • • p p p • • • p p p • • • entryσ k (i) × × • • • × × × • • • × ⊥ ⊥ • • • ⊥ p • • • ϕσ k (i) × × • • • × × × • • • × ⊥ p ⊥ p • • • ⊥ p p p • • • φσ 0 (i) ⊥ p ⊥ p • • • ⊥ p p p • • • p ⊥ p ⊥ p • • • ⊥ p p p • • •
addressed because of infinite sequences, is extended to finite and infinite properties at runtime. It is then established that enforceable properties are exactly response properties. Hence, FTPL trace properties, as a subset of obligation properties, are enforceable as well. Before ending this section, let us mention (infinite) renewal properties [START_REF] Ligatti | Run-time enforcement of nonsafety policies[END_REF], a superset of safety properties also containing some liveness properties, that can be enforced by edit-automata as runtime monitors. Intuitively, a property is a renewal property if every valid infinite sequence of actions has infinitely many valid prefixes. This is exactly the case of response properties [START_REF] Chang | Characterization of temporal property classes[END_REF]. FTPL trace properties being, as established above, response properties, they are also renewal properties and can then be enforced by edit-automata. Consequently, FTPL temporal properties, acting as scopes [START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF] of trace properties, can also be enforced in the same way.

Integrating Temporal Properties into Adaptation Policies

Although one of the main advantages of reconfigurable component-based systems is the ability of the system's architecture to evolve at runtime, reconfigurations must not happen at any but in suitable circumstances. In order to supervise and to dynamically influence component-based systems reconfigurations, this section introduces adaptation policies indicating reconfigurations suitable to perform, and rules that can impact on the architecture of the component-based system model.

To take into account some resource constraints, events in the system environment, or even properties over sequences of reconfigurations, we propose to extend adaptation policies by integrating FTPL properties into them. For that, adaptation policies exploit the above-mentioned properties and their domains. Each domain defines its specific vocabulary to qualify associated properties, based on the evaluation of the architectural or temporal constraints. Adaptation policies are defined by: a) architectural reconfiguration operations to specify the possible modifications of the architecture; and b) adaptation rules to link the properties concerning the component-based system and the need10 to activate a reconfiguration. We adapt definitions in [START_REF] Chauvel | Composition et expression qualitative de politiques d'adaptation pour les composants Fractal[END_REF][START_REF] Dormoy | Event-based Adaptation Policies for Fractal Components[END_REF] to fit in with our component-based system model semantics, when extending them with temporal properties.

Definition 7 (Adaptation Policies). Let S be a reconfiguration model, and F type a set of fuzzy types. Given σ(i) ∈ C, a finite set AP of adaptation policies for σ(i) is composed of elements

A = R N , R R , where: -R N ⊆ R is a finite (non-empty) set of architectural reconfiguration names, -R R = { F, B,

G, I } is a finite (non-empty) set of adaptation rules, where

• F ∈ F type is a fuzzy type,

• B ⊆ {φ σ (i) = value | φ ∈ P rop F T P L ∧ value ∈ B 4 } is a set of properties in P rop F T P L evaluated in B 4 on σ(i), • G ⊆ {cp σ (i) = value | cp ∈ CP ∧ value ∈ B 2 } is a set of configuration propositions in CP evaluated in B 2 on σ(i), • I ⊆ R N × F is a

relation between reconfigurations and fuzzy values.

Let us denote B σ(i) (resp. G σ(i) ) the conjunction of the properties evaluations in B (resp. guards evaluations in G) on σ(i).

To illustrate adaptation policies with events, let us suppose that the system where the location component is running can dynamically support the removal or the addition of either the GPS and the Wi-Fi components. Of course, at any given time there should be at least one of these components present. In certain cases, however, it can be beneficial to remove one of these components.

For example, when the energy level of the vehicle is low, the Wi-Fi component can be removed, and then added back when the internal batteries are recharged. Furthermore, when the vehicle enters a "Wi-Fi area" where there is no GPS signal available, it is suitable to remove the GPS component, which can be added back after exiting such an area. Figure 3 displays the cycabgps adaptation policy, which is written using a syntax inspired by Tangram4Fractal [START_REF] Chauvel | Composition et expression qualitative de politiques d'adaptation pour les composants Fractal[END_REF] adaptation policies. This policy influences the addgps and removegps reconfigurations to respectively add or remove the GPS component. It uses three events (lines 3 to 5): start (that occurs only when the adaptation policy becomes effective) and entry (resp. exit) that occurs when the vehicle enters (resp. exits) a "Wi-Fi area".

Example 2. For the adaptation policy in Fig. 3, we have the architectural reconfigurations set R N = {addgps, removegps} and F type = {{low, medium, high}} which contains all the fuzzy types used in this policy. For the adaptation rule spanning lines 23 to 25, we have, using the notation of Def. 7, F = {low, medium, high}, B = {after start, exit ( p until entry) = p }, G = {gps ∈ Components ∧ wif i ∈ Components = }, and finally I = {(removegps, high)}. This adaptation rule expresses that when the expression in B holds (i.e., the vehicle is within a "Wi-Fi area" -cf. Table 2 for details of the evaluation), if both the GPS and the Wi-Fi components are present, then the utility of removing the GPS component, by invoking the removegps reconfiguration, is high. Let S = C, C 0 , R run , →, l be a reconfiguration model and AP S a finite set of adaptation policies for S. We now define how the adaptation policies affect the behaviour of the component-based system model.

Definition 8 (Restriction by Adaptation Policies). The restriction of S by adaptation policies in AP

S is defined as S AP S = C AP S , C 0 AP S , R run , →, l , where C AP S is the least set s.t. if c ∈ C and A ∈ AP S then c A ∈ C AP S , R run ∩ (∪ A∈AP S R N ) = ∅, l : C AP S →
CP is a total interpretation function, and for every ope ∈ R run , the transition relation →∈ C AP S × R run × C AP S is the least set of triples (c A, ope, c A) satisfying the following rules:

[ACT1] c ope → c c A ope → c A (ope ∈ A∈AP S RN ) ∧ Bc ∧ Gc [ACT2] c ope → c c A ope → c A ope / ∈ A∈AP S RN
This definition means that all the configurations in C AP S are reachable from initial configurations by either reconfiguration operations obeying adaptation policies (Rule [ACT1]), or by normal reconfigurations which are not involved in the adaptation policy (Rule [ACT2]).

Runtime Policy Evaluation

Given a component-based system and a set of adaptation policies, a problem occurring while applying adaptation policies is to ensure that the reconfigurations (of a component-based system obeying the policies) conform to the specified reconfigurations. More formally, for two component-based systems modelled by S and S AP S , the problem is to decide whether the behaviour of S obeying its adaptation policies in AP S is also a behaviour of S. To address this problem, we propose to use the ready simulation notion [START_REF] Bloom | Bisimulation can't be traced[END_REF].

Definition 9 (Ready Simulation).

Let S 1 and S 2 be two reconfiguration models over R run . A binary relation

⊆ C 1 × C 2 is a ready simulation iff, for all ope in R run , (c 1 , c 2 ) ∈ implies i) Whenever (c 1 , ope, c 1 ) ∈→ 1 , then there exists c 2 ∈ C 2 such that (c 2 , ope, c 2 ) ∈→ 2 and (c 1 , c 2 ) ∈ . ii) Whenever c 1 ope →, then c 2 ope →.
We say that S 1 and S 2 are ready-similar, written

S 1 S 2 , if ∀c 0 1 ∈ C 0 1 ∃c 0 2 ∈ C 0 2 .(c 0 1 , c 0 2 ) ∈ .
Following [START_REF] Bloom | Bisimulation can't be traced[END_REF], we keep the ready-set definition for S as readies(c) = {ope | ope ∈ R run ∧ c ope →}. A useful fact follows immediately from Def. 9: (c 1 , c 2 ) ∈ implies readies(c 1 ) = readies(c 2 ). Consequently, it is enough to show the disequality of the ready-sets to show that the ready simulation does not hold between two configurations.

To be able to establish whether S AP S S or not, and thus to provide a correctness result concerning the restriction by adaptation policies, we consider the following decision problem. Adaptation Problem. Input: Component-based system modelled by S = C, C 0 , R run , →, l , c ∈ C, and the set AP ⊆ AP S of adaptation policies for c. Output: true if ∀A ∈ AP, c A c, and false otherwise.

For the component-based system under its adaptation policies, we define the ready set wrt. Def. 8 by: readies

(c A) = {ope | ope ∈ R run \ ∪ A∈AP R N ∧ c ope → } ∪ {ope | (ope ∈ A∈AP R N ) ∧ B c ∧ G c ∧ c ope →}.
Then, again, it is easy to see that c A c implies readies(c A) = readies(c). Both S and S AP S being infinite state systems, the simulation problem is undecidable in general. However, when the ready sets are different, we can reach a conclusion. Consequently, Proposition 1. The adaptation problem is semi-decidable.

The adaptation policies can be used for specifying reflection or enforcement mechanisms. The notion of reflection means that any unwanted behaviour triggers a corrective reconfiguration through an adaptation policy. The notion of enforcement, exposed in the AdaptEnfor algorithm in Fig. 4, means that no reconfiguration that would lead the system to behave in an unwanted way is allowed. This algorithm uses as inputs 1) a generic component-based system gcbs-an object used to manage a component-based system regardless of the design/development framework, and, 2) an array, v, containing candidate reconfigurations ordered by priority. Each of the variables currentConf , targetConf , and endConf represents a configuration while the variable r designates a reconfiguration 11 .

This algorithm contains five functions: a) retrieveConf(s) returns the configuration of the generic component-based system s; b) size(v) returns the size Finally, there are also five procedures used within this algorithm: a) remove(v,e) removes the element e of the array v; b) applyToSystem(c,s) initiates a reconfiguration of the system s to reach a configuration c; c) sendEvent(r,arg) sends the event "r normal" or "r exceptional", where r is a reconfiguration, and arg stands for "normal" or "exceptional"; d) break exits the current "while" loop; e) systemExit terminates the current run of the program.

Let us add that the way we enforce properties on adaptation policies supports the soundness and transparency principles [START_REF] Ligatti | Edit automata: enforcement mechanisms for run-time security policies[END_REF]. Given a set of properties to enforce at runtime, the mechanism we use is a) sound because it prevents (by not entering in the IF statement's body at line 16) the occurrence of reconfigurations that would lead the system to violate, at the next state of execution, the properties to enforce, b) transparent because it allows (by entering in the IF statement's body at line 16) the occurrence of reconfigurations (if any) that put the system in a state complying with these properties.

The "while" loop starting at line 12 in Fig. 4 ends when the size of the array v becomes equal to 0. Since, on every loop iteration, the size of v is only decremented (line 14), this algorithm always terminates. Proposition 2. The AdaptEnfor algorithm always terminates.

When the AdaptEnfor algorithm terminates with no reconfiguration operation available to be applied to the current configuration, i.e., when the v size becomes equal to 0 in the "while" loop, it means that the set {ope | (ope

∈ A∈AP R N ) ∧ B c ∧ G c ∧ c ope →}(⊆ readies(c A)
) is empty. In this case, as every adaptation policy for c specifies at least one adaptation rule for a reconfiguration operation, the ready sets of c and c A are different. This way the AdaptEnfor algorithm allows answering the adaptation problem with false. Moreover, Theorem 1 (Correctness). If a configuration c is not reachable in S then, for any AP S , it is not reachable in S AP S .

Correctness is clear because when we forget the B and G parts of an adaptation policy A from AP S restricting a behaviour of S AP S , we get a behaviour of S.

Reflection can be applied in a way similar to the enforcement mechanism presented above. The main difference is that, whereas enforcement prevents the occurrence of specific reconfigurations to avoid unwanted behaviours before they actually happen, reflection allows the detection of such behaviours and triggers corrective actions in the form of reconfigurations performed through adaptation policies. Such actions can range up to the total stop of the system in case of the detection of behaviours that would justify it.

Implementation and Case Study

This section describes an implementation developed in Java for the dynamic reconfiguration of component-based systems guided by adaptation policies. A case study shows the result of our experiment on the location component of the CyCab given in Fig. 1.

As shown in Fig. 5, in a nutshell, our implementation uses three controllers: a) the event controller receives events, stores them, and flushes then after they have been sent to a requester, b) the reflection controller sends events to the event controller when a property of a reflection policy is violated, and c) the adaptation policy controller manages reconfigurations, as well as, adaptation and enforcement policies as in the AdaptEnfor algorithm displayed in Fig. 4.

In addition, an event handler is used to receive events from an external source and to send them to the event controller. All interactions with the component-based system (implemented using Fractal in our case) take place through the generic component-based system manager, a set of Java classes developed in such a way that they can be used regardless of the framework used to design the component-based system without modifying its code. The cycabgps (Fig. 3) (resp. cycabwifi) adaptation policy, favours the removal of the GPS (resp. Wi-Fi) component when the energy is low, and favours its addition when the energy level is medium to high. Furthermore, when the CyCab is in a "Wi-Fi area", cycabgps (resp. cycabwifi) favours the removal of the GPS (resp. addition of the Wi-Fi) component.

At configuration 66, the CyCab enters a "Wi-Fi area" having only the GPS component present. The reflection controller, detecting that the vehicle is within a "Wi-Fi area" without the Wi-Fi component, sends, to the event controller, the reflectionNoWifiInWifiArea event. At the next configuration, as a consequence of the retrieval of this event the adaptation policy controller initiates the addwifi reconfiguration which adds and starts the Wi-Fi component. Then, at the following configuration, the application of the cycabgps adaptation policy (Fig. 3) by the adaptation policy controller causes the removal of the GPS component through the removegps reconfiguration. At configuration 134, the CyCab enters a "Wi-Fi area" having only the Wi-Fi component present. When the level of energy becomes high (configuration 142), in application of cycabgps, the GPS component is not added. As soon as the vehicle exits the "Wi-Fi area" (configuration 79 and 148), since the level of energy is high, the GPS component is added back.

Outside of a "Wi-Fi area", the Wi-Fi (resp. GPS) component is removed at configurations 15, 64, 89, and 159 (resp. 37 and 130), as a result of the application of adaptation policies, because the level of energy becomes low. Still outside of a "Wi-Fi area", when there is only one component present (among the Wi-Fi and GPS components), the other is added when the level of energy is medium to high (configurations 24, 50, 79, 99, 148, and 167).

These experimental results show that extending adaptation policies with temporal patterns provides the specifier with means allowing to better -in comparison with [START_REF] Chauvel | Composition et expression qualitative de politiques d'adaptation pour les composants Fractal[END_REF][START_REF] Gonnord | Quantity of resource properties expression and runtime assurance for embedded systems[END_REF][START_REF] Dormoy | Event-based Adaptation Policies for Fractal Components[END_REF] -comprehend and control the component-based sys-tem's behaviour. Because the frequency at which adaptation occurs depends on the system under scrutiny, this parameter must be specified as a user-defined para-meter. In a future development it will be possible to specify that adaptation needs to happen in some bounded time.

Of course, it should be possible to come up with a finite encoding of the bounded version of our example to use techniques for finite state systems. Our point, however, is to evaluate temporal and architectural constraints over changeable architectures at runtime. One can imagine new components, not even implemented at the beginning of the run, to be added at execution time. This, indeed, can lead to infinite behaviours.

Related Work and Conclusion

Related work

The analysis of systems whose topology evolves over time is a challenging topic. Tangram4Fractal [START_REF] Chauvel | Composition et expression qualitative de politiques d'adaptation pour les composants Fractal[END_REF] presents a qualitative approach of adaptation policies, but disallow the use of temporal properties. The work in [START_REF] Dormoy | Event-based Adaptation Policies for Fractal Components[END_REF] shows an evolution of Tangram4Fractal that permits adaptation policies based on a qMEDL logic [START_REF] Gonnord | Quantity of resource properties expression and runtime assurance for embedded systems[END_REF] to use external events. Architectural constraints, however, cannot be expressed with qMEDL.

The FTPL logic, expressing temporal and architectural constraints, is introduced in [START_REF] Dormoy | Using temporal logic for dynamic reconfigurations of components[END_REF]. It is based on Dwyer's work on patterns and scopes [START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF] and uses specifications inspired by [START_REF] Trentelman | Extending jml specifications with temporal logic[END_REF]. Nevertheless, this version of FTPL does not support external events and cannot always be evaluated at runtime.

Like Bounded Model Checking [START_REF] Biere | Bounded model checking[END_REF] (BMC for short), our approach may produce counterexamples when detecting property violation. Moreover, when no violation is detected, both approaches are incomplete for the safety properties. However, for some liveness properties, for example eventually, the satisfaction can be established. It is also possible to establish the satisfaction of some safety properties within the appropriate scope [START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF][START_REF] Trentelman | Extending jml specifications with temporal logic[END_REF]. Similar to [START_REF] Lanoix | Combining proof and model-checking to validate reconfigurable architectures[END_REF] using BMC, we can validate architectural or temporal properties over instantiated reconfigurable systems; this validation is size-bounded and partial.

Evaluation of FTPL properties at runtime is detailed in [START_REF] Dormoy | Runtime verification of temporal patterns for dynamic reconfigurations of components[END_REF]. This version of FTPL, however, does not support the use of external events. Furthermore, to allow easier runtime evaluation, we use a progressive semantics inspired by [START_REF] Bauer | Decentralised LTL monitoring[END_REF][START_REF] Bacchus | Planning for temporally extended goals[END_REF]. This semantics, unlike the one in [START_REF] Dormoy | Runtime verification of temporal patterns for dynamic reconfigurations of components[END_REF], takes fully into account the usage of scopes [START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF][START_REF] Trentelman | Extending jml specifications with temporal logic[END_REF] Our implementation for handling reflection is somehow similar to the steering performed with the MaCS framework in [START_REF] Kim | Monitoring, checking, and steering of real-time systems[END_REF]. The coupled PEDL and MEDL scripts act as the event and adaptation controllers in our implementation while the SADL script acts as our reflection controller. No enforcement is provided in MaCS.

In [START_REF] Falcone | Runtime verification of component-based systems[END_REF], only runtime verification is performed; there is no adaptation mechanism. Nevertheless, by using locations spanning over several components, the specifications considered for BIP systems allow, similar to our approach, describing global behaviours of the system. Dissimilar to our approach where the code of the component-based system under scrutiny is not modified, RV-BIP slightly modifies components and thus may not allow the component reusability; in this case, the separation of concerns principle would not be respected.

The work in [START_REF] Kähkönen | The lime interface specification language and runtime monitoring tool[END_REF] allows runtime monitoring of temporal properties for component interfaces. When components come with an abstract behavioural model, they can be considered as grey boxes rather than black boxes. Our approach, not limited to monitoring interactions of component interfaces with an external application, works in both cases.

Conclusion

As component-based systems evolve at runtime, and as a behaviour in which the runtime temporal property evaluation becomes false might be not acceptable, this paper has proposed to integrate temporal properties into adaptation policies, and to supervise-at runtime-the reconfiguration execution allowed by the adaptation policies. Inspired by proposals in [START_REF] Bauer | Comparing LTL semantics for runtime verification[END_REF], this paper continues with a fourvalued logic allowing to characterize the "potential" properties (un)satisfiability. In addition, the four-valued logic helps in guiding the reconfiguration process, namely in choosing the next reconfiguration operation to be applied. A prototype Java implementation of the algorithm for verifying and enforcing FTPL properties integrated into the adaptation policies has been developed, as a proof of concept.

As a future work, we plan to investigate a decentralized method to evaluate adaptation policies and temporal formulae by progression, as in [START_REF] Bauer | Decentralised LTL monitoring[END_REF]. On the implementation side, a future direction is to handle component-based systems using the FraSCAti [START_REF] Seinturier | A component-based middleware platform for reconfigurable service-oriented architectures[END_REF] framework.

Fig. 1 .

 1 Fig. 1. The location component in Fractal

Fig. 2 .

 2 Fig. 2. Configuration of the example of Fig. 1

  the reconfiguration relation, and l : C → CP is a total interpretation function. Let us note c ope → c for (c, ope, c ) ∈→, and c ope → when there is a target configuration c such that c ope → c . Given the model S = C, C 0 , R run , →, l , an evolution path (or a path for short)

  <FTPL> ::= <tpp> | <events> | cp <tpp> ::= after <events><tpp> | before <events><trp> | <trp> until <events> | <trp> <trp> ::= always cp | eventually cp | <trp> ∧ <trp> | <trp> ∨ <trp> <events> ::= <event>,<events> | <event> <event> ::= ope normal | ope exceptional | ope terminates | ext

Fig. 3 .

 3 Fig. 3. cycabgps adaptation policy

Fig. 4 .

 4 Fig. 4. Algorithm AdaptEnfor

  ). A configuration c is a tuple Elem, Rel where

	Components	= {controller, gps, location, merger, wif i}
	P rovidedInts = {gpsP osition, mergeP osition, position, secureP osition, wif iP osition}
	RequiredInts = {getGpsP osition, getM ergeP osition, getW if iP osition}
	P arameters	= {GpsP owerU sage, P ower, T rust, W if iP owerU sage}
	T ypes	= {M ergeP osition, P osition, SecureP osition, int}
	Container	= {gpsP osition → gps, mergeP osition → merger, position → controller,
		secureP osition → location, wif iP osition → wif i,
		getGpsP osition → merger, getM ergeP osition → controller,
		getW if iP osition → merger, GpsP owerU sage → merger,
		P ower → controller, T rust → merger, W if iP owerU sage → merger}
	ContainerT ype = {getGpsP osition → P osition, getM ergeP osition → M ergeP osition,
		getW if iP osition → P osition, gpsP osition → P osition,
		mergeP osition → M ergeP osition, position → SecureP osition,
		secureP osition → SecureP osition, wif iP osition → P osition, T rust → int,
		GpsP owerU sage → int, P ower → int, W if iP owerU sage → int}
	Contingency	= {getGpsP osition → optional, getM ergeP osition → mandatory,
	-Elem = Components getW if iP osition → optional} Interf aces P arent = {(controller, location), (gps, location), (merger, location), (wif i, location)} P arameters T ypes is a set of
	Binding architectural elements, such that = {gpsP osition → getGpsP osition, mergeP osition → getM ergeP osition, wif iP osition → getW if iP osition}
	Delegate	= {position → secureP osition}
	State	= {controller → started, gps → started, location → started, merger → started,
		wif i → started}
	V alue	= {GpsP owerU sage → 3, P ower → 95, T rust → 0, W if iP owerU sage → 2}
	-Rel =	Container P arent	ContainerT ype Binding Delegate Contingency State	V alue
	is a set of architectural relations which link architectural elements, such that
	• Container : Interf aces P arameters → Components is a total func-
	tion giving the component which supplies the considered interface or the
	component of a considered parameter;
	• ContainerT ype : Interf aces P arameters → T ypes is a total func-
	tion that associates a type to each (required or provided) interface and to
	each parameter;
	• Contingency : RequiredInts → {mandatory, optional} is a total func-
	tion indicating whether each required interface is mandatory or optional;
	• P arent ⊆ Components × Components is a relation linking a sub-
	component to the corresponding composite component 8 ;
	• Binding : P rovidedInts → RequiredInts is a partial function which
	binds together a provided interface and a required one;
	• Delegate : Interf aces → Interf aces is a partial function to express
	delegation links;
	• State : Components → {started, stopped} is a total function giving the
	status of instantiated components;
	• V alue : P arameters → {t|t ∈ P T ype} is a total function which gives
	the current value of each parameter.
	Example 1. To illustrate our model, the example of Fig. 1 is described in Fig. 2.

• Components is a non-empty set of the core entities, i.e components; • Interf aces = RequiredInts P rovidedInts is a finite set of the (required and provided) interfaces; • P arameters is a finite set of component parameters; • T ypes = IT ypes P T ypes is a finite set of the interface types and the parameter data types;

Table 2 .

 2 Detail of the evaluation of "after start, exit ( p until entry)"

qMEDL is a flavor of MEDL used to express quantity of resource properties.

FTPL stands for TPL (Temporal Pattern Language) prefixed by 'F' to denote its relation to Fractal-like components and to first-order integrity constraints over them.

http://www.projet-cristal.net/

For any (p, q) ∈ P arent, we say that q has a sub-component p, i.e. p is a child of q. Shared components (sub-components of multiple enclosing composite components) can have more than one parent.

Since B2 ⊂ B4, the evaluation c |= cp of the configuration proposition cp ∈ CP on the configuration c detailed on p. 5 is considered to be valued in B4.

As in[START_REF] Chauvel | Composition et expression qualitative de politiques d'adaptation pour les composants Fractal[END_REF][START_REF] Dormoy | Event-based Adaptation Policies for Fractal Components[END_REF], we use a fuzzy value (e.g.; in {low, medium, high}) to express this need.

In AdaptEnfor Algorithm, ≡ can be implemented by various (pre-)congruence relations-set equality for Elem and Rel in Def. 1, structural refinement in[START_REF] Dormoy | When structural refinement of components keeps temporal properties over reconfigurations[END_REF], or other relations compatible with the reconfiguration relation.

This work has been partially funded by the Labex ACTION, ANR-11-LABX-01-01. 3 http://fractal.objectweb.org/julia/index.html 4 http://gridcomp.ercim.org/

Since we want our implementation to be independent of a particular component-based framework, only a few classes implementing Java interfaces of the generic componentbased system manager use API specific to the componentbased system framework. This way, the controllers of Fig. 5 not being Fractal-based, our implementation can manage various component-based frameworks. The synchronization between adaptation policy and reflection controllers coupled with the way events are managed allows the controllers to operate together under the perfect synchrony hypothesis [START_REF] Jantsch | Modeling Embedded Systems and SoC's: Concurrency and Time in Models of Computation[END_REF].

When running the implementation, each reconfiguration is simulated (cf. line 15 of the AdaptEnfor algorithm, Fig. 4), starting with the ones with higher priority. The first one which does not violate any property from an enforcement policy is applied (lines 16 and 17). If the reconfiguration ends normally the event "r normal" (line 20), where r is the name of the above-mentioned reconfiguration, is sent to the event controller. If the reconfiguration ends with an error, the previous configuration is rolled back and the event "r exceptional" (line 26) is sent to the event controller. Events sent by the reflection controller to the event controller are caught by the adaptation policy controller that apply corrective actions using appropriate adaptation policies.

Figure 6 provides the results obtained by running our implementation with the location component of the CyCab given in Fig. 1. The top chart illustrates the evolution of the energy level, while the middle (resp. bottom) chart shows the presence (value 1) or the absence (value 0) of the GPS (resp. Wi-Fi) components. Note that the rate of energy consumption is related to the presence or absence of the GPS and Wi-Fi component. When the vehicle enters (resp. exits) a "Wi-Fi area", the event entry (resp. exit) is sent to the event controller, as shown by vertical segments on Fig. 6 at configurations 66 and 134 (resp. 78 and 147).

When the energy level goes below 10, a reflection policy triggers a reconfiguration (chargeBattery) that has the effect to update the energy level to 100. Just before configuration 100, a Fractal API has been used to artificially set the energy level to a negative value, this triggers (through a reflection policy) the reconfigurations stopCycab and chargeBattery that respectively stop the location composite component and update the energy level to 100. The location composite component being stopped, the energy level does not decrease until configuration 116 when it is restarted.


Mesaac Makpangou

Bassirou Ngom

Samba Ndiaye

Friticores: A RSS Feed Monitoring and Dissemination System

Keywords: RSS feed, content indexing, over-dht index, keyword-based search

RSS feeds is a simple information medium that permits to reduce the information discovery delay. It requires some effort to consumers to find suitable information especially if they ignore providers that could provide it. Providers that lack an established reputation are marginalized by users. This paper presents Friticores, a RSS feed monitoring and dissemination system that addresses both issues. With respect to providers, it stands as a dissemination system that makes each information update visible to all interested users. With respect to consumers, Friticores extends the traditional RSS feed service with filtering service and virtual feeds. The key contributions presented comprise the architecture of the system and the services offered to both consumers and providers, a partitioned persistent representation of feeds, and a distributed index scheme. As for the status of the work, the design is complete and the development of a simulation prototype is ongoing.

Introduction

With the development of web 1.0 and web 2.0 applications (e.g., e-store, blogs, social networks, wikis and mashups) Internet users who were passive consumers became content providers. Nowadays, number of users are interested in discovering without delay new updates from their favorite providers. RSS feeds allow contents providers to publish announcements of new information updates available at their sites; then users interested in receiving announcements from a particular provider, subscribe to his feed. Once subscribed to a feed, they receive all announcements that flow through that feed. Hence, RSS feeds provide a simple information dissemination mechanism that permits to reduce the delay between the occurrence of a new content and its discovery by interested users.

While this mechanism is a good match for consumers interested in contents from a few providers, it is less convenient for users interested in a large number of providers. Consider for instance a researcher interested in new scientific publications covering his research topics. A priori, one affordable solution is to subscribe to feeds provided by leading research groups, organizations supporting major conferences and journals of his domain, universities and research institutes, and major digital libraries. However these providers produce or distribute contents that concern the particular topics of this researcher and many others. Hence, this researcher needs support to filter out relevant information from the huge volume of received updates.A number of filtering facilities [START_REF] Ying | A Self-Organizing Search Engine for RSS Syndicated Web Contents[END_REF][START_REF] Yuan | Sensing Semantics of RSS Feeds by Fuzzy Matchmaking[END_REF][START_REF] Tomàs | RoSeS: a continuous contentbased query engine for RSS feeds[END_REF] already exist. One limitation for these solutions is bandwidth consumption: users still have to retrieve useless updates. For users with limited resources, wasting bandwidth to download useless updates might be an issue. Another problem that faces feeds users is the the difficulty to find all suitable feeds that treat their favorite subjects. Search engines such as syndic8 [START_REF][END_REF] allow users to find relevant feeds that match their requirements. However, these engines rely on static descriptions of existing feeds. Unfortunately, the actual contents provided over time by a provider often diverge from the initial static description of his feed. Such mismatch might lead to poor quality of service for search engines exploiting static descriptions of feeds. Beside, a continuous monitoring by users themselves would be too expensive in term of time, bandwidth, storage and processing.

On the provider's side, the main issue is the lack of visibility and reputation for certain providers. Consider for instance the case of the universities and research laboratories in Africa whose the quality of research are ignored by many users. This lack of visibility prevents users to subscribe to their feeds. The consequence is that the feeds will be released in a limited way, and the content posted by these sites will have limited impact. Moreover, the maintenance requires a significant investment to provide an acceptable quality of service. Insecurity, limited resources available, and the low impact of RSS on the universities's reputation lead them to sacrifice the RSS using and perpetuate the marginalization of the content of these universities. For such a universities, we need a dissemination system that gives them a fair chance to let interested users discover their publications, while devoting a minimum of resources to this service. A P2P network for the dissemination of RSS feeds to RSS users is proposed in [START_REF] Sandler | FeedTree: sharing web micronews with peer-to-peer event notification[END_REF][START_REF] Jun | FeedEx: collaborative exchange of news feeds[END_REF]. While this proposal balance the access load over participating servers, it does not help users discover relevant information, regardless their providers.

In this paper we propose Friticores, a RSS Feed Monitoring and Dissemination System designed to help researchers from underdeveloped Countries. Friticores allows a user to subscribe and to be notified in real-time when updates that match his subscriptions are available. Our scheme is based on a set of peers that collaborate to retrieve and disseminate RSS feeds. First, the system stands as a content-based publish/subscription system for RSS feeds that eliminates the provider's burden, that filters content before sending it to users who can set the content in which they wish to subscribe. Second, it consists of a keyword-based information retrieval system that permits users to catch up missed updates and to discover new feeds that concern their desired contents. This gives a fair chance to each provider to have his updates notified to all interested subscribers.

The main contribution of the paper is three-fold. First, a simple partitioned representation of RSS feeds that permits to efficiently store and retrieve feeds within a structured peer-to-peer storage network. A feed is represented as a set of immutable data, plus a list of keys that can only extend. Second, an index scheme that permits to offer to users keyword-based queries and subscriptions. This scheme relies on Bloom filter [START_REF] Bloom | Space/time trade-offs in hash coding with allowable errors[END_REF] to enforce a compact encoding of keyword sets as well as efficient matching operations. Third the system proposes a number of novel services and implements an architecture that permits to achieve them.

The rest of the paper are organized as follows. Section 2 discusses relate work. Section 3 presents the overview of the system, then Section 4 details some key aspects of the system. Finally, Section 5 points some future work and concludes the paper.

Related Work

Many proposed mechanisms [START_REF] He | Bloom filter-based keyword search over XML data in structured Peer-to-Peer systems[END_REF][START_REF] Bonifati | XPath lookup queries in P2P networks[END_REF][START_REF] Koloniari | Content-based routing of path queries in Peer-to-Peer systems[END_REF][START_REF] Jamard | Indexing textual XML in P2P networks using distributed bloom filters[END_REF][START_REF] Xiaochuan | A Time/Space Efficient XML Filtering System for Mobile Environment[END_REF] exploit XML document structure to handle complex and semantic queries expressed with XPath language. Our work differs from these proposals in that we consider keyword-based queries. Our work is more closely related to indexing schemes in P2P systems and to RSS feed filtering and dissemination systems.

Indexing Schemes

Distributed Bloom Filter. Jamard et al [START_REF] Jamard | Indexing textual XML in P2P networks using distributed bloom filters[END_REF] index XML documents and paths by introducing Distributed Bloom Filters (DBF). Bloom filters are divided into segments of equal size and segments are distributed in the network. Segments with a high probability of false positive are replaced by larger segments. For each segment number i, there exists a controller node responsible on which all i th segments are stored. Bloom filters are associated with topics and a shared catalog lists all available topics. Query processing takes place in three phases: the first step accesses all controllers that are responsible for a segment; the second step contacts peer servers; and the final step eliminates false positives. Additional maintenance such as segment replacement and shared catalog update introduce index overhead. Moreover the index depends on a hight availability of the node controller since it is the responsible of all i th segments and its failure breaks all the system. Our system splits content keys into chunks, in the same way Bloom filters are decomposed here into segments. One difference is that we intend to use our index to perform broad semantic matchings.

Prefix Tries Indexes. Data search on DHTs is made deterministically. To support complex queries, many over-DHT indexes have been proposed 3 . PHT [START_REF] Sriram | Brief Announcement: Prefix Hash Tree[END_REF] is an index structure that uses a prefix tree built over a DHT. Nodes are identified by a D-bit prefix. PHT stores objects at the tree leaf nodes. The trie structure is distributed over the same structured P2P storage system as the indexed contents. PHT maintains a double list that connects all leaf nodes and supports object insertion and deletion. A leaf node that already stores more than B objects must be split before inserting a new key. One challenging issue with PHT is performance, especially if one has to split nodes very often.

Tang et al propose LIGHT [START_REF] Tang | LIGHT: A Query-Efficient Yet Low-Maintenance Indexing Scheme over DHTs[END_REF] to improve over-DHT indexes performance. LIGHT is also based on prefix tree and consists of a trie structure, a data structure called "leaf bucket" and a naming function. When LIGHT split a node, it keeps the half data on the local node (split node), while the remaining half is transferred to the remote node. Given a key, LIGHT-lookup returns the corresponding DHT-key. For this, the label of the "leaf bucket" that covers the key must be found, then applying the naming function allows to get data DHT-key. LIGHT consumes less bandwidth than PHT.

However, PHT and LIGHT indexes yield low performance when performing an inexact query search (such as matching keyword queries) since its search mechanism uses key prefix which yields poor performance for a content-based routing scheme.

Inverted list indexes. An inverted list is a set of pairs (w, O), where w is a keyword, and O is the set of objects containing that keyword. A keyword search method in a P2P networks can use a distributed index based on the inverted list [START_REF] Gnawali | A Keyword Set Search System for Peer-to-Peer Networks[END_REF][START_REF] Reynolds | Efficient peer-to-peer keyword searching[END_REF]. The naive approach is to distribute the entire structure in the network so that each keyword is assigned to a node that indexes objects having this keyword. This naive approach has a number of drawbacks: high bandwidth consumption, uneven load of nodes, redundant storage of popular keywords, and the weak filtering of information when querying with popular keywords.

Wang et al [START_REF] Wang | Multi-keyword search over P2P based on Counting Bloom Filter[END_REF] use counting Bloom Filter to resolve "AND" and "OR" queries in P2P networks. Intermediate results intersection are avoided while satisfying a multiple keywords based query. A node that receives an "AND" query sends its filter to the other nodes having the query keywords. Each node does locally the intersection with its local filter and return the result. The requesting node performs locally received results and returns the response. A node that receives an "OR" query sends its local stored keywords that matches the query to the requesting node at the same time it sends the filter to other nodes, once a node receive the filter, it makes the difference between its local keywords and all received keywords, then it returns the result directly to the requesting node.

A survey of solutions that improve the naive inverted list solution can be found in [START_REF] Risson | Survey of research towards robust peer-to-peer networks: search methods[END_REF][START_REF] Passarella | Review: A survey on content-centric technologies for the current Internet: CDN and P2P solutions[END_REF].

Hypercube-based Index Joung et al [START_REF] Joung | Keyword Search in DHT-Based Peer-to-Peer Networks[END_REF] addresses a number of drawbacks inherent to the use of keyword inverted lists. They propose to rely on a r-dimension hypercube H r (V, E) to build the index. Two types of searches can be performed: pin search and superset search. A pin search find the sets of entries for a given set of keywords. A superset search aims to return a set of objects that can describe a given keyword set. Superset search is conducted with a spanning tree. Browsing that tree allows to find all supersets describing the keyword set. Superset search is expensive since several nodes can be visited unnecessarily, this increases the number of messages if the query contains few keywords. To eliminate these problems, Szekeres et al [START_REF] Szekeres | A keyword search algorithm for structured peer-to-peer networks[END_REF] propose indexing and searching algorithms based on ad-hoc spanning trees. They construct paths from object's keyword-set to all the subsets of this keyword-set. Keywords are lexicographically ordered. However this requirement is not easily feasible in a content retrieval system where users use different writing style.

RSS Feeds Filtering and Dissemination

Zhou et al propose SoSpace [START_REF] Ying | A Self-Organizing Search Engine for RSS Syndicated Web Contents[END_REF] a search engine for RSS feeds. A node in SoSpace can either be a provider or a RSS aggregator. In addition to the feeds, Each node keeps both the RSS feeds and an inverted list of all the terms that appear on them. An item in a RSS feed is treated by SoSpace as a document. The query processing follows three steps: initially the requesting node sends messages to nodes responsible for the query terms asking posting list or bloom filter of each term, then the requesting node collects and combines responses and finally the requesting node gets the documents description.

Weixiong et al [START_REF] Rao | A distributed full-text top-k document dissemination system in distributed hash tables[END_REF] allow users to subscribe to their favorite content using keywords. The system consists of a service of RSS feeds aggregation and a services of feeds distribution which send the most k relevant feeds to the user. A user registers its keywords-based subscriptions (query or filter) on the alert agent which creates an URL for him. The user periodically polls the URL as in the actual case. The relevance between a document and a query is based on "rendezvous" of terms. If a node responsible of a document term receives a document, it forwards it to all registered alert agent. Each alert agent maintains a set of k documents candidates. Techniques such as terms selection and documents pruning are used to increase the performance.

Our proposal differs from these two solutions mainly on the indexing scheme. They rely inverted list (or equivalent scheme) while we implements an over-dht index.

Friticores Overview

Friticores is a feed monitoring and dissemination system. A feed is statically characterized by its location and a description of information that it provides. From a dynamic point of view, a feed models a continuous flow of resource's advertisements (called items). Each item comprises: a title, the summary of the advertised resource, the URL where one can access this resource. We assume that both feeds' descriptions and items summaries are given as sets of keywords. 4Friticores provides to its users four basic services.

-registerFeed(FeedLocation url, FeedDescription desc); -publishItems(FeedLocation url, ItemList items); -ItemRefList search(FeedLocation url, Set<Keyword> keywords); subscribe(FeedLocation url, Set<Keyword> keywords);

To providers the possibility to register feeds and to publish items; to consumers, the possibility to receive items published within a particular feed or related to a particular topic (the feed location is set to null); consumers can either formulate queries or subscribe for asynchronous notifications of suitable items when available. To request a topic-based query or subscription, one simply specifies a null URL as feed location.

The system is structured in three layers. Figure ?? shows the main components of the system and how they interact with one another. The top layer implements the system API while the lowest layer is the storage system. The intermediary layer comprises the components that implement the services offered to users. These include the feed store (FS), the feed search engine (FSE), and the subscription management system (sms). The fourth component is used by other components to achieve their service.

FS component implements primitives offered to providers: registerFeed() that permits to store feeds' descriptions andpublishItems() which is used to publish information updates (or items). The FS component provides an additional primitive that permits to retrieve items (or updates) published at a feed. FS stores feeds' descriptions and updates in the underlying DHT-based storage overlay network. FS cooperates with distributed index component to index stored feeds.

The feed search engine component solves each query and returns feeds or items that meet the query criteria to the requester. FSE relies on the Index component to determine the feeds that match the query criteria.

The subscription management component manages users' subscriptions. One virtual feed is associated with each subscription. The heart of this component is a scheduler that repeats periodically, for each virtual feed, the corresponding query to the FSE component; returned feeds are notified to subscribers.

The distributed index component maintains the index structure over the DHT-based storage system. It hides detailed representation of the index to other companion components. It provides them two basic primitives: one permits to add new keys in the index, and the other permits to lookup keys of contents that match the query criteria.

System Functioning

This section describes the details some key points of the system, in particular the system api, partitioned representation of feeds, and the index scheme.

System Api

Users post their demands (queries or subscriptions) through Users' Agents (UA). A demand can be a url-based/topic-based subscription or query.

Url-based subscriptions permit users to obtain the current functioning of RSS. Users may specify a keyword-based filter such as to prevent notifications of unsuitable feeds.

When an user wants to do an foresight on a given topic, he can not subscribe to all providers that treat the topic. The UA component allows him to post a set of keywords that describes the desired topic. We call such subscriptions topic-based subscriptions.

For each subscription (topic-based or url-based), the UA creates a virtual feed composed by all items matching the subscription. When a new item matches a virtual feed description, his subscriber will be notified.

If an user wants to find existing items, he posts a query request rather than a subscription. Again, the system supports both url-based and topic-based queries.

The difference between a subscription and a query is that the former is a lasting query while the latter is an instantaneous search.

UAs rely on the underlying Search Engine to handle queries and on the subscription management system to handle subscriptions.

On the providers' side, crawlers monitor the web and register new feeds. They are also responsible of monitoring information updates and to publish them.

Partitioned Representations of Feeds

We use Bloom filter to code feeds' descriptions and updates' summaries as well.

We partition the sequence of items published by a feed according to their publication date. We define a sub-feed as a set of items published at the same date by the same feed; it may contain any number of items. We associate to each sub-feed an identifier that distinguishes it from other sub-feeds of the same feed, and the union Bloom filter of Bloom filters characterizing its contained items.

Each sub-feed is stored within the storage network using its characteristic Bloom filter as key. To represent the whole feed, we store an object that contains the keys that identify its subfields. We use the feed Bloom filter as the global feed object's key.

Overall, the persistent representation of a feed is one feed object and a set of item containers (one per sub-feed).

Friticores Index Scheme

The propose index scheme is designed specially to solve matching requests sent by the users agents or by the subscription management system. It ensures the broad semantic matching of received keyword-based queries against stored objects represented by their descriptions given as a keyword set.

The baseline of our solution is three-fold. Firstly, we build an index of Bloom filters used as storage keys to store feeds and sub-feeds. Secondly, given a set of keywords that define a query, we compute the Bloom filter corresponding to these keywords,relying on the same set of hash functions that were used to compute the Bloom filters used as storage keys. Finally to locate items that match a query, we search for indexed keys that match the query Bloom filter. The matched keys are then used to retrieve suitable feeds.

Bloom filter matching operation, per say, is simple and efficient. The issue here is to build a distributed key index, stored on the DHT and which supports efficiently the matching process (which can be viewed as a form of complex query). A number of existing solutions to support complex queries rely on PHT [START_REF] Sriram | Brief Announcement: Prefix Hash Tree[END_REF] or on hypercube [START_REF] Joung | Keyword Search in DHT-Based Peer-to-Peer Networks[END_REF]. We have considered using these data structure; however, it turns out that they did not fit well for our case. In particular, our Bloom filters are bitmaps of large size. Using a PHT or an hypercube-like structure to represent our index yield poor performance for the matching operation.

The solution we have adopted is to split each key of size m into k chunks and to assign a common unique group identifier g i to all chunks of the same key. Each chunk is characterized by its position pos (from 0 to k -1) and its value bf (a substring of the initial Bloom filter). We index chunks instead of entire keys. Each posting in the index structure is then a 3-tuple (< bf, position, g i >). A chunk (< bf, position, g i >) is stored using bf as key. To lookup contents that match a wry, we follow the same process:(i) computation of the Bloom filter that characterizes this request; (ii) splitting this filter in chunks relying on the splitting algorithm; (iii) lookup individual chunks; (iv) merge different returned chunks to reconstitute matched contents keys.

The detailed description of the index structure and of the add and lookup protocols are out of the scope of this paper. One can easily convince himself that chunks of different positions and possibly from different keys could have the same storage key. Hence the chunk index structure and the lookup require careful design.

Conclusion

We have presented Friticores, a RSS feed monitoring and Dissemination system. Friticores is primary destined to feed users (consumers and providers) with limited resources or willing to avoid wasting of resources. Friticores also aims to give each provider a fair chance to improve its visibility with respect to users that could be interested in his publications, thanks to the provision of topic-based queries and subscriptions. We highlighted the a partitioned representation of feeds that eases feed storage within a dht-based storage system, and our index scheme that permits efficient matching of keyword-based queries against feeds' descriptions. We detailed the system architecture and how components interact to achieve both novel and the traditional feed services.

We are implementing a simulation prototype in oder to evaluate Fritcores performances. In a near future, we plain to setup a monitoring system such as to collect real data that will be used to defined a benchmark for our evaluation.

Fig. 1 .

 1 Fig. 1. Friticores architecture

A detailed survey of complex query supports in DHT based P2P systems can be found in[START_REF] Hidalgo | Towards an Efficient Support for Complex Queries on Structured Peer-to-Peer Networks[END_REF]

If this were not the case, number of tools exist that can help extract keywords from full text.