Yliès Falcone

Mohamad Jaber

Thanh-Hung Nguyen

Marius Bozga

Saddek Bensalem

Runtime Verification of Component-based Systems

Verification of component-based systems still suffers from limitations such as state space explosion since a large number of different components may interact in an heterogeneous environment. Those limitations entail the need for complementary verification methods such as runtime verification based on dynamic analysis and prone to scalability. In this paper, we integrate runtime verification into the BIP (Behavior, Interaction, and Priority) framework. BIP is a powerful component-based framework for the construction of heterogeneous systems. Our method augments BIP systems with monitors checking a user-provided specification. This method has been implemented in RV-BIP, a prototype tool that we used to validate the whole approach on a robotic application.

Introduction

A component-based approach consists in building complex systems by composing components (building blocks). This confers numerous advantages (e.g., productivity, incremental construction, compositionality) that allow to deal with complexity in the construction phase. Component-based systems (CBS) are desirable because they allow reuse of sub-systems as well as their incremental modification without requiring global changes. Their development requires methods and tools supporting a concept of architecture which characterizes the coordination between components. An architecture structures a system and involves components and relationships between the externally visible properties of those components. The global behavior of a system can, in principle, be inferred from the behavior of its components and its architecture. Componentbased design is based on the separation between coordination and computation. Systems are built from units processing sequential code insulated from concurrent execution issues. The isolation of coordination mechanisms allows a global treatment and analysis on coordination constraints between components even if local computations on components are not visible (i.e., components are "black boxes"). BIP (Behavior Interaction Priority). BIP is a general framework supporting rigorous design. It uses a dedicated language and an associated toolset supporting the design flow. The BIP language allows building complex systems by coordinating the behavior of a set of atomic components. Behavior is described with Labelled Transition Systems (LTS) extended with data and functions written in C. The description of coordination between components is layered. The first layer describes the interactions between components. The second layer describes dynamic priorities between the interactions and is used also to express scheduling policies. The combination of interactions and priorities characterizes the overall architecture of a system. It confers BIP strong expressiveness that cannot be matched by other existing formalism dedicated to CBS [START_REF] Bliudze | A Notion of Glue Expressiveness for Component-Based Systems[END_REF]. Moreover, BIP has a rigorous operational semantics: the behavior of a composite component is formally described as the composition of the behaviors of its atomic components. This allows a direct relation between the underlying semantic model and its implementation. Runtime-verification (RV) [START_REF]Runtime Verification[END_REF][START_REF] Bauer | Comparing ltl semantics for runtime verification[END_REF][START_REF] Falcone | Runtime verification of safety-progress properties[END_REF] is an effective technique to ensure, at runtime, that a system meets a desirable behavior. It can be used in numerous application domains, and more particularly when integrating together unreliable software components. In RV, a run of the system under scrutiny is analyzed incrementally using a decision procedure: a monitor. This monitor may be generated from a user-provided high level specification (e.g., a temporal formula, an automaton). This monitor aims to detect violation or satisfaction w.r.t. the given specification. Generally, it is a state machine processing an execution sequence (step by step) of the monitored program, and producing a sequence of verdicts (truth-values taken from a truth-domain) indicating specification fulfillment or violation. Recently [START_REF] Falcone | Runtime verification of safety-progress properties[END_REF] a new framework has been introduced for runtime verification. This expressive framework, leveraged by a finite-trace semantics and an expressive truth-domain, allows to monitor all specifications expressing a linear temporal behavior. The proposed approach (informal overview). We introduce a complementary validation technique for CBS in general and BIP systems in particular. We leverage the BIP framework by integrating a component-based version of the runtime verification framework introduced in [START_REF] Falcone | Runtime verification of safety-progress properties[END_REF]. Given a specification, our method uniformly integrates a monitor as an additional component in a BIP system that is able to runtime check the satisfaction or violation of the specification. The whole method is implemented in a prototype tool, RV-BIP, that automatically instrument BIP systems with monitors. Thanks to the code generator of BIP, the generated self-monitoring system can be directly translated into an actual C module embedded in the global system whose behavior is checked at runtime against the specification. The whole approach has been evaluated on a real robotic application and our experiments validate the relevance of our method. Paper Organization. The paper is structured as follows. In Section 2 we give a minimal introduction to the BIP framework. Section 3 defines an abstract RV framework for CBS described in BIP. Section 4 shows how the abstract RV framework is implemented for BIP systems. Section 5 describes RV-BIP, a prototype implementation of our method, used to evaluate our method on a robot application. Section 6 is dedicated to related work. Finally, Section 7 raises some concluding remarks and open perspectives. Notations. In this paper, we use the following notations. For two domains of elements E and F , we note

[E → F ] (resp. [E F ]
) the set of functions (resp. partial functions) from E to F . When elements of E depends on the elements of F , we note {e ∈ E} f ∈F , where

F ⊆ F , for {e ∈ E | f ∈ F } or {e} f ∈F when clear from context.

BIP -Behavior Interaction Priority

In this section we recall the necessary concepts of the BIP framework [START_REF] Basu | Modeling heterogeneous real-time components in BIP[END_REF]. BIP is a component-based framework for constructing systems by superposing three layers of modeling: Behavior, Interaction, and Priority. The behavior layer consists of a set of atomic components represented by transition systems. The interaction layer models the collaboration between components. Interactions are described using sets of ports and connectors between them [START_REF] Bliudze | The algebra of connectors-structuring interaction in BIP[END_REF]. The priority layer is used to enforce scheduling policies applied to the interaction layer, given by a strict partial order on interactions.

Component-based Construction

BIP offers primitives and constructs for modeling and composing complex behaviors from atomic components. Atomic components are Labeled Transition Systems (LTS) extended with C functions and data. Transitions are labeled with sets of communication ports. Composite components are obtained from atomic components by specifying connectors and priorities.

Atomic

Components. An atomic component is endowed with a set of local variables X taking values in a domain Data. Atomic components synchronize and exchange data with other components through the notion of port.

Definition 1 (Port). A port p[X ]

, where X ⊆ X, is defined by a port identifier p and some data variables in a set X (referred as the support set).

Definition 2 (Atomic component). An atomic component B is defined as a tuple (P, L, T, X, {g τ } τ ∈T , {f τ } τ ∈T ), where:

-(P, L, T ) is an LTS over a set of ports P . L is a set of control locations and T ⊆ L × P × L is a set of transitions. -X is a set of variables.

-For each transition τ ∈ T :

• g τ is a Boolean condition over X: the guard of τ ,

• f τ ∈ {x := f x (X) | x ∈ X} * : the computation step of τ , a list of statements.
For τ = (l, p, l ) ∈ T a transition of the internal LTS, l (resp. l ) is referred as the source (resp. destination) location and p is a port through which an interaction with another component can take place. Moreover, a transition τ = (l, p, l ) ∈ T in the internal LTS involves a transition in the atomic component of the form (l, p, g τ , f τ , l ) which can be executed only if the guard g τ evaluates to true, and f τ is a computation step: a set of assignments to local variables in X. At location l 1 , the transition labelled by the port p 1 is possible (the guard evaluates to true by default). When an interaction through p 1 takes place, a random value is assigned to the variable x through x := rand (). From the control location l 2 , the transition labelled by the port p 2 is possible, the variable x is not modified, the value of x is printed and exported through p 2 .

Semantics of Atomic Components. The semantics of an atomic component is an LTS over configurations and ports, formally defined as follows:

Definition 3 (Semantics of Atomic Components). The semantics of the atomic component (P, L, T, X,

{g τ } τ ∈T , {f τ } τ ∈T ) is an LTS (P, Q, T 0 ) s.t. -Q = L × [X → Data], -T 0 = {((l, v), p, (l , v )) ∈ Q × P × Q | ∃τ = (l, p, l ) ∈ T : g τ (v) ∧ v = f τ (v)}.
A configuration is a pair (l, v) ∈ Q where l ∈ L is a control location, and v ∈ [X → Data] is a valuation of the variables in X. The evolution of configurations (l 1 , v) p(vp) → (l 2 , v ), where v p is a valuation of variables attached to port p, is possible if there exists a transition (l 1 , p[x p ], g τ , f τ , l 2 ), s.t. g τ (v) = true. As a result, the valuation v of variables is modified to

v = f τ (v[x p ← v p ]).
Creating composite components. Assuming some available atomic components B 1 , . . . , B n , we show how to connect {B i } i∈I with I ⊆ [1, n] using connectors.

A connector γ is used to specify possible interactions, i.e., the sets of ports that have to be jointly executed. Two types of ports (synchron, trigger) are defined, in order to specify the feasible interactions of a connector. A trigger port is active: it can initiate an interaction without synchronizing with other ports. It is graphically represented by a triangle. A synchron port is passive: it needs synchronization with other ports for initiating an interaction. It is graphically represented by a circle. A feasible interaction of a connector is a subset of its ports s.t. either it contains some trigger, or it is maximal.

u u u u s r 1 r 2 r 3 u u u s r 1 r 2 r 3 Rendezvous Broadcast
The figure on the left shows two connectors: Rendezvous (only the maximal interaction sr 1 r 2 r 3 r 4 is possible), Broadcast (all the interactions containing the trigger port s are possible). Formally, a connector is defined as follows:

Definition 4 (Connector). A connector γ is a tuple (P γ , t, G, F ), where:

- A communication between the atomic components of {B i } i∈I through a connector (P γ , G, F ) is defined using the notion of interaction: Definition 5 (Interaction). A set of ports a = {p j } j∈J ⊆ P γ for some J ⊆ I is an interaction of γ if one of the following conditions holds: (1) there exists j ∈ J s.t. p j is trigger; (2) for all j ∈ J, p j is synchron and {p j } j∈J = P γ .

P γ = {p i [x i ] | p i ∈ B i .P } i∈I s.t
An interaction a has a guard and two functions G a , F a , respectively obtained by projecting G and F on the variables of the ports involved in a. We denote by I(γ) the set of interactions of γ. Synchronization through an interaction involves two steps. First, the guard G a is evaluated, then the update function F a is applied. If there are several possible interactions inside a connector, we choose the interaction involving the maximum3 number of ports. One can also add priorities to reduce non-determinism whenever several interactions are enabled. Then, the interaction with the highest priority is chosen.

Definition 6 (Composite Component).

A composite component is defined from a set of available atomic components and a set of connectors. The connection of the {B i } i∈I using the set Γ of connectors is denoted Γ ({B i } i∈I ).

Note that a composite component obtained by composition of a set of atomic components can be composed with other components in a hierarchical and incremental fashion using the same operational semantics.

Definition 7 (Semantics of Composite Components).

A state q of a composite component C = Γ (B 1 , . . . , B n ), where Γ connects the B i 's for i ∈ I, is an n-tuple q = (q 1 , . . . , q n ) where q i = (l i , v i ) is a state of B i . Thus, the semantics of C is precisely defined as a transition system (Q, A, -→), where:

-Q = B 1 .Q × . . . × B n .Q, -A = ∪ γ∈Γ {a ∈ I(γ)
} is the set of all possible interactions, --→ is the least set of transitions satisfying the following rule:

∃γ ∈ Γ : γ = (P γ , G, F ) ∃a ∈ I(γ) G a (v(X)) ∀i ∈ I : q i pi(vi) -→ i q i ∧ v i = F ai (v(X)) ∀i ∈ I : q i = q i (q 1 , . . . , q n ) a -→ (q 1 , . . . , q n )
where a = {p i } i∈I , X is the set of variables attached to the ports of a, v is the global valuation of variables, and F ai is the partial function derived from F restricted to the variable associated to p i .

The meaning of the above rule is the following: if there exists an interaction a s.t. all its ports are enabled in the current state and its guard (G a (v(X))) evaluates to true, then we can fire the interaction. When a is fired, not involved components stay in the same state, and, involved components evolve according to the interaction. Notice that several distinct interactions can be enabled at the same time, thus introducing non-determinism in the product behavior, possibly restricted using priorities. Definition 8 (Priority). Let C = (Q, A, -→) be the behavior of the composite component Γ (B 1 , . . . , B n ). A priority model π is a strict partial order on the set of interactions A. Given a priority model π, we abbreviate (a, a ) ∈ π to a ≺ a . The component π(C) is defined by the behavior (Q, A, -→ π ), where -→ π is the least set of transitions satisfying the following rule:

q a -→ q a ∈ A, q ∈ Q : a ≺ a ∧ q a -→ q q a -→ π q
An interaction is enabled in π(C) only if it is enabled in C, and, it is maximal according to π among the active interactions in C. Finally, we consider systems defined as a parallel composition of components together with an initial state.

Definition 9 (System).

A system S is a pair (B, Init) where B is a component and Init is the initial state of B.

An RV Framework for Component-Based Systems

We adapt classical RV frameworks dedicated to monitoring of sequential monolithic programs to CBS in general, and, to BIP systems in particular. We consider a composite component C = Γ (B 1 , . . . , B n ) and a priority model π, where the runtime semantics of π(C) is an LTS (Q, A, -→ π ) as introduced in Definitions 7 and 8.

Specifications for component-based systems (CBS)

Considered specifications of CBS are state-based specifications expressing some desired behavior. We do not assume any particular specification formalism except that we require it expresses a subset of the possible linear behaviors of CBS. In order to make our approach as general as possible, we only describe the events of the possible specification language. We also assume the existence of a monitor synthesis algorithm from this specification formalism (see Section 3.2). For this purpose, the existing solutions (e.g., [START_REF] Stolz | Temporal assertions with parametrised propositions[END_REF]) provided by the research efforts in RV can be easily adapted.

We follow a classical approach where events are built over a set of atomic propositions Prop. Intuitively, an atomic proposition is a Boolean expression over the states of the components (e.g., "in the component B 1 , the variable x should be positive if in the component B 2 the variable y is negative"). More formally, an event of π(C) is defined as a state formula over the atomic propositions expressed on components involved in π(C). The set of events is defined with the following grammar:

Σ(π(C)) : Atom ∨ Atom | Atom ∧ Atom | Atom ⇒ Atom | ¬ Atom Atom : component.var == val | component.var ≥ val | component.loc == a location | component.port == a port component.var : ∪ i∈[1,n] B i .X val : v ∈ Data a location : s ∈ ∪ i∈[1,n] B i .L a port : p ∈ ∪ i∈[1,n] B i .P

Verification Monitors [4]

A monitor is a procedure consuming events fed by a BIP system and producing an appraisal on the sequence of events read so far. We follow a general approach considering verification monitors as deterministic finite-state machines producing a truth-value (a verdict) in an expressive 4-valued truth-domain

B 4 def = {⊥, ⊥ c , c , }, introduced in [3]
and used in [START_REF] Falcone | Runtime verification of safety-progress properties[END_REF]. B 4 consists of the possible evaluations of a sequence of events and its possible futures relatively to the specification used to generate the monitor:

-The truth-value c (resp. ⊥ c ) denotes "currently true" (resp. "currently false") and expresses the satisfaction (resp. violation) of the specification "if the system execution stops here". -The truth-value (resp. ⊥) is a definitive verdict denoting the satisfaction (resp. violation) of the specification: the monitor can be stopped.

We define the notion of monitor for a specification defined relatively to a set of events Σ expressed on a composite component.

Definition 10 (Monitor).

A monitor A is a tuple (Θ A , θ A init , Σ, -→ A , B 4 , ver A ). The finite set Θ A denotes the control states and θ A init ∈ Θ A is the initial state. The complete function -→ A : Θ A ×Σ → Θ A is the transition function. In the following we abbreviate -→ A (θ, a) = θ by θ a -→ A θ . The function ver A : Θ A → B 4 is an output function, producing verdicts (i.e., truth-values) in B 4 from control states. Such monitors are independent from any specification formalism used to generate them and are able to check any specification expressing a linear temporal specification [START_REF] Falcone | Runtime verification of safety-progress properties[END_REF]. Intuitively, runtime verification of a specification with such monitors works as follows. An execution sequence is processed in a lock-step manner. On each received event, the monitor produces an appraisal on the sequence read so far. For a formal presentation of the semantics of the monitor and a formal definition of sequence checking, we refer to [START_REF] Falcone | Runtime verification of safety-progress properties[END_REF]. In the remainder, we consider a monitor A = (Θ A , θ A init , Σ, -→ A , B 4 , ver A ).

Runs and traces of BIP systems

Runs of BIP systems. Each state q ∈ Q in the LTS of a component can be seen as an environment mapping variables used in the specification over an alphabet Σ to values.

Definition 11 (Environments in a component). The set of possible environments in

π(C) is Env def = ∪ i∈[1,n] {state i → Q i } ∪ [B i .X → Data] .
The environment defined by a state q = (q 1 , . . . , q n ), where

q i = (l i , v i ) for each i ∈ [1, n], is [[q]] ∈ Env s.t. [[q]] def = ∪ i∈[1,n] (∪ xi∈Bi.var {x → v i (x)} ∪ ∪ i∈[1,n] {state i → l i }.
After an interaction bringing the component in a state q, an event e is fired if the stateformula associated to e holds, noted q e, i.e., when e evaluates to true in [[q]], i.e., [[q]](e) = true. Let us note that, after reaching a state of the LTS corresponding to the runtime behaviors of a BIP component, it is always possible to determine whether an event is fired or not, i.e., whether the corresponding state-formula holds or not.

We present the notion of run of a composite component and how it is monitored.

Definition 12 (Run of a composite component). A run of length m of a system (π(C), Init) is the sequence of environments

[[q 0 ]] • [[q 1 ]] • • • [[q m ]] s.t.: q 0 = Init, and, ∀i ∈ [0, m -1] : q i ∈ Q ∧ ∃a i ∈ A : q i ai -→ π q i+1 .
Definition 13 (Monitoring a run of a system). The verdict

[[A]](q 0 • q 1 • • • q m ) stated by A for a run [[q 0 ]] • [[q 1 ]] • • • [[q m ]] is ver A (θ m ) where ∀i ∈ [0, m -1] : θ i e -→ A θ i+1
where e is the unique event enabled in θ i s.t. q i+1 |= e.

Building a trace from a run. As one of the challenges in RV is to lower the performance impact on the target program, we should take care of minimizing the information sent to the monitor. Making the monitor processing directly the run of the target program directly is not a reasonable solution because it would yield prohibiting overhead. Our proposal is to send a relevant abstraction of the run to the monitor that we call a trace. Intuitively, given a run, the obtained trace is its minimal abstraction (information wise) that permits to evaluate the specification as if the run was not abstracted. Given Spec(Σ), a specification defined over a vocabulary of events Σ, we design an abstraction function ↓ Σ α building this minimal abstraction. We thus define a notion of informativeness of environments built from states. Intuitively, an environment ρ 1 is less informative than an environment ρ 2 if it has less variables defined, i.e., ρ 1 ρ 2 if Dom(ρ 1 ) ⊆ Dom(ρ 2 ) and ∀x ∈ Dom(ρ 1 ) : ρ 1 (x) = ρ 2 (x). When monitoring a CBS our aim will be to dynamically build the least informative environment so that the monitoring activity of the system amounts to monitoring with the global state.

Definition 14 (Abstraction function). The abstraction function ↓

Σ α : Q → Env is the least function s.t.: ∀q ∈ Q : ↓ Σ α (q) = ρ and ρ is s.t.: ∀x ∈ Dom([[q]]) : ρ(x) = [[q]](x) if ∃e ∈ Σ, ∃ap ∈ Prop(e) : used (ap) = (B i , x), with x ∈ B i .X; undef otherwise.
Property 1 (Abstraction preserves event evaluation). The previous abstraction function adheres to the two following principles:

soundness: ∀e ∈ Σ, ∀q ∈ Q : ↓ Σ α (q) e ⇔ q e, completeness: ∀e ∈ Σ, ∀q ∈ Q : ↓ Σ α (q) e∨ ↓ Σ α (q) e. Soundness states that the concrete and abstracted evaluations are the same. Completeness states that evaluation of all specification events remains possible: abstraction does not erase the needed information from the environment.

Definition 15 (Trace of a composite component). The trace defined from a run

[[q 0 ]] • [[q 1 ]] • • • [[q m ]] through an abstraction function ↓ Σ α is the sequence of environments de- fined as ↓ Σ α (q 0 ) • ↓ Σ α (q 1 ) • • • ↓ Σ α (q m
). The notion of trace evaluation by a monitor directly follows from the notion of run evaluation. Moreover, the following theorem, which is a direct consequence of Property 1, states that, for runtime verification, there is no difference regarding property evaluation to process the trace instead of the run.

Theorem 1 (Trace evaluation vs run evaluation by a monitor). For A defined on Σ, the abstraction function ↓ Σ α , and a run

[[q 0 ]] • [[q 1 ]] • • • [[q m ]],
we have:

[[A]] [[q 0 ]] • [[q 1 ]] • • • [[q m ]] = [[A]] ↓ Σ α (q 0 ) • ↓ Σ α (q 1 ) • • • ↓ Σ α (q m )
In the next section, we will instrument BIP systems in such a way that, given a specification, the minimal abstraction function (information-wise) is dynamically generated.

Verifying the Runtime Behavior of BIP Systems

This section presents how we instrument and integrate an abstract monitor A = (Θ A , θ A init , Σ, -→ A , B 4 , ver A ) into a BIP system made of a composite component C = Γ (B 1 , . . . , B n ) and priority rules π. The work-flow is as follows (see Fig. 1):

1. From the input abstract monitor we extract the list of components and their corresponding variables used by the monitor (Section 4.1). 2. For each component and its corresponding variables extracted from the monitor we instrument the selected components so as to observe them (Section 4.2). 3. From the monitor we generate the corresponding atomic component. Then, we add the generated component (a monitor in BIP) to the input composite component (Section 4.3). 4. Finally, we add the new connections between the instrumented atomic components and the monitor in BIP (Section 4.4).

BIP Monitor

Extraction of needed information

The first step is to retrieve from the monitor the set of components and their corresponding variables that should be monitored. For each selected component, transitions are instrumented to observe the just needed set of variables. For a specification expressed over Σ(π(Γ (B 1 , . . . , B n ))) and its monitor, comp(Σ ) is the subset of ∪ i∈[1,n] {B i } corresponding to the set of components that should be monitored. We also define occur(Σ) to be the subset of

{B i .loc | i ∈ [1, n]} ∪ {B i .port | i ∈ [1, n]} ∪ ∪ i∈[1,n] B i .X de-
noting the set of variables used in the specification. Then from occur(Σ), we sort the variables according to the component B i (where B i ∈ comp(Σ )) they are related to:

c v() = [1, n] → {B i .loc} i∈[1,n] ∪ {B i .port} i∈[1,n] ∪ ∪ i∈[1,n] B i .X s.t. c v (i ) is the set of variables related to component B i .

Instrumentation of atomic component

For a composite component Γ (B 1 , . . . , B n ), we transform each atomic component B i , i ∈ [1, n], so that it is able to interact with the monitor, if necessary.

Definition 16 (Instrumenting atomic components). Given

B = (P, L, T, X, {g τ } τ ∈T , {f τ } τ ∈T ) s.t. B = B i ∈ {B 1 , . . . , B n }, we define a new atomic component B m = B if B / ∈ comp(Σ ) (P m , L m , T m , X m , {g τ } τ ∈T m , {f τ } τ ∈T m ) otherwise where, (P m , L m , T m , X m , {g τ } τ ∈T m , {f τ } τ ∈T m ) is defined as follows: -X m = X ∪ {loc | B i .loc ∈ c v (i )} ∪ {port | B i .port ∈ c v (i )}; -P m = P ∪ {p m [c v (i )]}, -L m = L ∪ {l τ } τ ∈inst(T )
, where inst(T ) is defined as follows:

inst(T ) = T if {Bi.loc, Bi.port} ∩ c v (i) = ∅ {τ ∈ T | c v (i) ∩ var(fτ ) = ∅} otherwise -T m = T \ inst(T ) ∪ {in(τ ) | τ ∈ inst(T )} ∪ {out(τ ) | τ ∈ inst(T )}, where,
• in(τ ) = (l, p, f in(τ ) , g τ , l τ ), where We note B m = Instrum(B). In X m , loc and port are variables containing a location name and a port name respectively. In P m , p m designates the port created for interacting with the monitor. Moreover, inst(T ) is the set of transitions that should be instrumented: we instrument atomic components whose variables are needed by the monitor. T m designates the transitions in the instrumented atomic component. We instrument the transitions in the corresponding atomic component that are modifying a variable involved with the monitor. If the state or the port of an atomic component is needed, all transitions are instrumented. For each transition τ ∈ inst(T ) that should be instrumented we add a new transition to interact with the monitor. Transitions are also instrumented by adding new statements to save the state and the port name, if necessary.

f in(τ ) =        fτ if Bi.loc / ∈ c v (i) ∧ Bi.port / ∈ c v (i) fτ ; [loc := "l"] if Bi.loc ∈ c v (i) ∧ Bi.port / ∈ c v (i) fτ ; [port := "p"] if Bi.loc / ∈ c v (i) ∧ Bi.port ∈ c v (i) fτ ; [loc := "l"; port := "p"] if Bi.loc ∈ c v (i) ∧ Bi.port ∈ c v (i) • out(τ ) = (l τ , p m , f out(τ ) , true, l ), where f out(τ ) = [].
Example 2 (Instrumentation of an atomic component). Figure 2 illustrates the instrumentation of the atomic component depicted on the left-hand side into the instrumented component on the right-hand side. For instance, supposing that the state should be monitored, from the transition τ 0 = (l 0 , p 1 , f τ0 , true, l 1 ) with f τ0 = [done := 0], we create a new state l τ0 and the transitions in(τ 0 ) = (l 0 , p 1 , f in , true, l τ0 ) with f in = [done := 0; loc := "l0"; port := "p 1 "], and out(τ 0 ) = (l τ0 , p 1 , [], true, l 1 ).

Creating an atomic component from a monitor

From an abstract monitor (cf. Definition 10) given as an XML file, we construct the corresponding atomic component in BIP that interacts with the instrumented atomic components and produces verdicts following the behavior of the original monitor.

Definition 17 (Building monitors in BIP). From a monitor A = (Θ A , θ A init , Σ, -→ A , B 4 , ver A ), we define the corresponding atomic component M A = (P, L, T, X, {g τ } τ ∈T , {f τ } τ ∈T ) as an atomic component implementing its behavior:

-P = {p m [X], p intern []}, -L = Θ A ∪ {q mi } qi∈Θ A , -T = T 1 ∪ T 2 , where -T 1 = {(q i , p m , [], true, q mi ) | q i ∈ Θ A }, -T 2 = {(q mi , p intern , a, print(ver A (q i )), q i ) | q i a -→ A q i ∧(q i , p M , q mi ) ∈ T 1 }, -X = occur(Σ).
We note M A = BuildMon(A) and call M A a BIP monitor. T 1 denotes the set of transitions interacting with the composite component. T 2 is the set of transitions used to display verdicts following the behavior of the original monitor A. The set of variables of the monitor is the set of variables used in the specification (as in Section 4.1).

Example 3 (Transforming an abstract monitor into a BIP monitor). Fig. 3 illustrates the transformation of Definition 17. The atomic component in Figure 3(a) is transformed into the BIP monitor in Figure 3(b). <VerificationMonitor> <State id="s1" initial="true"> <Transition event="e1" nextState="s1" output="currently true"/> <Transition event="not e1" nextState="s2" output="false"/> </State> <State id="s2"> <Transition event="true" nextState="s2" output="false"/> </State> </VerificationMonitor> (a) Abstract Monitor print("currently true"); print("false");

print("false");

Connections

The next step of our transformation is to define the connectors between the transformed components B m and the BIP monitor M A .

Definition 18 (Connections). Given

A and π(Γ (B 1 , . . . , B n )), the monitored com- posite component is π m (Γ m (B m 1 , . . . , B m n , M A ))
, where:

-B m i = Instrum(B i ), for i ∈ [1, n], (see Definition 16); -M A = BuildMon(A), (see Definition 17); -Γ m = γ ∪ {γ 1 = (P γ1 , true, F γ1 ), γ 2 = (M A .p intern , true, ∅)}, where, -P γ1 = {B i .p m [X m i ]} Bi∈comp(Σ ) } ∪ {M A .p m }
, where all ports are synchron; -F γ1 , the update function, is the identity data transfer from the variables in the ports of the interacting components B i (i ∈ 51, n]) to the corresponding variables in the monitor port; the type of the port M A .p intern in the connector γ 2 is synchron (one and only one interaction is defined by this connector: γ 2 , see Definition 5);

-π m = π ∪ {a ≺ a | a ∈ ∪ γ∈Γ I(γ) ∧ a ∈ I(γ 1 ) ∪ I(γ 2 )}.
The interactions defined by γ 1 and γ 2 have more priority than those defined by Γ (illustrated in Fig. 1). It ensures that, after execution of an interaction by the involved components, the monitor produces verdict before involving other interactions.

Summary and discussion

We propose a 4-stage approach to introduce runtime verification for CBS. Our method directly integrates an abstract monitor in a CBS. Thanks to the BIP framework, monitoring of a specification can be taken into account at design stage. Moreover, the actual system, automatically generated from the augmented BIP model, is runtime-checked.

The correctness proof is omitted due to the lack of space, and, relies on the following informal arguments. Our transformations do not modify the data nor the behavior induced by the initial interactions. No deadlock is introduced because the synthesized BIP monitor is always ready to receive events from the instrumented components. Finally, the priorities introduced when connecting the instrumented components to the BIP monitor (Section 4.4) guarantee that the monitor always receives fresh data, i.e., the latest system state.

Implementation and Evaluation

RV-BIP: A tool for Runtime Verification of BIP systems

RV-BIP is a Java implementation (∼ 2500 LOC) of the transformations described in Section 4, and, is part of the BIP distribution. RV-BIP takes as input a BIP system and an abstract monitor (an XML file) and then outputs a new BIP system whose behavior is monitored. It uses the following modules (see Fig. 1):

Case study: a robotic application

We experimented RV-BIP on a robotic application modeled in BIP: Dala robot [START_REF] Fleury | GenoM: A Tool for the Specification and the Implementation of Operating Modules in a Distributed Robot Architecture[END_REF][START_REF] Bensalem | Toward a more dependable software architecture for autonomous robots[END_REF]. The Dala robot is a large and realistic interactive system. It is an infinite system (in terms of states and transitions) that cannot be model-checked. The functional level of the Dala robot consists of a set of modules. A module is composed of a set of services corresponding to different tasks and a set of posters where the produced data is stored and exchanged between different modules. In this section, due to the lack of space, we present a simplified model of the modules with only the services related to two properties among those we runtime checked.

Execution order: Figure 4 shows a simplified model of Dala. It consists of 3 components: ProxyInterface, InitService and SetSpeedService. ProxyInterface communicates with the control layer using the mailbox by executing the transition check. Init-Service is responsible for the initialization of the module and SetSpeedService performs the main task of the module. According to the received request, Proxy triggers either InitService or SetSpeedService. Each service has a status variable done: value 1 means that the corresponding task has been successfully executed. A service can be triggered through the port trigger, then it executes its task by taking the transition start and finally it returns to the initial location by the transition finish when the task is done. The execution order of some services are important. In this module, InitService initializes Table 1. Formalization of the requirements for the Dala robot ϕ 1 : (e 1 ) * , where, e 1 : (SetSpeedService.port=="trigger " ∧ ProxyInterface.port=="exec")⇒(InitService.done==1) ϕ 3 : (e 1 ) * , where, e 1 : (Reader .port=="read" ∧ poster .port=="read" ∧ Clock .port=="getTime") ⇒(Clock .time-poster .wrtime≤2 ) ϕ 2 : (e 1 e 2 ) * , where, ϕ 4 : (e 1 ( +e 2 +e 2 e 2 )e 3 ) * , where, the robot and should be successfully executed before SetSpeedService sets the speed parameter of the robot. This requirement is formalized as "ϕ 1 and ϕ 2 ", see Table 1.

Data freshness: In Dala, the modules communicate by a set of posters. Data generated by a module is written in a poster that can be accessed by another module. The behavior of the robot might depend on this data, therefore it is necessary that the data is up to date: the data read by a service of a module (called Reader ) must be fresh enough compared to the moment it has been written (by a service called Writer ). If t 1 and t 2 respectively are the moments of reading and writing actions, then the difference between t 1 and t 2 must be less than a specific duration δ, i.e., |t 2 -t 1 | ≤ δ. This requirement is formalized as "ϕ 3 and ϕ 4 ", see Table . 1. In the model, the time counter is implemented by a component Clock , and the tick transition occurs every second. Experiments: 2 reports results on checking the ordering and freshness properties of the Dala robot. Ordering violated and Ordering guaranteed correspond to the model presented in Fig. 4: the first one might have the violation of the ordering specification whereas the second one always guarantees it. Each consists of an InitService, a Set-SpeedService and ten other services (corresponding to different tasks). It is similar for Data freshness violated and Data freshness guaranteed: the first might have the violation of the freshness specification whereas the second always guarantees it. We consider two modules: the first has a service responsible for writing data and five other services; the second has a service responsible for reading data produced by the first module and also five other services. In Table 2, time-no-monitor indicates the execution time without monitoring; specification is the monitored specification; the optimized column reports the execution time and the overhead obtained with the monitor that interacts only with the two components involved in the specification; and the not-optimized column reports the execution time and the overhead obtained with a monitor that observes all components of the system (even the ones that are not involved in the specification).

The results substantiate our claim that if we monitor only components involved in the specification, using the abstraction technique defined in Section 3 and implemented in Section 4, the overhead is reduced significantly.

Related Work

Static verification of component-based system. With the growing demand of scalability and complexity for systems, verification techniques should be used to determine whether a designed system meets its requirements. Static formal verification [START_REF] Umrigar | Formal verification of a real-time hardware design[END_REF][START_REF] Queille | Specification and verification of concurrent systems in CESAR[END_REF][START_REF] Clarke | Synthesis of synchronisation skeletons for branching time temporal logic[END_REF] is based on mathematical techniques to prove or disprove the correctness of a design w.r.t. a given formal specification. It searches for input patterns which lead to violations of the desired properties and prove the correctness when such violations do not exist. Existing formal verification methods for component-based systems are based on either static analysis or on model-checking [START_REF] Mcmillan | Symbolic model checking[END_REF][START_REF] Burch | Symbolic model checking: 10 20 states and beyond[END_REF][START_REF] Clarke | Bounded model checking using satisfiability solving[END_REF]. Approaches based on static analysis consist in computing specific invariants in order to abstract the state space. Though this kind of approaches is less sensitive to state explosion, it still suffers from some limitations. First these techniques are rather limited in terms of the properties they can check: they are mostly limited to safety properties and thus some interesting behavioral properties remains out of the scope of these techniques. Moreover, since these approaches rely on abstraction and over approximation of the state space, they yield several false positives.

Behavioral approaches such as model-checking are based on an exhaustive exploration of the state space of the model obtained from the operational semantics of the specification language. For large systems, this exploration leads to a very large number of states (the well-known state explosion problem). Despite recent advances in modelchecking, the state-explosion problem is far from being solved and refrain the use of these methods in component-based systems where the state space tends to become huge due to the number of possible configurations and interactions between components. On the other hand, techniques based on compositional verification [START_REF] Clarke | Compositional model checking[END_REF][START_REF] Chang | Compositional verification of real-time systems[END_REF][START_REF] Long | Model Checking, Abstraction, and Compositional Reasoning[END_REF] (less sensitive to state explosion) are not applicable when the behavior of some parts of the system is unknown -as it can be the case in BIP when using external C functions.

A compositional verification method based on invariants for checking safety properties in component-based systems is provided in [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF][START_REF] Bensalem | Incremental component-based construction and verification using invariants[END_REF]. Although the method has been successfully applied to large-scale and complex systems, the use of invariants can deal only with safety properties and might produce many false positive counter examples.

Another compositional approach is design-by-contract [START_REF] Meyer | Applying "design by contract[END_REF][START_REF] Abadi | Composing specifications[END_REF] that considers a property provided by a component as a contract between this component and its environment. For instance [START_REF] Hafaiedh | Reasoning about safety and progress using contracts[END_REF] provides a method that searches an implementation model that satisfies a given contract. Although the experimental results are promising, it is not always possible to find an implementation model that satisfies a given property. Moreover, the composition of contracts in concurrent systems can be very expensive. Dynamic verification of component-based systems. Specification and verification of the behavior of CBS have received some research endeavor. A first series of approaches specify the behavior of components in terms of pre and post-conditions (e.g., with JML) or assertions (e.g., using Eiffel). More recently and closer to our work is the LIME specification language [START_REF] Kähkönen | The lime interface specification language and runtime monitoring tool[END_REF] that allows runtime monitoring of temporal properties for component interfaces. Components are seen as black boxes and LIME specifications describe how components should interact with an external application by describing a desired behavior on the calls and returns over the interface. Comparison with our approach. The limitations of static validation techniques lead us to investigate the use of runtime verification as an alternative and complementary technique to validate CBS. Compared to previous dynamic techniques, our approach offer several advantages. First, it uses the latest advances in runtime verification using an expressive 4-valued truth-domain allowing our monitor to be generated using any monitor synthesis framework. Note also that the proposed RV framework only uses information about the events used in the specification. The monitors presented in this paper are bounded to regular properties, however, the expressiveness of the BIP language confers our monitors a potential to be Turing-complete. Moreover, our approach is not limited to monitoring component interfaces. It is often the case that components come with an abstract behavioral model, i.e., components are gray boxes instead of black boxes. Our monitoring framework supports both kinds of approaches. Furthermore, the specifications considered for BIP systems use locations spanning over several components allowing the specification of global behaviors of the system in composition.

Conclusion and Future Work

This paper introduces runtime verification as a complementary validation technique for component-based systems written in the BIP framework. Our technique is based on a general and expressive runtime verification framework. It dynamically builds a minimal abstraction of the current runtime state of the system so as to lower the performance impact. By generating monitors directly as BIP components, we are able to generate actual monitored C programs. Our approach has been implemented in RV-BIP that smoothly integrate in the existing BIP tool-set. Finally, experimental evaluations on a robotic application substantiate our claims and the feasibility of our approach.

Several research perspectives can be considered. A first direction is to combine the recent advances in RV that use static analysis (see e.g., [START_REF] Bodden | Clara: A framework for partially evaluating finite-state runtime monitors ahead of time[END_REF]). In RV, using static analysis techniques may reduce the overhead induced by a monitor by disabling unnecessary runtime checks. Also related to overhead reduction, a dynamic instrumentation technique, enabling the monitor to remove connectors when they are not needed anymore, would reduce the overhead even more. Another possible direction is to extend the proposed framework for runtime enforcement [START_REF] Falcone | You should better enforce than verify[END_REF]. Runtime enforcement is an extension of RV aiming at circumventing property violation and provides better confidence in system behaviors. A more practical direction is to connect RV-BIP to the various existing monitor synthesis tools available within the RV community.

  Let us note Prop(e) the set of atomic propositions used in an event e ∈ π(C). For ap ∈ Prop(e) we define used (ap) as the set of pairs made of a component and variables that are used to define ap: used(ap) = match (ap) with component.var == val → (component,var) component.var ≥ val → (component,var) component.loc == a location → (component,loc) component.port == a port → (component,port)

2 (γ 2 > γ 3 , γ 4 Fig. 1 .

 2241 Fig. 1. Overview of the work-flow

Fig. 2 .

 2 Fig. 2. Instrumentation of an atomic component

Fig. 3 .

 3 Transforming an abstract monitor into a BIP Monitor.

Fig. 4 .

 4 Fig. 4. Two services involving the ordering specification -Extraction: this module extracts the components and the corresponding variables used in the monitor. It takes as input an abstract monitor and then outputs a list of components with their corresponding variables, -Atomic Transformation: this module instruments the atomic components selected from the extraction module. It takes as input the output of the Extraction module and a BIP file containing the original BIP system, -Building Monitor: this module takes as input an abstract monitor and then outputs the corresponding atomic component, -Connections: this module constructs the new composite component whose behavior is monitored. It takes as input the output from the Atomic Transformation and Building Monitor modules and then outputs a new composite component.

e 1 : 1 : 2 : 2 : 3 :

 11223 InitService.port=="finish" e Writer .port=="write" e SetSpeedService.port=="trigger " e Clock .port=="tick " e Reader .read=="read"

  Example 1 (Atomic component). The figure below shows an example of atomic component with two ports p 1 , p 2 , a variable x, and two control locations l 1 , l 2 .

	x	p 2
	l 1	p 2
		print(x)
	p 1
	x := rand()	l 2
	p 1

In the rest of this article, we use the dot notation to denote the elements of atomic components, e.g., B.P denotes the set of ports of an atomic component B.

  . ∀i ∈ I : P γ ∩ B i .P = {p i }, t : P γ → {true, false} s.t. t(p) = true if p is trigger (and false if synchron), -G is a Boolean expression over the set of variables ∪ i∈I x i (the guard), -F is an update function defined over the set of variables ∪ i∈I x i . P γ is the set of connected ports called the support set of γ. The ports in P γ are tagged with function t indicating whether they are trigger or synchron. Moreover, for each i ∈ I, x i is a set of variables associated to the port p i .

Table 2 .

 2 Results of monitoring the requirements Execution order and Data freshness

		time-no-monitor specification	optimized	not-optimized
				time (s) ovhd (%) time (s) ovhd (%)
	Ordering violated	1.896	ϕ1 ϕ2	2.045 1.953	7.8 3	9.163 9.192	383 384
	Ordering guaranteed	1.836	ϕ1 ϕ2	1.984 1.889	8.0 2.8	8.9 8.896	384 384
	Data freshness violated	1.638	ϕ3 ϕ4	1.684 1.682	2,8 2,6	4.337 3.773	164 130
	Data freshness guaranteed	1.634	ϕ3 ϕ4	1.678 1.690	2,6 3,4	4.383 3.782	168 131

This work is partially supported by the FP7 IP ASCENS.

If there are several maximal interactions, the choice between them is at random.


Sami Hebib
email: 1hebib@laas.fr2haubert@laas.fr

Hervé Aubert

Triband Antenna Feeding Circuit for Circular Polarization Diversity

In this paper, a compact and original feeding circuit architecture is proposed to synthesis the circular polarization of a triband antenna. A diplexer is used in this circuit in order to achieve circular polarization diversity, that is, right-hand circular polarization (RH-CP) for two radio-navigation bands (GPS/Galileo) and left-hand circular polarization (LH-CP) for a telemetry band (MicroSat TM). Simulation and measurement results are presented and validate the proposed feeding circuit concept.

INTRODUCTION

The need for circularly polarized multiband antennas is increasing particularly with the multiplication of satellite radionavigation systems (GPS, Galileo, GLONASS,...). Recently, an original circularly polarized triband antenna covering two radionavigation bands (GPS/Galileo: 1.197 and 1.575GHz) and one telemetry band (TM MicroSat : 2.245GHz) has been published by the authors [START_REF] Hebib | Multiband pyramidal antenna loaded by a cutoff open-ended waveguide[END_REF]. The circular polarization behaviour of this antenna is obtained by feeding its four radiating elements with progressive 90°-phase difference and equal magnitude (circular polarization synthesis). The use of such a technique is motivated by its good performance in terms of purity of circular polarization. A feeding circuit is therefore needed in order to provide the required excitation law at the different operating frequency bands of the antenna. To our knowledge, compact feeding circuits dealing with more than two frequency bands are rare, not to say, nonexistent. Moreover, the need for different circular polarizations (right or left) for different bands will further complicate this circuit.

In this paper, an original multiband feeding circuit architecture is proposed for circular polarization diversity. As an application, a very compact triband feeding circuit (11cm x 6.5cm) is designed, fabricated and measured. It provides right hand circular polarization (RH-CP) for two radionavigation bands and left hand circular polarization (LH-CP) for one telemetry band. For the first time, the simulation and measurement results of this circuit are presented and discussed.

II. DESCRIPTION OF THE MULTIBAND FEEDING ARCHETECTURE FOR POLARIZATION DIVERSITY

The proposed multiband feeding circuit architecture for circular polarization diversity is depicted in Figure 1. In this architecture, the bands needing right hand circular polarization (RH-CP) and those requiring left hand circular polarization (CP-LH) are separated, processed separately and then recombined using diplexers. Generating the required phase excitation law (progressive 90 °-phase differences) is achieved by a standard architecture based on 90°/180° couplers. The design of the diplexers of the Figure 1 remains the most difficult part. A diplexer based on distributed elements was designed for a multiband antenna with different polarization (linear and RH-CP) [START_REF] Marcaccioli | Planar microstrip diplexer for a multifunctional antenna[END_REF]. However, the use of distributed elements leads to a drastic increase of size compared to a lumped element implementation.

III. APPLICATION: GPS/GALILEO/TM MICROSAT TRIBAND ANTENNA FEEDING CIRCUIT

A. Description of the application

The considered application deals with the feeding of a triband antenna covering two radionavigation bands (Galileo/ GPS) and a telemetry band (TM MicroSat) [START_REF] Hebib | Multiband pyramidal antenna loaded by a cutoff open-ended waveguide[END_REF]. Circular polarization diversity is required in order to set right hand circular polarization for navigation applications and left hand circular polarization for telemetry applications. The technical specifications for this application are listed in Table I.

B. Couplers selection

The couplers for the two GPS/Galileo bands (RH-CP subcircuit in Figure 1) should cover a relative bandwidth of about 33%. They are connected in such a way to generate a right hand circular polarization in the bands GPS/Galileo. On the other hand, the couplers for MicroSat TM band (LH-CP sub-circuit in Figure 1) would be relatively narrowband since the relative bandwidth of the telemetry band is about 4%. However, they should be connected so as to obtain a left hand circular polarization. In order that the feeding circuit may be easily integrated into the limited area available in the triband antenna [START_REF] Hebib | Multiband pyramidal antenna loaded by a cutoff open-ended waveguide[END_REF], all the used couplers should be very compact. One can find a variety of commercial compact wideband surface-mount couplers with relative bandwidth up to 140%. For their compactness, these commercial couplers have been chosen for the design of the feeding circuit. However, due to the lack of commercial 180° couplers covering the bands of interest, each 180° coupler is replaced by three 90° couplers at the price of 3dB of additional losses. The 90° couplers chosen for GPS/Galileo bands and TM MicroSat band are, respectively, Mini-Circuits QCN-19 and QBA-24W [3]. These components are not only compact but also exhibit good performance in the bands of interest. Furthermore, the Sparameters of these couplers can be directly downloaded from the manufacturer's website.

C. Diplexer design

The diplexer should occupy a small area and present low insertion loss and high levels of channel isolation. It can be realized according to two techniques [START_REF] Matthaei | Microwave Filters, Impedance-Matching Networks, and Coupling Structures[END_REF]: the use of directional couplers or the connection of two parallel filters. The first option leads to a not easily compactable architecture, thus the second technique has been chosen. The designed diplexer is formed by the connection of a low-pass filter allowing the passage of the two GPS/Galileo bands and a high-pass filter allowing through the MicroSat TM band (see Figure 2 (a)). For compactness reasons and since five diplexers are required in the feeding circuit, the design of these two filters using distributed elements would not be possible. Thus, commercial surface-mount filters are selected for the design of the diplexer. This latter is designed using Mini-Circuits LFCN-1575 (low-pass filter) and HFCN-1810 (high-pass filter)[3]. Ideally, a filter should present zero impedance in its pass band and infinite impedance at all other frequencies. The design of a diplexer by the connection of two filters requires the use of filters having infinite impedance in their stop bands. If this condition is not satisfied, each filter may degrade the other performance. Using the S-parameters provided by Mini-Circuits, it was found that the two selected filters have relatively low input impedance in their rejection band. Consequently, the diplexer can not be simply designed by the straightforward connection of these two filters. One solution is to add impedance transformers or simply transmission lines upstream of the two filters in order to increase their input impedance at the reject band. These impedance transformers should not much affect the input impedance in the pass band. Using microstrip technology, the low-pass filter (LFCN-1575) is preceded by a microstrip line of length l 1 which transforms its low input impedance in the MicroSat TM band to a relatively high value. Similarly, the high-pass filter (HFCN-1810) is loaded by a microstrip line with length l 2 in order to increase the filter's input impedance in the GPS/Galileo bands. The T-junction thus constructed is illustrated in Figure 2 (b). To get the best performance in terms of insertion loss and rejection at the three operating bands of the antenna, an optimization of the lengths l 1 and l 2 (see Figure 2 (b)) is performed using Agilent ADS. The substrate used is TACONIC CER 10-0250, which has a relative permittivity constant of 9.5, with 0.635 mm thickness, and a loss tangent (tanį) of 0.0035. A 50Ω microstrip line on this substrate is approximately 0.6mm in width. The above-mentioned optimization yields the optimal values for the lengths l 1 and l 2 as follows: l 1 =22.9mm and l 2 =15.1mm. Figure 3

D. Feeding circuit simulation and realization

The simulation of different parts of the feeding circuit is achieved using Agilent ADS. The couplers and the filters are modeled by their S-parameters which are provided by the manufacturer (Mini-Circuit). It should be noted that the circuit-based simulation does not take into account parasitic effects related to the interconnection lines and connectors. Figure 4 shows photographs of the fabricated compact feeding circuit (110mm x 65 mm). 50ȍ chip resistors (EIA case size 0402) were used to load the isolated and unused outputs of the different couplers (QCN-19, QBA-24W).

E. Measurement results and discussion

Measurements of the feeding circuit were performed using Wiltron 360B VNA. Two ports were measured simultaneously while the three others were loaded with 50 SMA terminations. Figure 5 shows the simulated and measured transmission coefficients of the fabricated feeding circuit. The phase differences between transmission coefficients (measured only) of the fabricated feeding circuit are depicted in Figure 6. Table II summarizes the simulated and measured phase differences between transmission coefficients at the three operating frequencies of the antenna. At the intermediate frequency (1.575 GHz), simulated results of the amplitudes of the transmission coefficients show a good agreement with the experimental results. As a matter of fact, an amplitude difference between the four transmission coefficients not greater than 1 dB is obtained at this frequency. At the upper frequency (2.245 GHz), an amplitude imbalance of nearly 4 dB is observed experimentally (only 0.43 dB was expected from simulation). However, the amplitude attenuation of the four transmission coefficients at this frequency is lower than that obtained at the lower frequency (1.197 GHz). At this frequency and despite the low amplitude imbalance (1.5dB), the amplitudes of the transmission coefficients differ significantly from those predicted by simulation (about -21dB in measurement compared to -12dB in simulation). The phase difference results indicate that the maximum phase deviation does not exceed 10 ° between the four outputs of the feeding circuit at the two first frequencies (lower and intermediate). However, at the upper frequency, a deviation of about 23 ° is obtained in the worst case.

Additional simulations and measurements were conducted to understand the origin of this discrepancy between measurement and simulation, especially noted at the lower frequency. It has been found that this unexpected difference comes from the designed diplexer based on commercial filters. In fact, the design of the diplexer using the measured S-parameters instead of those given by the manufacturer would be more appropriate. Our approach (in progress) is now to redesign and optimize the diplexer's T-junction by using our measured S-parameters and, hence, to reduce the significant difference mainly observed at the lower frequency of the feeding circuit. Due to its only two parameters l 1 and l 2 , the simple structure of the T-junction would not be difficult to optimize by using the new measured filter S-parameters. The experimental results of the improved feeding circuit design will be presented in the conference.

IV. CONCLUSION

In this paper, a new compact feeding circuit was proposed for a triband antenna with circular polarization diversity. The two radionavigation bands of this antenna require a right hand circular polarization while the telemetry band requires a left hand one. Even if a new design of the diplexer using the measured S-parameters of its filters is necessary to: (1) reduce the insertion losses at the lower and upper frequency bands and (2) improve the phase deviation performance at the upper frequency band, the obtained results confirm the feasibility and also the difficulty of designing a compact feeding circuit for triband antennas with circular polarization diversity.

∠S 13 -∠S 12 (°) ∠S 14 -∠S 12 (°) ∠S 15 -∠S 12 (°)

f

Figure 1 .

 1 Figure 1. Feeding circuit architecture for circular polarization diversity

Figure 2 .

 2 Figure 2. (a) The diplexer configuration; (b) The optimized T junction

  plots the insertion loss and the channel isolation of the diplexer formed by the combination of the two filters (LFCN-1575 and HFCN-1810) and the optimized T-junction shown in Figure 2 (b).

Figure 3 .

 3 Figure 3. Simulated transmission coefficients of the optimized diplexer

Figure 4 .Figure 5 .

 45 Figure 4. Photographs of the fabricated compact feeding circuit for circular polarization diversity

Figure 6 .

 6 Figure 6. Measured phase differences between transmission coefficients: (a) ∠S13-∠S12 ; (b) ∠S14-∠S12 ; and (c) ∠S15-∠S12.

TABLE I TECHNICAL

 I REQUIREMENTS FOR THE GPS/GALILEO/MICROSAT TRIBAND ANTENNA

		Band 1	Band 2	Band 3
	Bands	E5a/L5 and E5b	Extended L1	Telemetry (TM)
	Systems	GPS/Galileo	GPS/Galileo	CNES MicroSat
	Center frequency	f1=1.197 GHz	f2=1.575 GHz	f3=2.245 GHz
	Bandwidth	50 MHz	32 MHz	90 MHz
	Polarization	Right-hand CP	Left-hand CP

TABLE II SIMULATED

 II AND MEASURED PHASE DIFFERENCES BETWEEN TRANSMISSION COEFFICIENTS AT THE THREE OPERATING FREQUENCIES OF THE TRIBAND ANTENNA

  1 =1.197 GHz

		Simulation	90.1	179.2	-90.6
		Measurement	80.8	172.1	-98.4
		Simulation	90	180.2	-89.8
	f 2 =1.575 GHz	Measurement	85.1	179.6	-86
		Simulation	-90.1	179.6	89.5
	f 3 =2.245 GHz	Measurement	-83.1	190	113.1

ACKNOWLEDGMENT

This work was supported by the French Space Agency (CNES) under grant No 70941/00. The authors wish to thank P. Marcoul and J. Rayssac for their efforts in the fabrication of the antenna feeding circuit.