Ludovic Henrio
email: ludovic.henrio@cnrs.fr

Oleksandra Kulankhina
email: oleksandra.kulankhina@inria.fr

Dongqian Liu

Eric Madelaine
email: eric.madelaine@inria.fr

Verifying the correct composition of distributed components: Formalisation and Tool *

This article provides formal definitions characterizing well-formed composition of components in order to guarantee their safe deployment and execution. Our work focuses on the structural aspects of component composition; it puts together most of the concepts common to many component models, but never formalized as a whole. Our formalization characterizes correct component architectures made of functional and non-functional aspects, both structured as component assemblies. Interceptor chains can be used for a safe and controlled interaction between the two aspects. Our well-formed components guarantee a set of properties ensuring that the deployed component system has a correct architecture and can run safely. Finally, those definitions constitute the formal basis for our Eclipsebased environment for the development and specification of component-based applications.

Introduction

Designing safe distributed component-based software systems is a challenging task including a wide range of issues ranging from the safe composition of components to the applications performance and reliability. This work focuses on the correctness of component assembly which is a strong prerequisite for correct deployment and execution of components. We target component models which are hierarchical [START_REF] Hnětynka | Dynamic reconfiguration and access to services in hierarchical component models[END_REF] and provide runtime control on the component application. In component-based software engineering, this last feature, i.e. the control and management of the system architecture and of the business application, is part of what is generally called non-functional concern. More precisely, non-functional aspects may cover many aspects, from security, latency, time aspects, energy or cost, to management concerns including mechanisms for dynamic reconfiguration, fault-tolerance, load balancing, self-healing, or more elaborate autonomic behaviours. In this paper, we are essentialy considering the second category, i.e. the management aspects, and we want to support the ability to design non-functional aspects themselves as a component system, which ensures a clear design of the whole application. The business logic of the application is called the functional aspect.

Our main goal is to provide a clear and formal definition of component assemblies and a set of logic predicates ensuring the correctness of component composition and component interconnection. In particular our predicates ensure a strong separation of concerns: a non-functional component can only interact with non-functional components, or with non-functional interfaces of business components. This way, each binding between components only transmits either functional or non-functional invocations. However a clean interaction between these concerns is highly desirable: we introduce interceptors, which are special components providing interaction between functional and non-functional elements. They can observe functional invocations and trigger a reaction of the control part of the component. In the other direction, non-functional components can influence the functional behavior by modifying its behaviour in two ways: either through reconfiguration, i.e. modification at runtime of the component architecture, or by changing parameters, i.e. component attributes, that will influence the functional behaviour.

In this paper we focus on one specific component model: the Grid Component Model (GCM) [START_REF] Baude | GCM: A Grid Extension to Fractal for Autonomous Distributed Components[END_REF]. GCM allows the construction of distributed hierarchical applications with asynchronous group communications and strong separation between business logic and control parts of a system. To our knowledge, GCM is one of the only established component models that provides specific features for managing complex software systems, and that offers architectural artifacts and methodological approaches to organise the control part of such applications. GCM-based systems can be designed and modeled using the Ver-Cors tool 1 ; An XML-based Architecture Description Language (ADL) file, describing the architecture of the application, can then be generated by VerCors and used to build and deploy the GCM application, using the GCM/ProActive execution environment [START_REF] Baude | Programming distributed and adaptable autonomous components-the GCM/ProActive framework[END_REF]. We started from the formal representation of GCM architecture given in [START_REF] Ameur-Boulifa | Behavioural Semantics for Asynchronous Components[END_REF] and introduced a number of important concepts. This article has the following new contributions:

• First, we provide a formal representation of component architectures including a flexible set of constructs for the definition of non-functional part of an application which has never been formalized before. The business logic and control parts of a system are strongly separated. • Second, we formalize the notion of interceptors and define a number of auxiliary predicates insuring their safe composition with the rest of the system. • Third, we specify a set of key properties for component architecture, those properties are guaranteed for any component assembly that is well-formed according to the rules defined in Section 3.4. After validation of these rules, we garantee that the generated ADL code is correct, in the sense that building the component-based application by running the GCM component factory will terminate successfully with no runtime error. Additionally, the properties we exhibit are necessary prerequisite for the correct execution and the reconfigurability of the system; those properties include uniqueness of naming, separation of concerns, and communication determinacy. • Finally, we implement an environment allowing graphical modeling and validity check for the distributed systems architecture with respect to the proposed formalization.

The purpose of our formalization is threefold. First it is component model independent: by formalizing the correctness rules, we make them applicable outside the scope of GCM, and of our tools. Second, it makes it easier to re-use the formalization for different purposes, e.g. to implement different checkers, or encode it in a theorem prover. Finally, it allows reasoning on the properties ensured by the component model: properties of Section 3.5 can be formally proven from the definition of component correctness.

This paper is organized as follows. Section 2 describes the Grid Component Model and our modeling platform. Section 3 presents the formalization of GCM architecture and of correct architecture. Section 4 describes how to adapt our formalism to other features or other component models and presents an overview of the related work. Section 5 describes our environment for modeling GCM-based systems.

GCM

GCM [START_REF] Baude | GCM: A Grid Extension to Fractal for Autonomous Distributed Components[END_REF] is a component model targeting large-scale distributed applications. It is an extension of the Fractal [START_REF] Bruneton | The Fractal Component Model and Its Support in Java. Software Practice and Experience, special issue on Experiences with Auto-adaptive and Reconfigurable Systems[END_REF] component model; we summarize below the architectural aspects of GCM, and its main advantages. We also provide an illustrative example of a real-world application built using GCM.

A GCM component application is a composition of components, interfaces and bindings. GCM is a hierarchical component model, consequently there are two types of components in GCM: primitive and composite ones. Composite components are used to compose other components while the primitive ones are the leaves of the composition hierarchy. More precisely, a composite component (Application in Figure 1) is made of two parts: membrane (gray part) and content (white part). The content contains the sub-components dealing with the functional aspects. The membrane includes sub-components which are responsible for everything besides business logic: control, monitoring, structural reconfiguration, etc. A primitive component is similar except that the content is not known (e.g., Front-end, Repository and W1 in Figure 1). It encapsulates some business code. It has a list of methods, which it can execute.

The communication between components is performed in the form of method invocation. In Fractal and GCM interfaces are similar to object interfaces characterized by a set of methods that can transit through this interface. There are client and server interfaces. Client interfaces (e.g. C1) emit the methods invocations. Server interfaces (e.g. S1) receive them. We also distinguish the interfaces dealing with the business logic (functional interfaces drawn in blue color) and the ones dealing with the control of an application (non-functional ones colored in green). A binding is an arrow from a client to a server interface, communications between components follow those bindings.

In GCM, the interfaces can be attached to the components. An interface that is accessible from the exterior of a component is called an external interfaces (e.g. S1). When an interface is reachable from the inside of a component, i.e. from its content, it is called an internal interfaces (e.g. M1). The membrane of a component can also have internal interfaces, but they are not declared explicitly. The set of internal interfaces of a membrane is represented by the union of two other sets: all the external interfaces of the component containing the membrane and all the internal interfaces of the content inside the component. All the interfaces are taken with the same properties, but with an opposite role (e.g. a server interface becomes a client one and vice-verse). Figure 2 illustrates the (implicite) internal interfaces of a membrane, displayed in red color.

Figure 1 shows an illustrative example taken from [START_REF] Baude | Programming distributed and adaptable autonomous components-the GCM/ProActive framework[END_REF]. It represents the architecture of a real-world GCM system implementing an autonomic master-slave application treating incoming requests in parallel. Component Front-end is a front-end of the application. It receives the job-requests from the user. The requests are, then, processed by the workers (W1 and W2). The results are sent to the repository represented by a component Repository. The application reconfigures itself autonomically: the workers are added or removed depending on the system workload. This is realized by the sequence of components: Collector, Analyser, Planner, and Executor. This sequence follows the principle of the MAPE model for autonomic computing. The Monitoring components (Monitor, In Monitor) in the membranes of the workers and in Application monitor different metrics such as served requests per minute, and available disk space, CPU, and memory. Component Collector gathers the information from the Monitoring components. It sends the information to the component Analyser. Based on the received information, Analyser sends an alarm to the Planning component (Planner). The former one plans the reconfiguration, which is enacted by the Execution component (Executor).

GCM provides the following features to the applications:

Strong separation of concerns The functional part of a GCM application can be separated from the control part thanks to the separation of a composite component into a membrane and a content and to the usage of functional and non-functional interfaces. In the provided example, the components performing the reconfiguration (Collector, Analyser, Planner, Executor) are separated from the ones responsible for the business logic (W1, W2, Repository). This separation ensures, as much as possible, the independence of the business code -the request treatment in the example -from the management code -the sequence of control components in the example. Reconfiguration In GCM, the architecture of the application can be accessed and modified at runtime; this is realized in the example by the execution component. It allows the non-functional concern to modify the structure of the functional (and the non-functional) part of the component application, and thus to change its behavior. Interceptors Sometimes, some information should be shared between the functional part and the controllers of the application. Interceptors are specific components inside the membrane that can intercept the flow of functional calls in order to trigger reaction from the non-functional aspects. For example, in the use-case, Monitor components are monitoring the number of job-requests sent to the worker, they illustrate very well what is an interceptor. In the membrane, functional interfaces are directly connected, however one or several interceptors can be inserted within such a binding and interact with other non-functional components (see the non-functional binding between Monitor and Collector in the example). One-to-many / many-to-one communications GCM also targets large-scale distributed systems where an invocation is to be broadcast to several entities or simply sent to different servers to ensure loadbalancing. For this, GCM introduces one-to-many client interfaces, called multicast interfaces like the interface M1 of Figure 1. From a structural point of view the particularity of multicast interfaces is that they can be connected to several server interfaces. Symmetrically, GCM introduce gathercast server interfaces for synchronizing many-to-one communications, typically waiting for a number of communications before triggering a communication. Our main contribution here is a formal definition and specification of the non-functional aspects of components; we will also see how we formally insure the separation of concerns and how we formally specify the interceptors.

VerCors

VerCors is a platform for the specification, analysis, verification, and validation of the GCM-based applications. The principle of the tool is illustrated in Figure 3. First, a user specifies the architecture of a GCM-based application, the signature of its interfaces, and the behavior of the primitive components using VerCors Component Editor (VCE). Then, from these descriptions the behavioral model of an application is generated (ADL2N) in a form of a dedicated behavioral semantic model: a parameterized networks of synchronized automata (pNets). This semantic model is transformed by abstraction functions (ABS*), until reaching a finite model suitable for model-checking. Finally, the resulting behavioral model is translated (N2F) into a set of languages used by a Model Checker (CADP tool [START_REF] Garavel | CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF]). Finally, the Model Checker verifies the correctness of the model with respect to a set of temporal logic properties (user requirements) and in the case of detected errors it provides their description.

Once the requirements have been proven correct on the VCE specification, the user can generate the set of files (ADL for the Architecture Description, IDL for the Interface definition in the form of Java interfaces). Then naturally, user has to provide java classes implementing the service methods of the primitive components. These files are processed by the GCM component factory to build an executable application, that is executed with the GCM/ProActive execution environment.

In this paper we focus only on the structural aspect of GCM-based applications which is covered by the VerCors Component Editor. Our purpose is to ensure that the components provided to the rest of the tool chain are well-formed; for this we describe below a set of rules that must be satisfied to ensure the Using VerCors tool, we were able to design the architecture of the example illustrated at Figure 1, check its static semantic correctness properties, generate ADL files and deploy the corresponding application.

Formalization

The purpose of this section is to define formally well-formed components and exhibit their properties.

Structure

We start with the formal model representing the GCM architecture. First, we discuss the core elements. Second, we formalize the non-functional part of the GCM architecture.

Core

In this section we define the core elements of GCM, namely: Interfaces, Components and Bindings. Their formalization is given in Table 1. We denote A i∈I i a set of elements A i indexed in a set I. The formal definition is not provided for some elements of the table, because they are the terminal symbols. Such elements are presented in different font (e.g. Name, Type, NF).

Each server (SItf) or client (CItf) interface is characterized by three attributes: Name is the name of an interface; MSignatures represent the methods which can be served by a server interface or called by a client interface, with their signature; Nature defines if it is a functional or a non-functional interface.

Each component is characterized by its name, the sets of external client and server interfaces, and its membrane. A primitive component also includes a set of local methods. A composite component includes its content with a specific structure. The membrane is responsible for the non-functional activity. The content is defined by the sets of internal client and server interface, sub-components and a set of bindings located inside the content.

Function name Function Definition Sym

Sym :

Itf → Itf Itf GetIt f : (Membr | Cont | Comp) → Itf GetIt f (X : Comp | Cont) ::= SIt f (X) ∪CIt f (X) GetIt f (X : Membr) ::= Sym Itf(Parent(X)) ∪ Itf(Cont(Parent(X)) GetSrc GetSrc : Binding × (Membr | Cont) → Itf GetSrc((Src, Dst), ctnr) ::= itf s.t. Name(itf) = Name(Src)∧ itf ∈ Itf(ctnr) ∧ Role(itf) = C, i f Src = This.Name itf ∈ Itf(comp).(comp ∈ ctnr ∧ Name(comp) = CName), i f Src = CName.Name GetDst GetDst : Binding × (Membr | Cont) → Itf GetDst((Src, Dst), ctnr) ::= itf s.t. Name(itf) = Name(Dst)∧ itf ∈ Itf(ctnr) ∧ Role(itf) = S, i f Dst = This.Name itf ∈ Itf(comp).(comp ∈ ctnr ∧ Name(comp) = CName), i f Dst = CName.Name Parent Parent : (Itf | Comp | Membr | Cont) → Membr | Cont | Comp
Table 2: Auxiliary functions A binding connects two interfaces. It is described as a couple of names defining its source and target interfaces. Each name consists of two parts. The first part describes the container of the interface, either the name of a sub-component or the identifier This. The second part is the name of the interface itself.

Non-functional aspects

The Nature property of interfaces can be either functional (F) or non-functional (NF). The membrane is the part of a component which is responsible for the non-functional aspect of an application. Its formalization is given in the bottom of Table 1. The bindings (Binding l∈L l ) are the connections between the interfaces in the membrane. A membrane can contain a set of sub-components (Comp k∈K k ). The interceptors are recognized in this set essentially from their binding patterns, all the other components in a membrane are simple controllers.

Auxiliary functions

In this section we introduce the auxiliary functions used for the GCM architecture well-formness formalization. The auxiliary functions are given in Table 2.

First, we use auxiliary functions providing the access to the attributes of the interfaces and components. For example, the Nature(itf : Itf) function returns the nature of an interface, Binding(membr : Membr) returns the set of bindings in a membrane. The definitions of such functions are straightforward and we omit them in Table 2.

Second, the symmetry function (Sym) takes an interface as an input and returns an interface with exactly the same properties but with an opposite role: a client (. . .) C interface becomes a server (. . .) S one and symmetrically. to Third, we introduce a GetItf function. It takes a container (a component, a membrane or a content) as an input and computes the set of interfaces stored by it. If its argument is a component or a content, then its result is the union of its server and client interfaces sets. The case of membrane is more complicated as its internal interfaces are not explicitly defined. Instead, we compute the set of the symmetric of the interfaces belonging to the component containing the membrane and its content.

Finally, most of the consistency rules dealing with the bindings will use the auxiliary functions GetSrc and GetDst. They are able to retrieve the Interface objects which represent respectively the source and the destination ends of a binding. If GetSrc and GetDst functions are applied to a binding inside a membrane, then they may return an internal interface of the membrane.

Conversely, some rules use the Parent auxiliary function, that recovers the container (component, membrane or content) of an interface, a component, a content or a membrane.

Interceptors

In this section we define interceptors more precisely. First, we provide the non-formal definition of an interceptor. Then, we introduce a predicate recognizing the interceptors among the other sub-components of a membrane.

An interceptor is a functional component inside a membrane. It is connected to one external and one internal functional interfaces of the membrane's parent. An interceptor "intercepts" a functional call that goes from outside to inside of the membrane (input interceptor) or vice versa (output interceptors). The interceptors are used to monitor an application and its functional calls. The only functional activity of an interceptor should be to intercept and forward the functional calls through its functional client and server interfaces. All the other actions are performed through non-functional interfaces. To allow more modularity in the design, interceptors can be assembled in chains inside the membrane. Interceptors in a chain must all be either input or all output; we shall speak of input chains and output chains.

In principle, it would be possible to relax this definition, and allow for more general interceptor structures, e.g. including some parallelism in the form of multicast client interface in the "chain", allowing more efficient processing. However it is not clear whether this would be useful fo rreal applications, and this not implemeted in the GCM/ProActive middleware, so we prefer to keep the (relatively) simpler form in the formal definition.

In order to distinguish formally the interceptors from the other components, we define a predicate IsInterc. It is given in Table3. It takes a component and a membrane as an input and returns true if the component belongs to a chain of interceptors inside the given membrane. An interceptor chain consist of one or several interceptors. IsInterc uses a predicate IsIntercChain which identifies if a given sequence of K components is a chain of pipelined interceptors inside the given membrane. IsIntercChain predicate checks the following features of the indexed set of components given as input:

• all the components are nested inside the membrane;

• all the components have exactly one functional server and one functional client interface;

• a functional call can go through the sequence of components. More formally, for any k ∈ 2...K there is a binding connecting client functional interface of the component number k -1 and server functional interface of the component number k; • the first component of an input chain intercepts a functional call to the content while the last component forwards the functional call to the content or vice versa for an output chain.

Predicate IsIntercChain uses two auxiliary functions: GetSItf F (comp) (resp. GetCItf F (comp)) returns the sets of all functional server (resp. client) interfaces of component comp.

The predicate IsExtEnd checks, for an input interceptor chain, whether the first interceptor in the chain is connected to a server functional interface of the parent component or, for output interceptors, whether the last one is connected to a client functional interface of the parent component

F (i k ) = {SI k } ∧ GetCItf F (i k ) = {CI k }) ∧ (∀k ∈ {1...K -1}).(∃b k ∈ Binding(membr). GetSrc(b k , membr) = CI k ∧ GetDst(b k , membr) = SI k+1 )∧ ∃b 0 , b K ∈ Binding(membr).∃I 0 , I K : Itf. (IsExtEnd(I 0 , b 0 , SI 1 , membr, I 0 ) ∧ IsIntEnd(CI k , b K , I K , membr, I K )) ∨(IsIntEnd(I 0 , b 0 , SI 1 , membr, I 0 ) ∧ IsExtEnd(CI k , b K , I K ,

Table 3: Interceptor Predicates

IsIntEnd is the symmetric, it checks connection with the content. However, the content is not known for a primitive component; in that case the interfaces of the content are computed by symmetry of the external (functional) interfaces of the component.

Well-formed components

In this section we define the well-formness rules for GCM components. First, we introduce the core rules and predicates used for the definition of well-formness. Then, we focus on the non-functional aspects.

Core

Table 4 formalizes the auxiliary predicates which are used for the definition of the following constraints:

• Components naming constraint (UniqueCompNames): all the components at the same level of hierarchy must have different names. This restriction is due the fact that components are referenced by their name; typically, QName can be of the form CName.Name; and if two components had the same name the functions GetSrc and GetDst would not return a single deterministic result. The two contents of two different composite components as well as two membranes are considered to be different name-spaces. A membrane and a content are also different name-spaces even if they belong to the same component. • Interfaces naming constraint (UniqueItfNames): all the interfaces of a component must have different names. This constraint will be checked separately, for the external interfaces of a component, and for the internal interfaces of a content. This constraint also ensures the determinacy of the functions GetSrc and GetDst.

Predicate name Predicate Definition UniqueNamesAndRoles UniqueNamesAndRoles(Itf i∈I

i : set of Itf) ⇔ ∀i, i ′ ∈ I.(i = i ′ ∧ Name(Itf i ) = Name(Itf i ′ )) ⇒ Role(Itf i ) = Role(Itf i ′ ) BindingNature BindingNature(b : Binding) ⇔ CL(GetSrc(b, Parent(b))) = CL(GetDst(b, Parent(b))) = 1∨ (CL(GetSrc(b, Parent(b))) > 1 ∧ CL(GetDst(b, Parent(b))) > 1)
Table 5: Non-functional Predicates because it is related to the non-functional aspect.

Let cont :

Cont =< SItf i∈I i , CItf j∈J j , Comp k∈K k , Binding l∈L l >; (3) W F(cont) ⇔    UniqueItfNames(SItf i∈I i ∪ CItf j∈J j ) ∧UniqueCompNames(Comp k∈K k )∧ CardValidity(Binding l∈L l ) ∧ ∀k ∈ K.W F(Comp k )∧ ∀B ∈ Binding l∈L l .BindingRoles(B) ∧ BindingTypes(B) ∧ BindingNature(B)
The well-formness of a membrane is only significant for the non-functional aspect, it is defined below.

Non-functional aspects

In this section we define the static semantics constraints ensuring safe composition of the non-functional part of a GCM-based application. Correctness of a membrane relies on the two predicates defined in Table 5:

• Interfaces naming constraint (UniqueNamesAndRoles): if there are two interfaces with the same names in a membrane, then they must have different roles. This is as slight relaxation from the UniqueItfNames rule of the general case: we want to allow corresponding external/internal interfaces pairs of opposite role to have the same name. This also ensure compatibility with the original Fractal model, where internal interfaces were implicitly defined as the symmetric of external ones. • Binding nature constraint(BindingNature) is a rule imposing the separation of concerns between functional and non-functional aspects. We want the functional interfaces to be bound together (only functional requests will be going through these), and non-functional interfaces to be connected together as a separate aspect. This is simple to impose in the content of composite components, but a little more tricky in the membrane because of the specific status of interceptors. The solution is to qualify as functional all the components in a content and all the interceptors, while all other components in the membrane are non-functional. Then the interfaces are declared functional or non-functional. From this we compute for each interface a control level ranging from 1 to 3, where 1 means functional; 2 and 3 mean non-functional. Then the compatible interfaces are either both "1", or both greater than "1". The ControlLevel function is formally defined as:

CL(X : Comp) ::= 2, i f Parent(X, context) : Membr ∧ ¬IsInterc(X, Parent(X))) 1, else CL(X : Cont | Membr) ::= 1 CL(X : Itf) ::= CL(Parent(X)), i f Nature(X) = F CL(Parent(X)) + 1, i f Nature(X) = NF (4)
This constraint on the nature of bindings was already mentioned in [START_REF] Naoumenko | Designing Non-functional Aspects With Components[END_REF], we propose here a formal definition that is simpler and more intuitive.

As the last step, we define the well-formness predicate for membranes. A membrane is well-formed if all its sub-components have distinct names, the naming constraint is respected for its interfaces, all its sub-components are well-formed, all its bindings ensure a valid cardinality, and the role, type, nature constraints are respected for all its sub-bindings, Let membr :

Membr =< Comp k∈K k , Binding l∈L l >; (5)
W F(membr) ⇔    UniqueCompNames(Comp k∈K k ) ∧UniqueNamesAndRoles(Itf(membr))∧ ∀k ∈ K.W F(Comp k ) ∧CardValidity(Binding l∈L l )∧ ∀B ∈ Binding l∈L l .BindingRoles(B) ∧ BindingTypes(B) ∧ BindingNature(B)
This section presented an extension to the definition of well-formed components defined in previous works [START_REF] Henrio | A Framework for Reasoning on Component Composition[END_REF][START_REF] Gaspar | Bringing Coq Into the World of GCM Distributed Applications[END_REF]. More precisely, most of the definitions given in this section allow us to formalize the notion of well-formed non-functional features and well-formed interceptors, that have never been formalized before. The new definition of well-formed components is the basis for the correct composition of distributed components with clear separation of concerns.

Properties

The well-formed definition of the preceding section guarantees that, from an architectural point of view, the specified component assembly behaves well, both at deployment time and during execution. More precisely, the constraints specified above ensure the following properties: Component encapsulation Bindings do not cross boundaries. Indeed, GetSrc and GetDst predicates are only defined in the context of the parent component, for example, the call to GetDst and GetSrc inside the definition of the BindingRoles predicate ensure that both bound interfaces are either internal interfaces of the parent component or external interfaces of its sub-components, which guarantees that no binding crosses component boundaries.

Deterministic communications

The CardValidity predicate guarantees that each client interface is bound to a single server interface, which guarantees that each communication between components is targeted at a single, well-defined, destination. Section 4.1 will introduce mutlticast interfaces to express communications with multiple destinations. Unique naming Several predicates ensure the uniqueness of component or interface names in each scope (sub-components of the same component, interfaces of the same component, etc.). This restriction is crucial for introspection and modification of the component structure. For example rebinding of interfaces can be easily expressed based on component and interface names. Separation of concerns The definition of non-functional aspects ensure that: 1) each component has a well-defined nature: functional if it belongs to the content, and non-functional if it belongs to the membrane. 2) each interface has a well-defined control level, depending on the component it belongs to and on the nature of the interface. The nature of components and interfaces is defined by the control-level (CL) predicate. 3) Bindings only connect together functional (resp. nonfunctional) interfaces. 4) We clearly identify interceptor components that are the only structural exception to these rules: an interceptor is a component in the membrane that can have a single functional client and a single functional server interface, but as many non-functional interfaces as necessary. In order to guarantee that the generated ADL deploys correctly, i.e. without runtime error, it is sufficient to ensure that (1) each interface and class the ADL file refers to exists (which is ensured by the generation process), that (2) no binding exception will be raised at instantiation time (which is ensured by the well-formedness property and in particular by the determinacy of communications), and that (3) each mandatory interface is bound and thus the component system can be started without error (which is again ensured by the well-formedness property dealing with bindings); finally (4) the unique names ensure that the components and interfaces can be manipulated adequately during instantiation. All those arguments ensure that each ADL file generated by our platform deploys correctly, provided the wellformed property is verified by the system.

The properties verified by well-formed components not only guarantee that the ADL generated from a well-formed specification deploys correctly, but also ensure some crucial properties concerning the runtime semantics (deterministic communications, separation of concerns, reconfigurability ...).

Extension and Related Work

While Section 3 focused on the core concepts of a component model with componentized membranes, we illustrate in this section how our framework can be used to model other features of GCM or of other component models. We also compare our approach with related works.

Collective communications

One of the crucial features of GCM is to enable one-to-many and many-to-one communications through specific interfaces, namely gathercast and multicast.

In order to specify such communications let us add a Cardinality (Card) field in the specification of the GCM interfaces. The cardinality can be singleton, multicast or gathercast. For example, interface M1 at Figure 1 is multicast: it sends requests to several workers at the same time. G1 is gathercast: it can receive requests from several workers. S1 and C1 are singleton interfaces.

These new interfaces modify the definition of cardinality validity. In particular, the multicast interface allows two bindings to originate from the same client interface. The CardValidity is modified as follows: The intended semantics is that any invocation emitted by a multicast interface is sent to all the server interfaces bound to it. Gathercast interface on the contrary synchronizes several invocations arriving at the same server interface, they do not entail any structural constraint. An interceptor chain should not contain any multicast functional interface because it should transmit invocations in a one-to-one manner.

Other component models

Our work is placed in the context of GCM component model but it can also be used to model the characteristics of most component models, we review some of them in this paragraph. First, concerning the functional parts of components, a lot of component models have a structure similar to GCM components, like, e.g., SCA [START_REF] Madelaine | SCA Assembly Specification Version 1.1[END_REF] or Fractal [START_REF] Bruneton | The Fractal Component Model and Its Support in Java. Software Practice and Experience, special issue on Experiences with Auto-adaptive and Reconfigurable Systems[END_REF]. Our framework can be used to formally define architectural correctness for these component models. Additionally, several frameworks offer different notion of componentized component control, we focus on these aspects below. SOFA 2.0 [START_REF] Bureš | SOFA 2.0: Balancing Advanced Features in a Hierarchical Component Model[END_REF] features hierarchical composition and componentized component control. Interestingly, similarly to our approach, one of the objectives of SOFA is also to provide formal verification tools for distributed component systems. It is easy to adapt our formal specification to SOFA 2.0, more precisely: Micro-controllers are components dedicated to non-functional concerns, they reside in the membrane and are not hierarchical: to take them into account, we should restrict the correctness rules for the membrane to only allow primitive components in the membrane. The other aspects of SOFA are not different from the model used in this paper. In particular, delegation chains are chains of interceptors, following exactly the rules defined in Section 3.3.

AOKell [START_REF] Seinturier | A Component Model Engineered with Components and Aspects[END_REF] is an extension of Fractal specifically for componentizing membranes, it is interesting to note that the authors define a notion of control level, which is quite similar to the ControlLevel function used in our paper. In this case again, our approach could be used to verify the correct composition of AOKell-based components, and ensure the safe design of AOKell component systems.

In a similar way, Dynaco [START_REF] Buisson | A framework for dynamic adaptation of parallel components[END_REF] could also benefit from our approach, it is a component model targeting dynamic adaptation and allowing full-fledged components in component's membranes.

Related Approaches

In a slightly different application domain, BIP [START_REF] Bensalem | Compositional verification for component-based systems and application[END_REF][START_REF] Basu | Rigorous Component-Based System Design Using the BIP Framework[END_REF] is a formal framework that allows building and analyzing complex component-based systems, both synchronous (reactive) or asynchronous (distributed) by coordinating the behaviour of a set of primitive and heterogeneous components. BIP is supported by a tool set including translators from various programming languages as Lustre and C into BIP, a compiler for generating code executable by a dedicated engine, and the verification tool dFinder.

Concerning the formalization of component structure, the two closest previous works are the formalization of Fractal in Alloy [START_REF] Merle | A formal specification of the Fractal component model in Alloy[END_REF], and the formalization of GCM in Isabelle/HOL [START_REF] Henrio | A Framework for Reasoning on Component Composition[END_REF]. The first framework focuses on structural aspects in order to prove the realisability of component systems, while the second aims at providing lemmas and theorems to reason on component models at a meta-level, and prove generic properties of the component model. None of those formalizations included the notion of non-functional components, many-to-many interfaces, or interceptors. The formal specification of component correctness defined in this paper could be used to extend the expressiveness of the component model in the Alloy and the Isabelle frameworks. Also the strength of the present work is that it is directly implemented in the VCE environment in order to provide tools accessible for the programmer. The tools presented here ensure, in a graphical environment, that the component systems composed by the programmer are well-formed.

From another point of view, in [START_REF] Gaspar | Bringing Coq Into the World of GCM Distributed Applications[END_REF] we investigated a language for generating correct-by-construction component systems, and reconfiguring them safely. Similarly to the cases above, this language does not deal with the structure of the membrane and one-to-many/many-to-one communications, it should be extended to the enhanced component structure presented here.

Implementation: the VCE modeling environment

The presented formal model and formal constraints were implemented in a tool called VerCors Component Editor (VCE v.3) which is the graphical specification part of the VerCors project. VCE v.3 combines a set of semantics models and graphical diagram editors, the tools for graphical and textual export of models and a set of additional wizards. Using VCE v.3 one can design the architecture of a componentS-based system, validate its structure according to the rules specified in this paper and export its representation, either as an ADL (XML) file, that will be used in the execution environment, or as a semantic representation, for model-checking. We briefly discuss below the basic features of the tool. The static semantics constraints, defined in the previous sections are encoded in VCE v.3 in order to validate component assemblies. The Acceleo language 4 is used for the definition of such rules. An example of a rule defining the naming constraint for the components is given below:

[not self.siblings(Component)->collect(name)->includes(self.name)/] This rule will be applied to each component. Here, self is the component on which the constraint is validated; let us denote it C. The function siblings(Component) returns the set of all the components in the same container as C. The function collect(name) extracts the names of all such components. Finally, includes(self.name) checks if there is any component with the same name as C and returns true if it finds one. VCE v.3 editor reports about the constraint violations. The elements of the architecture which are not correct are marked with red signs. The description of an error is given in a standard Eclipse Problem panel. Figure 4 illustrates an example of the architecture validation result; the architecture contains only one error: there is a binding between two interfaces with incompatible types (C1 and S1).

To conclude, based on the formal definitions given in this paper, we implemented an environment for the specification of the component-based applications involving group communications and with strong separation of functional and non-functional concerns. The validation of designed models ensures the correctness of the components assemblies. From this specification VerCors environment allows the verification of the behavioural properties of the system, and the generation of executable code that is safe by construction and can be run using the GCM/ProActive library.

Conclusion and Future Work

This article presented the formalization of rich component models with strong separation of functional and non-functional concerns, including the definition of interceptors. It also presented a tool implementing the formalized model. The main contributions of the article are:

• the formal definition of GCM components including non-functional aspect and interceptors;

• the formal definition of well-formness predicates including special rules for non-functional aspects, binding compatibility, and interceptors; special care has been put on the separation of concerns: the notion of control level was introduced and formally defined for the interfaces and components; • implementation of a tool for GCM-based systems architecture graphical modeling and their static semantics validation. • the identification of basic and crucial properties of the component assemblies which are guaranteed by our rules, and by the VCE platform. In particular, when a GCM application specification has been checked valid in VCE, the generated ADL file is guaranteed correct by construction, and the corresponding components will be built and deployed correctly (with no execution error) by the middleware component factory.

One of the key challenges addressed by this paper is the clear representation of interceptors chains and especially the formalization of predicates which recognize them among the other components inside a membrane.

Our approach is general enough to be extensible in order to take into account many-to-many communications or other component models.

However, the VerCors platform is not completely implemented yet. We are now working on the representation and validation of GCM-based systems behavior using UML State Machines for the definition of primitive components behavior in VCE v.3. This functionality is already partially specified and implemented. The state-machine and architecture models will be used to generate a finite semantic representation, suitable as the input to verification tools. The structural wellformess rules from this paper will have to be complemented by others, ensuring the coherency between the structural and behavioural models.

Figure 1 :

 1 Figure 1: A typical GCM component assembly (image produced by VerCors)

Figure 2 :

 2 Figure 2: Internal interfaces of a membrane

Figure 3 :

 3 Figure 3: Principles of the VerCors platform

  membr, I K )) IsExtEnd IsExtEnd(CI : CItf, b : Binding, SI : SItf, membr : Membr, I : Itf) ⇔ GetSrc(b, membr) = CI ∧ GetDst(b, membr) = SI ∧ Nature(I) = F∧ Sym(I) ∈ GetItf(Parent(membr)) IsIntEnd IsIntEnd(CI : CItf, b : Binding, SI : SItf, membr : Membr, I : Itf) ⇔ GetSrc(b, membr) = CI ∧ GetDst(b, membr) = SI ∧ Nature(I) = F∧ If IsComposite(Parent(membr)) then Sym(I) ∈ GetItf(Cont(Parent(membr))) Else Sym(I) ∈ Sym(GetItf(Parent(membr)))

  Binding) ⇔ ∀itf : Itf. ∀l, l ′ ∈ L.l = l ′ (itf = GetSrc(Binding l , Parent(Binding l )) = GetSrc(Binding l ′ , Parent(Binding l ′ ) ⇒ Card(itf) = multicast)

Figure 4 :

 4 Figure 4: VCE v.3

Table 1 :

 1 The formalization of GCM architecture correctness of a GCM component assembly, we describe their implementation in VCE in Section 5.

	Element	Formalization
	Server interface i , Nature) Primitive SItf ::= (Name, MSignature i∈I Prim ::= CName < SItf i∈I i , CItf j∈J j , M k∈K k Composite Compos ::= CName < SItf i∈I i , CItf j∈J j , Membr, Cont > , Membr >
	Component	Comp ::= Prim | Compos
	Content	Cont ::=< SItf i∈I i , CItf j∈J j , Comp k∈K k , Binding l∈L l	>
	Binding	Binding ::= (QName, QName)
		QName ::= This.Name | CName.Name
	Nature	Nature ::= F | NF
	Membrane	Membr ::=< Comp k∈K k , Binding l∈L l	>

S Client interface CItf ::= (Name, MSignature i∈I i , Nature) C Interface Itf ::= SItf | CItf Method signature MSignature ::= MName × Type → Type

  Comp, membr : Membr) ⇔ ∃ic.IsIntercChain(ic, membr) ∧ comp ∈ ic; IsIntercChain IsIntercChain({i 1 ...i K } : set of Comp, membr : Membr) ⇔ {i 1 ...i K } ⊆ Comp(membr) ∧ ∃SI 1 ...SI K ,CI 1 ...CI K . (∀k ∈ {1...K}). (GetSItf

	Predicate name	Predicate Definition
	IsInterc	IsInterc(comp :
		. Predicate

The VERCORS platform: VERification of models for distributed communicating COmponants, with safety and Security. http://team.inria.fr/scale/software/vercors/

http://www.obeodesigner.com/

http://www.eclipse.org/modeling/emf/ http://www.eclipse.org/modeling/gmf/

http://www.eclipse.org/acceleo/

This work was partialy funded by the Associated Team DAESD between INRIA and ECNU, Shanghai; and by the french Fond National pour la Société Numérique project OpenCloudware.

Predicate name Predicate Definition UniqueCompNames UniqueCompNames(Comp i∈I

Table 4: Core Predicates

• Role constraint (BindingRoles): a binding must go from a client interface to a server interface.

The predicate uses a function Role(I) that returns C (resp. S) if I is a client (resp. server) interface. • Typing constraint (BindingTypes): a binding must bind interfaces of compatible types. The compatibility of interfaces means that for each method of a client interface there must exist an adequate corresponding method in the server interface. In other words, if a client interfaces is connected to a server interface and it wants to call some method, then this method must actually exist on the server interface. In general, a corresponding method does not need to have exactly the same signature as the one required, but can use any sub-typing or inheritance pre-order available in the modeling language. We denote ≤ such an order between interface signatures. • Cardinality constraint, CardValidity, ensures that a client interface is bound to a single server one.

We use the previous constraints to define a well-formness predicate, denoted W F. It is defined recursively on component architecture, namely on primitive components, on composite components, and on contents.

A GCM primitive component is well-formed if all its interfaces have distinct names and its membrane is well-formed.

A GCM composite component is well-formed if all its external interfaces have distinct names, its content and its membrane are well-formed.

Let compos : Compos = CName < SItf i∈I i , CItf j∈J j , Membr, Cont >;

(2)

The content of a GCM component is well-formed if all its interfaces have distinct names, all its subcomponents have distinct names, all its nested bindings ensure valid cardinality, all its sub-components are well-formed, the role, type and nature constraints are respected for all its sub-bindings. The nature constraint for the bindings relies on The BindingNature predicates. It is discussed in Section 3.4.2


Clément Ballabriga
email: ballabri@irit.fr

Hugues Cassé
email: casse@irit.fr

Christine Rochange
email: rochange@irit.fr

Pascal Sainrat
email: sainrat@irit.fr

OTAWA: an Open Toolbox for Adaptive WCET Analysis

Keywords: Real-time, Worst-Case Execution Time, static analysis

The analysis of worst-case execution times has become mandatory in the design of hard real-time systems: it is absolutely necessary to know an upper bound of the execution time of each task to determine a task schedule that insures that deadlines will all be met. The OTAWA toolbox presented in this paper has been designed to host algorithms resulting from research in the domain of WCET analysis so that they can be combined to compute tight WCET estimates. It features an abstraction layer that decouples the analyses from the target hardware and from the instruction set architecture, as well as a set of functionalities that facilitate the implementation of new approaches.

Introduction

In hard real-time systems, critical tasks must meet strict deadlines. Missing one such deadline may have dramatic consequences, either in terms of human lives or economical and environmental issues. To avoid this, special attention is paid on determining a safe schedule for tasks.

Real-time task scheduling has been and is still a hot research topic, but it relies on the knowledge of the Worst-Case Execution Time (WCET) of the critical tasks. While this time is generally considered as known, the techniques required to compute it are not straightforward and cannot always support complex target architectures. As a result, research on WCET analysis is also very active.

The general approach to WCET analysis includes three steps: (a) flow analysis mainly consists in identifying (in)feasible paths and bounding loops; (b) low-level analysis aims at determining the global effects of the target architecture on execution times and at deriving the worst-case execution times of code snippets; (c) finally, the results of the flow and low-level analyses are combined to derive the overall WCET. For each of these three steps, several techniques have been investigated in the literature. Besides, several tools have been developed to implement these results. Most of them are still research prototypes but a few are now commercialized.

The design of the OTAWA toolbox presented in this paper started in 2004, at a time where very few tools were publicly available. Our main motivation was

to provide an open framework that could be used by researchers to implement their analyses and to combine them to already implemented ones. The expected characteristics of this framework were versatility (ability to support various target hardware configurations as well as various instruction sets) and modularity (support to facilitate the implementation of new analyses). OTAWA is not a tool but a toolbox : this means that it comes as a C++ library that can be used to develop WCET analysis tools. However, it includes a number of algorithms which make this task really easy (example tools are distributed with the library).

The paper is organized as follows. Section 2 reviews the state of the art on WCET analysis and gives a short overview of existing tools. The OTAWA toolbox is presented in Section 3 and Section 4 illustrates its capacities through a short report of how it has been used in several projects. Concluding remarks are given in Section 5.

Worst-Case Execution Time Analysis

Different approaches to WCET analysis

The execution time of a program on a given processor depends on the input data and on the initial state of the hardware (mainly on the contents of the memories). To evaluate its worst-case execution time (WCET), it is necessary to consider all the possible input values and all the possible initial hardware states. In most of the cases, this is not feasible: (a) determining input data sets that cover all the possible execution paths is hard, especially with floating point inputs1 ; (b) even if this was possible, the number of paths to explore would be too large and the time required to measure all of them would be prohibitive; (c) it is not always possible to initialize the hardware state prior to measurements so as to investigate all the possible states. Because it is not feasible to measure all the possible paths considering all the possible initial hardware states, it is now commonly admitted that WCET analysis must break down the execution paths into code snippets (generally basic blocks) so that time measurement or estimation is done on these units and the overall WCET is computed from the unit times.

One way to classify approaches to WCET analysis is to consider the way they determine the worst-case execution time of code snippets. Some of them are based on measurements performed preferably on the real target hardware, but possibly on a simulator [START_REF] Bernat | pWCET a Toolset for automatic Worst-Case Execution Time Analysis of Real-Time Embedded Programs[END_REF] while other ones use a model of the hardware to compute these times [START_REF] Heckmann | The Influence of Processor Architecture on the Design and the Results of WCET Tools[END_REF][19] [START_REF] Rochange | A Context-Parameterized Model for Static Analysis of Execution Times[END_REF].

Another approach is to focus on the way the unit times are combined to derive the complete WCET of the task. Some approaches need the program under analysis to be expressed in the form of an Abstract Syntax Tree (AST) [START_REF] Lim | An accurate worst case timing analysis technique for RISC processors[END_REF][10] and compute the WCET using analytical formulae related to the algorithmic-level statements found in the code. These approaches do not fit well with codes that have been optimized at compile time. Other solutions consider the Control Flow Graph (CFG) built from the object code and use path-based calculation [START_REF] Healy | Bounding pipeline and instruction cache performance[END_REF] or formulate the search of the longest execution path as an Integer Linear Program [START_REF] Li | Performance Analysis of Embedded Software using Implicit Path Enumeration[END_REF].

Besides to these contributions that are at the root of research on WCET analysis, a lot of work has been done to design algorithms able to derive execution times of basic blocks considering various and more and more complex hardware features. These solutions will be shortly reviewed below.

Analysis of the behavior of hardware mechanisms

WCET estimates are expected to be safe since the determination of a schedule of tasks that insures that hard deadlines will be met is based on them. So far, no way to obtain guaranteed WCET upper bounds without getting into the hardware architecture details has been found. Instead, existing methods compute execution time with cycle-accuracy. As a result, a number of papers have been published to show how to take into account the behavior of specific variants of hardware mechanisms in WCET analysis. In addition, it is often required for WCET estimates to be tight so as to avoid oversizing the hardware to insure schedulability. For this reason, research work also focuses on reducing the WCET overestimation.

Many hardware schemes now present in the processors used in embedded systems are supported by WCET analysis techniques:

the processor pipeline has been studied for many years from the first scalar architectures [START_REF] Lim | An accurate worst case timing analysis technique for RISC processors[END_REF] to superscalar configurations [START_REF] Lim | A worst case timing analysis technique for optimized programs[END_REF][30] and pipelines featuring dynamic instruction scheduling [START_REF] Heckmann | The Influence of Processor Architecture on the Design and the Results of WCET Tools[END_REF][19] [START_REF] Rochange | A Context-Parameterized Model for Static Analysis of Execution Times[END_REF]; -the analysability of cache memories has also been largely investigated. Several techniques have been proposed to analyze the behavior of instructions caches [START_REF] Alt | Cache Behavior Prediction by Abstract Interpretation[END_REF][15], data caches [29][28], and multi-level memory hierarchies [START_REF] Hardy | WCET analysis of multi-level non-inclusive set-associative instruction caches[END_REF]; -dynamic branch predictors have retained attention too [START_REF] Puaut | Worst Case Execution Time Analysis for a Processor with Branch Prediction[END_REF][3] [START_REF] Burguière | On the Complexity of Modelling Dynamic Branch Predictors when Computing Worst-Case Execution Times[END_REF]; -other mechanisms like the memory row buffer have been considered [START_REF] Bourgade | Accurate analysis of memory latencies for WCET estimation[END_REF] to model specific hardware.

A recent paper [START_REF] Wilhelm | The Worst-Case Execution Time Problem -Overview of Methods and Survey of Tools[END_REF] reviews and compares the WCET tools that have been designed by members of the ARTIST European Network of Excellence. Some of them are research prototypes and other ones are commercial tools. Since most of these tools were not publicly available or not mature enough at the time we started research analysis (2004), designing our own software was a necessity. However we always kept in mind the need of making it open so that it can host any research result on WCET analysis. [START_REF] Bate | Efficient Integration of Bimodal Branch Prediction and Pipeline Analysis[END_REF] The OTAWA toolbox

Objectives

Developments for the OTAWA toolbox started in 2004 with the objective of designing a framework that could integrate various kinds of methods related to WCET analysis and support a large range of target architectures. Such a framework is expected to:

capitalize results of research on WCET estimation make it possible to compare two different techniques that address the same problem (e.g. instruction cache analysis) though experiments carried out under identical conditions support the investigation of new algorithms by allowing experiments that combine them to state-of-the-art techniques. This avoids having to make either overwhelmingly optimistic or pessimistic assumptions for features that are out of the scope of the current work.

To achieve these goals, OTAWA exhibits two key features. First, both the target hardware and the code under study are processed through an abstract layer: this way, analyses are designed independently from the hardware and from the instruction set and can then be used for any architecture. Second, the toolbox provides all the facilities to implement new analyses with limited effort

The overall structure of the OTAWA toolset is shown in Figure 1. It includes a number of components that provide two classes of facilities: some of them maintain information about the application under analysis and about the target hardware architecture, as detailed in Section 3.2; other ones manipulate and enrich this information towards an estimation of the worst-case execution time (see Section 3.3).

Abstract layers

As explained above, OTAWA is organized in independent layers that provide an abstraction of the target hardware and associated Instruction Set Architecture (ISA) as well as a representation of the binary (.elf) code under analysis.

ISA support. This layer hides the details of the target ISA to the rest of the toolset and provides a unique interface to retrieve the information needed for the analyses related to WCET estimation. This way, most of the components of the toolbox can be designed independently of the instruction set. The layer features support for various ISAs implemented through a set of plugins. Available plugins have been generated using our GLISS tool [START_REF] Ratsiambahotra | A Versatile Generator of Instruction Set Simulators and Disassemblers[END_REF] that will be presented in Section 3.4 and support the following ISAs: PowerPC, ARM, TriCore, HCS12, Sparc.

Abstraction of the hardware architecture. Precise estimation of the worstcase execution time of instruction sequences requires a detailed knowledge of hardware parameters:

processor: width and length of the pipeline, number of functional units and their latencies, binding of instruction categories to the functional units, specification of the instruction queues (location, capacity) -caches: capacity, line width, organization (number of sets, number of ways), replacement policy, write policy, etc. -memories: as part of the French MORE project, we have implemented support for various memory components (DRAM, scratchpad), each exhibiting a specific access latencies and buffering policies.

Support for additional components or new architectural features can be added by the developer with limited effort. From the user side, the hardware parameters can be specified with an XML file. Since investigating formats that could describe any kind of processor was out of the scope of our research, we decided to limit our XML format to the minimum needed to specify standard architectures. Taking into account real-life processors still requires specific developments by the user, but this is made easy by the classes and functionalities available through the OTAWA library.

Properties. One key facility in the OTAWA toolbox is the possibility of defining properties that can be used to annotate any kind of object defined in the library (e.g. an instruction) in a very convenient way. These annotations are first used to build the CFG (or AST) representation of the program. The set of instructions in the program is retrieved through the ISA support layer, and a Control Flow Graph (CFG) can be built for each function. It consists of basic blocks, i.e. sequences of instructions with single entry and exit points, and of edges that express the possible flow from one basic block to another one. In the case of indirect branch instructions (e.g. implementation of a switch statement), it may happen that OTAWA requires help from the user who must specify the possible branch targets so that appropriate edges can be included in the CFG. The program under analysis is then represented within OTAWA as a set of interconnected CFGs.

The properties are also useful to store the results produced by the different analyses (e.g. the instruction cache analyzer annotates instructions to indicate whether they will hit or miss in the cache and the pipeline analyzer takes this information into account to determine the instruction fetch latencies).

Analyses

As explained before, the determination of the WCET of a task involves a number of analyses that must be performed in an appropriate order. In OTAWA, such analyses are implemented as Code Processors: a code processor is a function that uses available annotations and produces new annotations.

The distributed OTAWA library includes a set of analyses. Some are related to flow analysis and produce information that are useful to other analyses. Examples in this category are a CFG builder, a CFG virtualizer that produces a virtual CFG with the functions inlined (this allows call-contextual analyses) or a loop analyzer that determines loop headers and dominance relationships which are used e.g. by the instruction cache analysis. Other code processors provide facilities to use state-of-the-art analysis techniques, like Abstract Interpretation [START_REF] Cousot | Abstract Interpretation -A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints[END_REF]. Finally, a number of analyses compute data that can be combined to determine the final WCET. They include the pass that generates the integer linear program defined by the IPET method [START_REF] Li | Performance Analysis of Embedded Software using Implicit Path Enumeration[END_REF] but also several analyses that take into account the features of the target hardware. At this state, OTAWA provides the code processors needed to analyze:

instruction caches: the approach is based on Abstract Interpretation and is close to Ferdinand's method [START_REF] Ferdinand | Applying compiler techniques to cache behavior prediction[END_REF]. However, our implementation includes the improvements proposed in [START_REF] Ballabriga | Improving the First-Miss Computation in Set-Associative Instruction Caches[END_REF] to reduce complexity while performing an accurate persistence analysis in the case of loop nests. -pipelines: the method implemented in OTAWA to compute the worst-case execution times of basic blocks is original and has been presented in [START_REF] Rochange | A Context-Parameterized Model for Static Analysis of Execution Times[END_REF]. While the aiT tool uses abstract interpretation to build the set of possible processor states in input/output of each basic block, which is likely to be time consuming, our method is based on execution graphs and involves an analytical calculus. This is similar to the approach used in the Chronos tool [START_REF] Li | Modeling out-of-order processors for WCET analysis[END_REF] except for we consider a parametric view of the processor state at the entry of each basic block when they consider the worst-case processor state.

Experiments have shown that our algorithm provides more accurate results with comparable computation times. -dynamic branch predictors: we have developed an algorithm to take into account the behavior of a dynamic branch predictor [START_REF] Burguière | On the Complexity of Modelling Dynamic Branch Predictors when Computing Worst-Case Execution Times[END_REF]. It formulates the question of determining whether a branch will be always/sometimes/never well predicted as an integer linear program. However, experiments have shown that the complexity of this program is significant.

Handling analyses dependencies. When considering the full process of computing the WCET of a task, it appears that the involved analyses are interdependent through a producer-consumer scheme: annotations produced by one analysis are required by other passes. To respect these dependencies, the analyses must be invoked in an appropriate order as illustrated on the example shown in Figure 2. OTAWA provides a means to automatically handle dependencies: features can be used to express the properties that are required or produced by a code processor. For each defined feature, a default code processor must be specified: it will be executed when the feature is required if it has still not been produced. As a result, a simple WCET tool can be designed by only invoking a final WCET computation code processor: default code processors will be automatically called to generate the missing data. Display facilities. OTAWA provides facilities to dump out program representations and annotations produced by the different analysis. These outputs are as useful to the WCET tool developer, as well as to the real-time application developer. The former can use them to debug or to tune new analyses while the latter can get a better understanding of the program behavior and locate program regions that break the deadlines. More recently, OTAWA has been integrated in the Eclipse programming environment. The OTAWA plugin allows benefiting from the Eclipse graphical user interface to improve OTAWA use ergonomics and helps in achieving a better integration in the development cycle. The developer can seamlessly develop an application, compile it and get the WCET of some program parts. From the graphical program representation, time-faulty program regions can be also easily identified and fixed. Figures 3 and4 show how the source code and the CFG of the program under analysis can be displayed and colored to highlight the critical paths (the darker code regions are those that are responsible for the larger part of the total WCET).

Cycle-level simulator. In addition to the WCET-related analyses, the OTAWA toolbox also includes a code processor that builds and runs a cycle-level simulator. This simulator is generated on top of the SystemC library and matches

Complementary tools

In OTAWA, the abstraction of the Instruction Set Architecture is provided by a loader module in charge of loading the object code of the application under study and of building a representation of this code that is independent of the ISA. To design these loader modules, we use instruction set simulators generated by our GLISS tool from ISA specifications expressed in the SimNML language [START_REF] Ratsiambahotra | A Versatile Generator of Instruction Set Simulators and Disassemblers[END_REF]. An instruction set simulator is a library that provides functions to decode, disassemble and emulate instructions (emulation is performed on a logic state of the memory and registers).

Another complementary tool is oRange that is used to determine flow facts and more particularly loop bounds [START_REF] Michiel | Static loop bound analysis of C programs based on flow analysis and abstract interpretation[END_REF]. It works on the C source code of the application and uses flow analysis and abstract interpretation techniques to derive contextual loop bounds (a loop in a function can have different bounds for different calls). Debug information inserted by the compiler in the object code are used by OTAWA to assign source-level loop bounds to the corresponding machine-level instructions. In the future, oRange will be integrated into the OTAWA framework.

Finally, the integer linear programs generated as part of the IPET method [START_REF] Li | Performance Analysis of Embedded Software using Implicit Path Enumeration[END_REF] are solved by invoking the lp solve tool [START_REF]Open source (Mixed-Integer) Linear Programming system[END_REF].

Examples of use

The OTAWA toolbox has been involved in several projects. In this Section, we give insight into how it has been successfully used to fulfill a variety of objectives.

The goals of the MasCotTE project2 were to investigate the possibility for WCET analysis techniques to consider off-the-shelves processors with different levels of complexity. The basic functionalities of OTAWA coupled to our GLISS tool made it possible to model two processors used in automotive applications: the Freescale 16-bit Star12X and the high-performance Freescale MPC5554. This work has been reported in [START_REF] Cassé | Experimentation of WCET Computation on Both Ends of Automotive Processor Range[END_REF].

In the MERASA project 3 , the objective is to design a multicore processor able to execute mixed-critical workloads while offering timing predictability to hard real-time tasks. Two approaches to WCET analysis are considered: measurement-based techniques, with the RapiTime tool and static analysis, with the OTAWA toolset. Abstractions of the MERASA multicore and support for the TriCore ISA have been developed, as well as models for the specific components of the architecture: dynamic instruction scratchpad [START_REF] Metzlaff | Predictable Dynamic Instruction Scratchpad for Simultaneous Multithreaded Processors[END_REF], data scratchpad used for stack data, predictable bus and memory controller [START_REF] Paolieri | Hardware Support for WCET Analysis of HRT Multicore Systems[END_REF]. In addition, OTAWA has been used to analyze the WCET of a parallel 3D multigrid solver and used as a pilot study for the project. The contribution of this work, reported in [START_REF] Rochange | WCET Analysis of a Parallel 3G Multigrid Solver Executed on the MERASA Multi-core[END_REF], is in (a) the analysis of the synchronizations between parallel threads and, (b) the tight evaluation of the synchronization-related waiting times, based on the ability of OTAWA to analyze the WCET of specified partial execution paths.

The MORE project4 aims at providing a framework for the investigation of code transformations used to improve several criteria like code size, energy consumption or worst-case execution time. This framework is being designed using the OTAWA toolbox and includes evaluation tools (for worst-case execution times or energy consumption), transformation tools (emulators for code compression and data placement in memories, a plugin to control GCC optimizations through the GCC-ICI interface [START_REF] Huang | Transforming GCC into a research-friendly environment -plugins for optimization tuning and reordering, function cloning and program instrumentation[END_REF]) and an iterative transformation engine that explores the transformation space to determine the best combination of transformations with respect to the requirements. The original usage of OTAWA lies in the design of transformation emulators that use the annotation system. For example, code compression is implemented the following way: profiling data is collected using the cycle-level simulator available in OTAWA; the instructions that should be compressed are determined; then each instruction is annotated with the address where it would be found in the compressed code; finally, the WCET is analyzed considering the addresses in the compressed code (the addresses are used for the instruction cache analysis). This way, it is possible to estimate the impact of compression algorithms without having to generate the real compressed code neither the corresponding code loader for WCET analysis. Further details can be found in [START_REF] Cassé | A Framework to Experiment Optimizations for Real-Time and Embedded Software[END_REF].

Conclusion

Safe scheduling of critical tasks in hard real-time systems requires having knowledge of their Worst-Case Execution Times. WCET analysis has been a research topic for the last fifteen years, covering various domains from flow analysis (typically determining loop bounds and infeasible paths) to low-level analysis (computing the execution times of basic blocks taking into account the architecture of the target hardware). Several research groups have designed their own WCET tool to support their research and all these tools are complementary but redundant to a certain extent. It would probably be fruitful to promote their interoperability and we believe that the OTAWA toolbox presented in this paper exhibits interesting features for this purpose. First of all, it provides an abstract interface to the program to be analyzed and to the target hardware, which make it possible to develop platform-independent analyses. Second, it features a number of facilities that allow fast implementation of new analyses with a powerful means to capitalize their results towards the final WCET computation. It also provides an efficient mechanism to handle the dependencies between analyses. OTAWA has been successfully used in several projects and has proved its flexibility and openness, as well as the efficiency of its key features.

The OTAWA toolbox is available under the LGPL license from www.otawa.fr.

Fig. 1 .

 1 Fig. 1. Overview of the OTAWA framework

Fig. 3 .

 3 Fig. 3. Colored display of source code

Fig. 4 .

 4 Fig. 4. Colored display of a CFG

An exception is the case of programs written under the single-path programming paradigm[START_REF] Puschner | Writing temporally predictable code[END_REF] but this still remains marginal.

Maîtrise et Contrôle des Temps d'Exécution (Controlling Execution Times). This research has been partially funded by the French National Research Agency (ANR)

Multi-Core Execution of Hard Real-Time Applications Supporting Analysability. This research is partially funded by the European Community's Seventh Framework Programme under Grant Agreement No. 216415

Multi-criteria Optimizations for Real-time Embedded systems. This research is partially funded by the French National Research Agency (ANR) under Grant Agreement ANR-06-ARFU-002


Penelope M Sanderson
email: psanderson@itee.uq.edu.au

The power and the puzzles of auditory interfaces

Keywords: Auditory interface design, auditory displays, distraction, multimodal displays, multisensory integration, individual differences, music

des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Overview

Auditory interfaces are present in work and everyday environments as diverse as stockmarket trading, web traffic monitoring, patient monitoring, phones and personal assistants, vehicles, defence contexts, and assistive technologies for the visually impaired-I provide examples of recent designs. For the last 20 years in particular, auditory interface design has been stimulated by a multidisciplinary community drawn from computer science, psychology, physics, music, performance, acoustics, and other areas. During that time there has been greater clarity in how to design different forms of auditory interfaces, such as audifications, parameter-mapping sonifications, model-based sonifications, auditory icons, and earcons.

Successful design of auditory interfaces is challenging and requires attention to many issues, some of which are supported with a long theoretical and empirical tradition, and some which are not. Principles of auditory perception and psychoacoustics play a crucial role. Because auditory interfaces can inform or distract, or both, understanding how auditory attention works is also crucial if a display is to work as intended. Auditory interfaces work alongside information from the other senses such as vision, touch, and the vestibular system, so understanding how multimodal information is processed is increasingly important. Because auditory information is naturally heard by all within a certain range, understanding factors underlying people's tolerance of auditory displays is important, as is determining the appropriate scope of social participation in auditory information. Finally, individual differences can affect how well people can use auditory interfaces, yet such differences are seldom tested

In the address I will provide examples from our research on auditory displays that address some of the above questions, supplemented with work from other laboratories. Our main focus at The University of Queensland has been displays for medical contexts, but the principles we have uncovered extend well beyond healthcare. In one branch of our work we have addressed the problem of confusion between alarms. Recently we performed a controlled study of some controversial alarm sounds proposed by Patterson and Edworthy over 20 years ago-the results have important lessons for designers of auditory interfaces. In another branch of our work we have explored the question of how people combine auditory information with visual information from a head-mounted display while they are walking around and performing physical tasks. The results suggest that there is a subtle interplay of vestibular, optic, haptic, and auditory factors, and leave open many puzzles still to solve.

In much of our research, individual differences figure quite strongly. For example, we often find distinct performance differences between listeners with and without musical training, yet research and evaluations of auditory interfaces seldom classify participants in terms of musicality or music training. We have also uncovered differences in how easy and useful listeners at different points on Eyesenck's emphathy/psychoticism scale find it to work with auditory information. If such findings prove to be generalisable, they may have important implications for design of auditory interfaces and for how we deliver auditory information to listeners.