Marius Bozga
email: marius.bozga@imag.fr

Mohamad Jaber
email: mohamad.jaber@imag.fr

Joseph Sifakis
email: joseph.sifakis@imag.fr

Source-to-Source Architecture Transformation for Performance Optimization in BIP

BIP (Behavior, Interaction, Priorities) is a component framework for constructing systems from a set of atomic components by using two kinds of composition operators: interactions and priorities.

In this paper we present a method that transforms the interactions of a component-based program in BIP and generates a functionally equivalent program. The method is based on the successive application of three types of source-to-source transformations: flattening of components, flattening of connectors and composition of atomic components. We show that the system of the transformations is confluent and terminates. By exhaustive application of the transformations, any BIP component can be transformed into an equivalent monolithic component. From this component, efficient C code can be generated.

The method combines advantages of component-based description such as clarity, incremental construction and reasoning with the possibility to generate efficient monolithic code. It has been integrated in the design methodology for BIP and it has been successfully applied to two non trivial examples described in the paper.

I. INTRODUCTION

Component-based systems 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 is the structure of a system, which 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.

An advantage of component-based systems is that they have logically clear descriptions. Nonetheless, clarity may be at the detriment of efficiency. Naive compilation of component-based systems results in great inefficiency as a consequence of the interconnection of components [START_REF] Loveman | Program improvement by source-to-source transformation[END_REF].

Source-to-source transformations have been considered as a powerful means for optimizing programs [START_REF] Hindman | Atomicity via source-to-source translation[END_REF], [START_REF] Vincent | Combining source-to-source transformations and processor instruction set extensions for the automated design-space exploration of embedded systems[END_REF]. In contrast to conventional optimization techniques, these can be applied for deeper semantics-preserving transformations which are visible to the programmer and subject to his direction and guidance.

Source-to-source architecture transformations transform a component-based system into a functionally equivalent system, by changing the structure of its architecture. They may affect performance and quality attributes. They are useful for find-ing functionally equivalent systems that meet different extrafunctional (platform dependent) requirements.

We study transformations for a subset of the BIP (Behavior, Interaction, Priority) language [START_REF] Basu | Modeling heterogeneous real-time components in BIP[END_REF], [START_REF] Bliudze | Causal semantics for the algebra of connectors[END_REF] where an architecture is characterized as a hierarchically structured set of components obtained by composition from a set of atomic components. In BIP, composition is parameterized by interactions and priorities between the composed components. In this paper we consider only composition by interactions. Composite components can be hierarchically structured. BIP has been used to model complex heterogeneous systems. It can be considered as an extension of C with powerful primitives for multiparty interaction between components. It has a compilation chain allowing the generation of C++ code from BIP models. The generated code is modular and can be executed on a dedicated platform consisting of an Engine which orchestrates the computation of atomic components by executing their interactions. Hierarchical description allows incremental reasoning and progressive design of complex systems. Nonetheless, it may lead to inefficient programs if structure is preserved at run time. Compared to functionally equivalent monolithic C programs, BIP programs may be more than two times slower. This overhead is due to the computation of interactions between components by the Engine.

The aim of the work is to show that it is possible to synthesize efficient monolithic code from component-based software described incrementally. We study source-to-source transformations for BIP allowing the composition of components and thus leading to more efficient code. These are based on the operational semantics of BIP which allows to compute the meaning of a composite component as a behaviorally equivalent atomic component.

A BIP component is characterized by its interface and its behavior. An interface consists of a set of ports used to specify interactions. Each port p i has an associated variable v pi which is visible when an interaction involving p i is executed. We assume that the sets of ports and variables of components are disjoint. The behavior of a composite component is obtained by composing the behavior of its atomic components (see Figure 1).

The behavior of atomic components is described as a Petri net extended with data and functions given in C. A transition of the Petri net is labelled with a trigger and a function f describing a local computation. A trigger consists of a guard g on (local) data and a port p through which synchronization is sought. For a given marking and data state, a transition can be executed if it is enabled for this marking, its guard g is true and an interaction involving p is possible. Its execution is atomic. It is initiated by the interaction and followed by the execution of f .

Composition consists in applying a set of connectors to a set of components. A connector is defined by: 1) its port p and the associated variable v p ; 2) its interaction defined by a set of ports p 1 , . . . , p n of the composed components ; 3) functions U and D 1 , . . . , D n , specifying the flow of data upstream and downstream, respectively (see Figure 1). The global behavior resulting from the application of a connector to a set of components is defined as follows.

An interaction p 1 , . . . , p n of the connector is possible only if for each one of its ports p i , there exists an enabled transition in some component labelled by p i . Its execution involves two steps:

1) the variable v is assigned the value U (v p1 , . . . , v pn ); 2) the variables v i associated with the ports p i are assigned values D i (v). The execution of an interaction is followed by the execution of the local computations of the synchronized transitions. In Figure 1, we provide a simple BIP model. It is composed of three atomic components, which compute integers exported through the variables v 1 , v 2 and v 3 . The connector defines the interaction (strong synchronization) between p 1 , p 2 and p 3 . As a result of this interaction, each component receives the maximum of the exported values. A composite component is obtained by successive application of connectors from a set of atomic components. It is a finite set of components equipped with an acyclic containment relation and a set of connectors such that: 1) minimal elements are atomic components; 2) if p is the port of a connector then its interaction consists only of ports of components contained in the component with port p. The containment relation defines for each component a level in the hierarchy. A component of level n is obtained by composing a set of components of lower level among which there is at least one component of level n-1. The semantics of a composite component is defined from the semantics of atomic components (components at level 0) and the semantics of composition by using connectors. It allows computing for a composite component, an atomic component with an equivalent global behavior.

The main contributions of the paper are the following. We define composite components in BIP and their semantics. We show how by incremental composition of the components contained in a composite component, a behaviorally equivalent component can be computed. This composition operation has been implemented in the BIP2BIP tool, by using three types of source-to-source transformations. A set of interacting components is replaced by a functionally equivalent component. By successive application of compositions, an atomic component can be obtained, that is a component with no interactions.

The transformation from a composite component to an atomic one is fully automated and implemented through three steps:

1) Component flattening which replaces the hierarchy on components by a set of hierarchically structured connectors applied on atomic components; 2) Connector flattening which computes for each hierarchically structured connector an equivalent flat connector; 3) Component composition which composes atomic components to get an atomic component. Using such a transformation allows to combine advantages of component-based descriptions such as clarity and reuse with efficient implementation. The generated code is readable and by-construction functionally equivalent to the componentbased model. We show through non trivial examples the benefits of this approach.

To the best of our knowledge, we have not seen major work on source-to-source transformations for componentbased frameworks. In contrast to other frameworks, component composition in BIP is based on operational semantics. Furthermore, composition can be expressed not only at execution level but also at source level. Similar component frameworks such as [START_REF] Balarin | Metropolis: An integrated electronic system design environment[END_REF], [START_REF] Eker | Taming heterogeneity -the ptolemy approach[END_REF] have well-defined denotational semantics. Nonetheless, it is not clear how to define component composition at source level from these semantics. There also exist many component frameworks without rigorous semantics. In this case, using ad hoc transformations, may lead easily to consistences e.g. transformations may not be confluent.

The paper is structured as follows. In section 2 we define the syntax for the description of structured components in BIP. In section 3, we define the semantics by successive application of the three source-to-source transformations. In section 4, we provide benchmarks for two examples: a MPEG encoder and a concurrent sorting program. In Section 5, we discuss other applications and future developments.

II. COMPONENT BASED CONSTRUCTION

We define atomic components and their composition in BIP.

Definition 1 (port): A port p[x] is defined by

• p -the port identifier, • x -the data variable associated with the port. An atomic component is a Petri net extended with data. It consists of a set of ports P used for the synchronization with other components, a set of transitions T and a set of local variables X. Transitions describe the behavior of the component. They are represented as a labelled relation on the set of control locations L.

Definition 2 (atomic component): An atomic component B is defined by: B = (P, L, T, X, {g τ } τ ∈T , {f τ } τ ∈T ), where,

• (P, L, T ) is a Petri net, that is -P is a set of ports, -L = {l 1 , l 2 , . . . , l k } is a set of control locations, -T ⊆ 2 L × P × 2 L is a set of transitions, • X = {x 1 , . . . , x n }
is a set of variables and for each τ ∈ T respectively g τ is a guard, an action X := f τ (X). We will use the following notations. For a transition τ ∈ T , we define its pre-set • τ (resp. post-set τ • ) as the set of the places which are direct predecessors (resp. successors) of this transition. Moreover, we use the dotted notation to denote the parameters of atomic components. For example, B.P means the set of ports of the atomic component B.

Figure 2 shows an example of an atomic component with two ports r 1 , t 1 , a variable a, and two control locations l 1 , l 2 . At control location l 1 , the transition labelled t 1 is possible. When an interaction through t 1 takes place, a random value is assigned for the variable a. This value is exported through the port r 1 . From the control location l 2 , the transition labelled r 1 can occur (the guard is true by default), the variable a is eventually modified and the value of a is printed. • p is the exported port of the connector γ,

• P = {p i [x i ]} i∈I is the support set of γ, that is, the set of ports that γ synchronize, • δ = (G, U, D) where, -G is the guard of γ, an arbitrary predicate G({x i } i∈I ), -U is the upward update function of γ of the form, x := F u ({x i } i∈I ), -D is the downward update function of γ of the form, ∪ pi x i := F d xi (x).
Figure 3 shows a connector with two ports p 1 , p 2 , and exported port p. Synchronization through this connector involves two steps: 1) The computation of the upward update function U by assigning to x the maximum of the values of x 1 and x 2 associated with p 1 and p 2 ; 2) The computation of the downward update function D by assigning the value of x to both x 1 and x 2 .

For a set of connectors Γ = {γ j } j∈J , we define the dominance relation → on Γ as follows :

γ i → γ j ≡ γ j .p ∈ γ i .P
That is, γ i dominates γ j means that the exported port of γ j belongs to the support set of γ i (see Figure 4).

p 1 [x 1 : int] p 2 [x 2 : int] p[x : int] G : true U : x := max(x 1 , x 2 ); D : x 1 := x; x 2 := x;
C ::= B | ({C i } i∈I , Γ, P ) where, • B is an atomic component, • {C i } i∈I is a set of constituent components, • P = (∪ i∈I C i .P ) ∪ (∪ j∈J γ j .p)
, is the set of ports of the component, that is P contains the ports of the constituent components and the exported ports of the connectors, • Γ = {γ j } j∈J is a set of connectors, such that, 1) (Γ, →) has no cycle, 2) ∪ j∈J γ j .P ⊆ P (P is defined above), 3) Each γ ∈ Γ uses at most one port of every constituent component, that is, ∀γ ∈ Γ, ∀i ∈ I,

|C i .P ∩ γ.P | ≤ 1.
That is, a component is either an atomic component B or a composite component obtained as the composition of a set of constituent components {C i } i∈I by using a set of connectors Γ = {γ j } j∈J . The restriction 3) is needed to prevent simultaneous firing of two or more transitions in the same atomic component, because they may operate a priori on the same set of variables. For example, consider the BIP component composed of two composite components shown in Figure 5. Each constituent component consists of three identical atomic components described in Figure 2, connected by using the connector described in Figure 3. Each atomic component generates an integer. Then it synchronizes with all the other atomic components. During synchronization the global maximal value is computed and each atomic component receives the maximum of the values generated.

Definition 6 (flat component): Composite component C is flat, iff the set of constituent component {C i } i∈I are atomic components. C t 1 C 1 C 2 γ 3 γ 2 γ 4 γ 5 r 1 r 2 r 4 r 5 t 2 t 3 t 4 t 5 t 6 r 3 r 6 p 3 p 5 γ 1 p 1 p 2 p 4
Fig. 5. Example 2

III. SEMANTICS (TRANSFORMATIONS)

We define the semantics of composite components by a set of transformations which successively transform them into atomic components. That is, they eliminate component hierarchy and the hierarchical connectors by computing the product behavior.

The transformation from a composite component to an atomic one is released through three steps: Component flattening, Connector flattening, Component composition. In this section, we describe the three transformations, and we illustrate them on Example 2 shown in Figure 5.

A. Component flattening

This transformation replaces the hierarchy on components by a set of hierarchically structured connectors applied on atomic components. Consider a composite component C, obtained as the composition of a set of components {C i } i∈I . The purpose of this transformation is to replace each non atomic component C j of C by its description. By successive applications of this transformation, the component C can be modelled as the set of its atomic components and their hierarchically structured connectors (see Figure 6).

Definition 7 (Component flattening): Consider a non atomic component C = ({C i } i∈I , Γ, P ) such that there exists a non atomic component

C j ∈ {C i } i∈I with C j = ({C jk } k∈K , Γ j , P j ). We define C[C j → Γ j ] as the com- ponent C = ({C i } i∈I ∪ {C jk } k∈K \ {C j }, Γ ∪ Γ j , P ).
Component flattening is defined by the following function:

F c (C) = C if C is flat F c (C[C j → Γ j ]) if C is not flat
Proposition 1: Component flattening is well-defined i.e., F c is a function which produces a unique result on every input component, and terminates in a finite number of steps.

Proof: Regarding the unicity of result, we can show that, if two constituent components respectively C j and C k can be replaced inside the composite component C, then the replacement can be done in any order and the final result is the same. That is, formally we have

C[C j → Γ j ][C k → Γ k ] = C[C k → Γ k ][C j → Γ j ].
The result follows immediately from the definition and elementary properties of union on sets.

Regarding termination, every transformation step decreases the overall number of composite components by one, so component flattening eventually terminates when all the components are atomic. Finally, let us remark that this transformation never increases the structural complexity of the transformed component. The overall set of atomic components as well as the overall set of the hierarchical connectors are preserved as such during the transformation.

B. Connector flattening

This transformation flattens hierarchical connectors. It takes two connectors γ i and γ j with γ i → γ j and produces an equivalent connector. We show in Figure 8 the composition of two connectors γ i and γ j . It consists in "glueing" them together on the exported port p j . For the composite connector, the update functions are respectively, the bottom-up composition of the upward update functions, and the top-down composition of the downward update functions. This implements a general twophase protocol for executing hierarchical connectors. First, data is synthesized in a bottom up fashion by executing upward update functions, as long as guards are true. Second, data is propagated downwards through downward update functions, from the top to the support set of the connector.

Definition 8 (Connector glueing): Given connectors

γ i = (p i [x i ], P i , δ i = (G i , U i , D i )
) and γ j = (p j [x j ], P j , δ j = (G j , U j , D j )) such that γ i → γ j we define the composition γ i [p j → γ j ] as a connector γ = (p, P, δ) where -

• p = p i , • P = P j ∪ P i \ {p j }, p j x i p i x j γ i (G i , U i , D i ) γ j (G j , U j , D j ) x i p i γ(G, U, D)
G = G j ∧ G i [F u j /x j ], -U = x i := F u i [F u j /x j ], -D = ∪ p k ∈Pj x k := F d j,x k [F d i,xi /x i ] ∪ ∪ p k ∈Pi\{pj } x k := F d i,x k . Let us introduce some notations. Let Γ = {γ i = (p i [x], P i , δ i )} i∈I
a set of connectors, and let P = {{p i } ∪ P i } i∈I the set of all used ports. We call a port p j ∈ P transient in Γ if it is both exported by some connector γ j from Γ and used by another connector γ i from Γ. Obviously, transient ports can be eliminated through connector glueing. For a transient port p j exported by a connector γ j , we will use the notation Γ[p j → γ j ] to denote the new set of connectors obtained by replacing thoroughly p j by its exporting connector γ j , formally:

Γ[p j → γ j ] = {γ | γ ∈ Γ, p j ∈ γ.ports, γ = γ j } ∪ {γ[p j → γ j ] | γ ∈ Γ, p j ∈ γ.ports}.
That is, all connectors (except γ j ) without p j in their support set are kept unchanged, while the others are transformed according to definition 8.

Definition 9 (Connector flattening):

Connector flattening is defined by the following function:

F γ (Γ) =          Γ if Γ is a set of flat connectors F γ (Γ[p j → γ j ]) if Γ is not a set of flat connectors, p j is a transient port of Γ Proposition 2:
Connector flattening is well-defined i.e., F γ is a function which produces a unique result on every set of connectors, and terminates in a finite number of steps.

Proof: Regarding the unicity of result, if p j and p k are two transient ports of Γ defined respectively by connectors γ j and γ k , then flattening can be done in any order, formally

Γ[p j → γ j ][p k → γ k ] = Γ[p k → γ k ][p j → γ j ].
The equality amounts to show that any connector γ of Γ, different from γ j and γ k gets transformed in the same way, independently of the order of application of the two transformations. This is easily shown, case by case, depending on the occurrence of ports p j and p k on the support of γ, γ j and γ k following the definition 8.

Regarding termination, flattening of connectors is applicable as long as there are transient ports. Moreover, it can be shown that, every flattening step reduces the number of transient ports by one -the one that is replaced by its definition. Hence, the flattening eventually terminates when no more transient ports exist, that is, Γ is a set of flat connectors. U : x 1 := max(max(max(r 1 .x, r 2 .x), r 3 .x), max(max(r 4 .x, r 5 .x), r 6 .x)); In a similar way to component flattening, this second transformation does not increase the structural complexity of the transformed components. The overall set of atomic components is preserved as such, whereas, the overall set of connectors is decreasing. However, the remaining connectors have an increased computational complexity, because they should integrate the guards and the data transfer of the eliminated ones.

G : true D : r 1 .x := x 1 ; r 2 .x := x 1 ; r 3 .x := x 1 ; r 4 .x := x 1 ; r 5 .x := x 1 ; r 6 .x := x 1 ; t 1 t 2 t 3 t 4 t 5 t 6 r 1 r 2 r 3 r 4 r 5 r 6 p 1 [x 1 ] p 1

C. Component composition

We present the third transformation which allows to obtain a single atomic component from a set of atomic components and a set of flat connectors. This transformation defines the composition of behaviors. Intuitively, as shown in Figure 11, the composition operation consists in "glueing" together transitions from atomic components that are synchronized through the interaction of some connector (interaction p 1 p 2 for this example). Guards of synchronized transitions are obtained by conjuncting individual guards and the guard of the connector. Similarly, actions of synchronized transitions are obtained as the sequential composition of the upward update function followed by the downward update function of the connector, followed by the actions of the components in an arbitrary order. • the set of ports P = ∪ γ∈Γ γ.p, • the set of places L = ∪ i∈I B i .L, • the set of variables X = (∪ i∈I B i .X) ∪ (∪ γ∈Γ γ.p.x),

p1 g1 f1 f2 g2 p2 p1 p2 p p = p1p2 g12 f12 f 12 = U 12 ; D 12 ; (f 1 ∪ f 2 ) g 12 = G 12 ∧ g 1 ∧ g 2 G12 U12 D12
• each transition in T corresponds to a set of interacting transitions {τ 1 , . . . , τ k } ⊆ ∪ i∈I T i such that ∪ k i=1 τ i .p = γ.P (γ ∈ Γ). We define the transition τ = (l, γ.p, l ′ ) where,

-l = • τ 1 ∪ . . . ∪ • τ k , -l ′ = τ • 1 ∪ . . . ∪ τ • k , -the guard g τ = ∧ k i=1 g τi ∧ γ i .δ.G, -the action X := f τ (X) with f τ = γ i .δ.U ; γ i .δ.D;
(∪ k i=1 f τi ). Figure 12 shows the Petri net obtained by composition of the atomic components of Figure 10 through the interaction r 1 r 2 r 3 r 4 r 5 r 6 .

In contrast to previous transformations, component composition may lead to an exponential blowup of the number of transitions in the resulting Petri net. This situation may happen if the same interaction can be realized by combining different transitions from each one of the involved components. For instance, the interaction p 1 p 2 can give rise to four transitions in the resulting Petri net if there are two transitions labeled by p 1 and p 2 in the synchronizing components. Nevertheless, in practice we are rarely faced to this situation, as in atomic

t 1 r = r 1 r 2 r 3 r 4 r 5 r 6 G : true a 1 =rand() t 2 a 2 =rand() a 3 =rand() a 4 =rand() a 5 =rand() a 6 =rand() t 6 t 3 t 4 t 5
F : U ; D; f f : print(a 1 ) ∪ print(a 2 ) ∪ print(a 3 ) ∪ print(a 4 ) ∪ print(a 5 ) ∪ print(a 6 )
D : a 1 := x 1 ; a 2 := x 1 ; a 3 := x 1 ; a 4 := x 1 ; a 5 := x 1 ; a 6 := x 1 ;

U : x 1 := max(max(max(a 1 , a 2 ), a 3 ), max(max(a 4 , a 5 ), a 6 )); components each port occurs at most in one transition (as in examples shown hereafter). In this case, the resulting Petri net has as many transitions as connectors in Γ.

IV. EXPERIMENTAL RESULTS

A. The BIP2BIP tool

These transformations have been implemented in the BIP2BIP tool, which is currently integrated in the BIP toolset [START_REF]BIP[END_REF] as shown in Figure 13.

The frontend of the BIP toolset is a parser that generates a model from a system described in the BIP language. The BIP language allows the description of hierarchically structured components as described in the previous sections. The functions and data are written in C. The language supports description of atomic components as extended Petri nets. It also allows the description of composite components by using connectors. From the generated model, the code-generator generates C++ code, executable on a dedicated middleware, the BIP Engine. The BIP Engine can perform execution and enumerative statespace exploration. The generated state graphs can be analyzed by using model-checking tools. The BIP2BIP tool is written in Java (∼4000 loc). It allows transformation of parsed models. It contains the following modules implementing the presented transformations.

• Component flattening : this module transforms a composite component to an equivalent one consisting only of atomic components of the initial model and a set of connectors. • Connector flattening : this module transforms an hierarchically structured connector to an equivalent flat one. • Component composition : this module transforms a set of atomic components and a set of flat connectors into an equivalent atomic component. By exhaustive application of these transformations, an atomic component can be obtained. From the latter, the codegenerator can generate standalone C code, which can be run directly without the Engine. In particular, all the remaining non-determinism in the final atomic component is eliminated at code generation by applying an implicit priority between It should be noted that the transformations also can be applied independently, to obtain models that respond to a particular user needs. For example, one may decide to eliminate only partially the hierarchy of components, or to compose only some components. The performance of BIP2BIP is quite satisfactory. For example, when applied to an artificially complex BIP model, consisting of 256 atomic components, composed by using 509 connectors with 7 levels of hierarchy, it takes less than 15 seconds to generate the corresponding C program.

B. Examples of transformation

For two examples, we compare the execution times of BIP programs before and after flattening. These examples show that it is possible to generate efficient C code from componentbased descriptions in BIP.

1) MPEG video encoder: In the framework of an industrial project, we have componentized in BIP an MPEG4 encoder written in C by an industrial partner. The aim of this work was to evaluate gains in scheduling and quality control of the componentized program. The results were quite positive regarding quality control [START_REF] Combaz | Symbolic quality control for multimedia applications[END_REF] but the componentized program was almost two times slower than the handwritten C program. We have used BIP2BIP to generate automatically C code from the BIP program as explained below (see Figure 14 Figure 15 shows the execution times for the initial handwritten C code, for the BIP program and the corresponding C code generated automatically by using the presented technique. Notice that the automatically generated C code and the handwritten C code have almost the same execution times. The advantages from the componentization of the handwritten code are multiple. The BIP program has been rescheduled as shown in [START_REF] Combaz | Symbolic quality control for multimedia applications[END_REF] so as to meet given timing requirements. Table I gives the size of the handwritten C code, the BIP model, as well of the generated C++ code from the BIP model C (1) and the generated C code from the BIP model after flattening C (2) . The time taken by the BIP2BIP tool to generate automatically C (2) is less than 1sec. 2) Concurrent Sorting: This example is inspired from a network sorting algorithm [START_REF] Ajtai | Sorting in c log n parallel steps[END_REF]. We consider 2 n atomic components, each of them containing an array of N values. We want to sort all the values, so that the elements of the first component are smaller than those of the second component and so on. We solve the problem by using incremental hierarchical composition of components with particular connectors.

f in f out f in f in f out f in f out f out f in f out in 1 in 2 f in f out f out f in
In Figure 16, we give a model for sorting the elements of 4 atomic components. The components C 1 and C 2 are identical. The pair (B 1 , B 2 ) is composed by using two connectors γ 1 and γ 2 to form the composite component C 1 . Each atomic component computes the minimum and the maximum of the values in its array. These values are then exported on the port p. The connector γ 1 is used to compare the maximum value of B 1 with the minimum value of B 2 , and to permute them if the maximum is bigger than the minimum value.

When the maximum value of the B 1 is smaller than the minimum value of B 2 , that is the components are correctly sorted, then the second connector γ 2 is triggered. It is used to export the minimum value of B 1 and the maximum value of B 2 to the upper level. At this level the same principle is applied to sort the values of the composite components C 1 and C 2 . This pattern can be repeated to obtain arbitrary higher hierarchies (see Figure 17). ... ... ... ...

C 2 C 1 γ 1 γ 2 B 1 B 2 γ 1 γ 2 p(M in, M ax) r(M in, M ax) q(M in, M ax) p(M in, M ax) q(M in, M ax) G : p.M ax > q.M in U :
G : p.M ax <= q.M in U : M in := p.M in; M ax := q.M ax; D : p.M in := M in; q.M ax := M ax; D : x := p.M ax; p.M ax := q.M in; q.M in := x;

Fig. 16. Concurrent Sorting

Figure 18 shows the execution times for the hierarchically structured BIP program and for the corresponding C code generated automatically by using the presented technique. The paper shows that it is possible to reconcile componentbased incremental design and efficient code generation by applying a paradigm based on the combined use of 1) a high level modelling notation based on well-defined operational semantics and supporting powerful mechanisms for expressing structured coordination between components; 2) semanticspreserving source-to-source transformations that progressively transform architectural constraints between components into internal computation of product components.

BIP has already successfully been used for the componentization of non trivial systems such as the controller of the DALA robot [START_REF] Basu | Incremental component-based construction and verification of a robotic system[END_REF]. This allowed building componentbased models for which enhanced analysis and verification is possible by using tools such as D-Finder [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF] for compositional verification. The use of the BIP2BIP tool allows to reduce overheads in execution time by reducing modularity introduced by the designer when it is not necessary at implementation level.

This paradigm opens the way to the synthesis of efficient monolithic software which is correct-by-construction by using the design methodology supported by BIP. The methodology is currently under study, and involves the following steps:

1) The system (software) to be designed is decomposed into components. The decomposition can be represented as a tree which shows how the system can be obtained as the incremental composition of components. Its root is the system and its leaves correspond to atomic components; 2) Description of the behavior of the atomic components; 3) Description of composite components as the composition of atomic components by using only connectors and priorities. This is possible because BIP is expressive enough for expressing any kind of coordination by using only architectural constraints [START_REF] Bliudze | A notion of glue expressiveness for component-based systems[END_REF]. Along steps 2) and 3) it is possible by using the D-Finder tool, to generate and/or check invariants of the components and validate their properties. The methodology provides sufficient conditions for preserving the already established properties of the sub-systems along the construction.

The BIP2BIP tool is an essential feature of the BIP toolset. Further developments will focus on source-to-source transformations for BIP programs with priorities by following a similar flattening principle. In fact, priority rules can be compiled in the form of restrictions of the guards of components. We plan to use BIP2BIP, for optimizing distributed implementations [START_REF] Basu | Distributed semantics and implementation for systems with interaction and priority[END_REF], in particular to generate monolithic C code for subsystems implemented on the same site.

Fig. 1 .

 1 Fig. 1. Example 1

Fig. 2 .

 2 Fig. 2. An example of an atomic component in BIP Definition 3 (connector): A connector γ = (p[x], P, δ) is defined as follows• p is the exported port of the connector γ,• P = {p i [x i ]} i∈I is the support set of γ, that is, the set of ports that γ synchronize,• δ = (G, U, D) where,-G is the guard of γ, an arbitrary predicate G({x i } i∈I ), -U is the upward update function of γ of the form,x := F u ({x i } i∈I ), -D is the downward update function of γ of the form, ∪ pi x i := F d xi (x). Figure3shows a connector with two ports p 1 , p 2 , and exported port p. Synchronization through this connector involves two steps: 1) The computation of the upward update function U by assigning to x the maximum of the values of x 1 and x 2 associated with p 1 and p 2 ; 2) The computation of the downward update function D by assigning the value of x to both x 1 and x 2 .For a set of connectors Γ = {γ j } j∈J , we define the dominance relation → on Γ as follows :

Fig. 3 .Fig. 4 .

 34 Fig. 3. An example of a connector in BIP

Fig. 6 .Fig. 7 .

 67 Fig. 6. Component flattening By applying to Example 2 the transformation C[C 1 → {γ 2 , γ 3 }] then C[C 2 → {γ 4 , γ 5 }], we obtain the new component in Figure 7.

Fig. 8 .

 8 Fig. 8. Connector glueing

Fig. 9 .

 9 Fig. 9. Connector wiring for Example 2

Fig. 10 .

 10 Fig. 10. Result for connector flattening for Example 2

Fig. 11 .

 11 Fig. 11. Component composition Definition 10 (Component composition): Consider a component C = ({B i } i∈I , Γ, P ) such that ∀i ∈ I B i is an atomic component and Γ is a set of flat connectors. We define the composition Γ({B i } i∈I ) as component B = (P, L, T, X, {g τ } τ ∈T , {f τ } τ ∈T ) defined as follows:

Fig. 12 .

 12 Fig. 12. Component composition for Example 2

Fig. 13 .

 13 Fig. 13. BIP toolset: General architecture

  ). The BIP program consists of 11 atomic components, and 14 connectors. It uses the data and the functions of the initial handwritten C program. It is composed of two atomic components and one composite component. The atomic component GrabFrame gets a frame and produces macroblocks (each frame is split into N macroblocks of 256 pixels). The atomic component OutputFrame produces an encoded

Fig. 14 .

 14 Fig. 14. MPEG4 encoder

Fig. 15 .

 15 Fig. 15. Execution time for the MPEG4 Encoder

Fig. 17 .

 17 Fig. 17. Concurrent Sorting

Fig. 18 .

 18 Fig. 18. Execution time for concurrent sorting V. CONCLUSION

  Table II shows the size in lines of code of the BIP program, the component-based C++ corresponding program and the C code for 4, 8, 16, 32 and 64 atomic components. The size of the BIP model changes only linearly with n.

	n		BIP C (1)	C (2)
	2	loc	112	360	400
	3	loc	120	400	620
	4	loc	128	440	1100
	5	loc	136	480	1850
	6	loc	144	520	2850
			TABLE II
	CODE SIZE IN LOC FOR CONCURRENT SORTING

p 1 , v 1 p 2 , v 2 p 3 , v 3 p, v p 1 , v 1 p 2 , v 2 p 3 , v 3 p, v G : true U : v := M ax(v1, v2, v3); D1 : v1 := v; D2 : v2 := v; D3 : v3 := v;


Saddek Bensalem

Marius Bozga

Thanh-Hung Nguyen

Joseph Sifakis

D-Finder: A Tool for Compositional Deadlock Detection and Verification

D-Finder tool implements a compositional method for the verification of component-based systems described in BIP language encompassing multi-party interaction. For deadlock detection, D-Finder applies proof strategies to eliminate potential deadlocks by computing increasingly stronger invariants.

Methodology

Compositional verification techniques are used to cope with state explosion in concurrent systems. The idea is to aply divide-and-conquer approaches to infer global properties of complex systems from properties of their components. Separate verification of components limits state explosion. Nonetheless, components mutually interact in a system and their behavior and properties are inter-related. This is a major difficulty in designing compositional techniques. As explained in [START_REF] Kupferman | Modular model checking[END_REF], compositional rules are in general of the form

B 1 < Φ 1 >, B 2 < Φ 2 >, C(Φ 1 , Φ 2 , Φ) B 1 B 2 < Φ > (1)
That is, if two components with behaviors B 1 , B 2 meet individually properties Φ 1 , Φ 2 respectively, and C(Φ 1 , Φ 2 , Φ) is some condition taking into account the semantics of parallel composition operation and relating the individual properties with the global property, then the system B 1 B 2 resulting from the composition of B 1 and B 2 will satisfy a global property Φ.

-Compositional verification by assume-guarantee . In this approach properties are decomposed into two parts. One is an assumption about the global behavior of the environment of the component; the other is a property guaranteed by the component when the assumption about its environment holds. This approach has been extensively studied (see for example [START_REF] Alur | Reactive modules[END_REF][START_REF] Abadi | Conjoining specifications[END_REF][START_REF] Clarke | Compositional model checking[END_REF][START_REF] Chandy | Parallel program design: a foundation[END_REF][START_REF] Grumberg | Model checking and modular verification[END_REF][START_REF] Mcmillan | A compositional rule for hardware design refinement[END_REF][START_REF] Pnueli | In transition from global to modular temporal reasoning about programs[END_REF][START_REF] Stark | A proof technique for rely/guarantee properties[END_REF]). Many issues make the application of assume-guarantee rules diffcult. These are discussed in detail in a recent paper [START_REF] Cobleigh | Breaking up is hard to do: An evaluation of automated assume-guarantee reasoning[END_REF] which provides an evaluation of automated assume-guarantee techniques. The main difficulties are finding decompositions into sub-systems and choosing adequate assumptions for a particular decomposition.

-D-Finder's approach to compositional verification . We present a different approach for compositional verification of invariants based on the following rule:

{B i < Φ i >} i , Ψ ∈ II( γ {B i } i , {Φ i } i ), ( i Φ i ) ∧ Ψ ⇒ Φ γ {B i } i < Φ > (2)
The rule allows to prove invariance of Φ for systems obtained by using a n-ary composition operation parameterized by a set of interactions γ. It uses global invariants which are the conjunction of individual invariants of components Φ i and an interaction invariant Ψ . The latter expresses constraints on the global state space induced by interactions between components. It can be computed automatically from abstractions of the system to be verified. These are the composition of finite state abstractions B α i of the components B i with respect to their invariants Φ i . They can be represented as a Petri net whose transitions correspond to interactions between components. Interaction invariants correspond to traps [START_REF] Peterson | Petri Net theory and the modelling of systems[END_REF] of the Petri net and are computed symbolically as solutions of a set of boolean equations. Figure 1 illustrates the method for a system with two components, invariants Φ 1 and Φ 2 and interaction invariant Ψ . Our method differs from assumeguarantee methods in that it avoids combinatorial explosion of the decomposition and is directly applicable to systems with multiparty (not only binary) interactions. Furthermore, it needs only guarantees for components. It replaces the search for adequate assumptions for each component by the use of interaction invariants. These can be computed automatically from given component invariants (guarantees). Interaction invariants correspond to a "cooperation test" in the terminology of [START_REF] Apt | A proof system for communicating sequential processes[END_REF] as they allow to eliminate product states which are not feasible by the semantics.

1.1

Checking Deadlock-freedom and Invariance Properties D-Finder provides a method for automated verification of component-based systems described in BIP (Behavior-Interaction-Priority) language [START_REF] Basu | Modeling heterogeneous real-time components in bip[END_REF]. In BIP, a system is the composition of a set of atomic components which are automata extended with data and functions written in C. To prove a global invariant Φ for a system γ(B 1 , . . . , B n ), obtained by composing a set of atomic components B 1 , ..., B n by using a set of interactions γ, we use the rule (2) above, where

B i < Φ i > means that Φ i is an invariant of component B i and Ψ is an interaction invariant of γ(B 1 , . . . , B n ) computed automatically from Φ i and γ(B 1 , . . . , B n ).
A key issue in the application of this rule is finding component invariants Φ i . If the components B i are finite state, then we can take Φ = Reach(B i ), the set of reachable state of B i , or any upper approximation of Reach(B i ). If the components are infinite state, Reach(B i ) is approximated using techniques presented in [START_REF] Lakhnech | Incremental verification by abstraction[END_REF][START_REF] Bradley | Checking safety by inductive generalization of counterexamples to induction[END_REF].

-Checking Invariance Properties. We give a sketch of a semi-algorithm allowing to prove invariance of Φ by iterative application of the rule (2). The semi-algorithm takes a system γ(B 1 , . . . , B n ), Init and a predicate Φ. It iteratively computes invariants of the form

X = Ψ ∧ ( n i=1 Φ i )
where Ψ is an interaction invariant and Φ i an invariant of component B i . If X is not strong enough for proving that Φ is an invariant (X ∧ ¬Φ = f alse) then either a new iteration with stronger Φ i is started or we stop. In this case, we cannot conclude about invariance of Φ.

-Checking Deadlock-Freedom. Checking global deadlock-freedom of a system γ(B 1 , . . . , B n ) is a particular case of proving invariants -proving invariance of the predicate ¬DIS, where DIS is the set of the states of γ(B 1 , . . . , B n ) from which all interactions are disabled.

Generating Component Invariants and Interaction Invariants

D-Finder provides methods for computing component invariants, particulary useful for checking deadlock-freedom. It also provides a general method for computing interaction invariants for γ(B 1 , . . . , B n ) from a given set of component invariants Φ i .

-Computing Component Invariants. Invariants for atomic components are generated by simple forward analysis of their behavior. A key issue is efficient computation of such invariants as the precise symbolic computation of reachable states requires quantifier elimination. An alternative to quantifier elimination is to compute over-approximations based on syntactic analysis of the predicates occuring in guards and actions. In this case, the obtained invariants may not be inductive. D-Finder uses different strategies which allow to derive local assertions, that is, predicates attached to control locations and which are satisfied whenever the computation reaches the corresponding control location. A more detailed presentation, as well as the techniques implemented in D-Finder for generating component invariants are given in [START_REF] Bensalem | Automatic generation of invariants[END_REF][START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF]. -Computing Interaction Invariants. Interaction invariants express global synchronization constraints between atomic components. Their computation consists of the following steps. 1) For given component invariants Φ i of the atomic components B i , we compute a finite-state abstractions B αi i of B i where α i is the abstraction induced by the elementary predicates occuring in Φ i . This step is necessary only for components B i which are infinite state. 2)

The system γ(B α1 1 , • • • , B αn n ) which is an abstraction of γ(B 1 , • • • , B n )
, can be considered as a safe Petri net. The set of the traps of the Petri net defines a global invariant which we compute symbolically. 3) The concretization of this invariant gives an interaction invariant of the initial system. D-Finder consists of a set of modules interconnected as shown in Figure 2.

It takes as input a BIP program and progressively find and eliminate potential deadlocks. It basically works as follows. First, it constructs the predicate characterizing the set of deadlock states (DIS generation module). Second, iteratively, it constructs increasingly stronger local invariants of components (Φ i generation module) and using them, finer finite state abstractions and increasingly stronger global interaction invariants (Abstraction and Ψ generation module). Third, it checks deadlock freedom by checking satisfiabilty of ∧Φ i ∧ Φ ∧ Dis (satisfiability module). If it succeeds, the system is proven deadlock-free, else it may continue or gives up, according to the user choice. For doing all this, D-Finder is con-

Φ i Ψ V Φ i ∧ Ψ ∧ DIS V Φ i Ψ generation
Fig. 2. DeadlockFinder tool nected with several external tools. It uses Omega [START_REF] Team | The omega library[END_REF] for quantifier elimination and Yices [START_REF] Dutertre | A fast linear-arithmetic solver for DPLL(T)[END_REF] for checking satisfiability of predicates. It is also connected to the state space exploration tool of the BIP platform, for finer analysis when the heuristic fails to prove deadlock-freedom. We provide non trivial examples showing the capabilities of D-Finder as well as the efficiency of the method.

Experimentation and Concluding remarks

We provide experimental results for four examples. The first example is Utopar, an industrial case study of the European Integrated project SPEEDS (http://www.speeds.eu.com/) about an automated transportation system. A succinct description of Utopar can be found at http://www.combest.eu/home/?link=Application2. The system is the composition of three types of components: autonomous vehicles, called U-cars, a centralized Automatic Control System and Calling Units. The latter two types have (almost exclusively) discrete behavior. U-cars are equipped with a local controller, responsible for handling the U-cars sensors and performing various routing and driving computations depending on users' requests. We analyzed a simplified version of Utopar by abstracting from data exchanged between components as well as from continuous dynamics of the cars. In this version, each U-Car is modeled by a component having 7 control locations and 6 integer variables. The Automatic Control System has 3 control locations and 2 integer variables. The Calling Units have 2 control locations and no variables. In the second example, we consider Readers-Writer systems in order to evaluate how the method scales up for components without data. The third example is Gas Station in order to compare with other compositional method assume-guarantee [START_REF] Cobleigh | Breaking up is hard to do: An evaluation of automated assume-guarantee reasoning[END_REF]. Finally, as a last example, we consider Dinning Philosophers which is a well-known classical example.

The table below provides an overview of the experimental results obtained for these examples. In this table, n is the number of BIP components in the example, q is the total number of control locations, x b (resp. x i ) is the total number of boolean (resp. integer) variables, D ci is the number of deadlock configurations remaining in DIS ∧ CI ∧ II and t is the total time for computing invariants and checking for satisfiability of DIS ∧ CI ∧ II. Detailed results are available at http://www-verimag.imag.fr/˜thnguyen/tool. We did some comparison with some well-known monolithic verification tools such as NewSMV (NuSMV) and Spin. All the experimentations are done on a Linux machine Intel Pentium 4 3.0 GHz and 1G Ram.

  Fig. 1.

Fig. 3 .

 3 Fig. 3. Comparison with NuSmv and Spin on Dinning Philosopher

Fig. 4 .

 4 Fig. 4. Comparison with NuSmv on Gas Station

The first comparison between NuSmv, Spin and DFinder is on Dinning Philosopher example. We increase the number of Philosophers and compare the verification time between these three tools (figure 3). In this figure , Spin runs out of memory at the size 17 (Philosophers); NuSmv runs out of memory at the size 150 while DFinder can go much further until the size 3000.

The second comparison between NuSmv and DFinder is on Gas Station example. We consider a system with 3 pumps and increase the number of customers. The comparison of verification time is in figure 4. In this figure, NuSmv runs out of memory at the size 180 (Customers) while DFinder can go much further until the size 3000.