B Berthomieu

J.-P Bodeveix

S Dal Zilio
email: dalzilio@laas.fr

M Filali

D Le Botlan

G Verdier

F Vernadat

Real-Time Model Checking Support for AADL

Keywords: Formal verification, Architecture Description Languages, AADL, Model Driven Engineering

We describe a model-checking toolchain for the behavioral verification of AADL models that takes into account the realtime semantics of the language and that is compatible with the AADL Behavioral Annex. We give a high-level view of the tools and transformations involved in the verification process and focus on the support offered by our framework for checking user-defined properties. We also describe the experimental results obtained on a significant avionic demonstrator, that models a network protocol in charge of data communications between an airplane and ground stations.

Introduction

The increasing complexity of the software and hardware components used in safety critical systems has encouraged the adoption of new architectures and computing modules, more powerful, but also more complex than their ancestors. While these new architectures make development and maintenance easier, it also make it more difficult to fully understand, analyze and test these systems.

Formal verification methods, such as model-checking, are advocated as one of the solutions to this consistent increase in design complexity. While verification activities should be performed at all stages of the development process, there are strong incentives for carrying out as much verification as possible during the early phases, especially during the functional and architectural design phases. To support this trend, a number of high level system modeling languages have been proposed-often referred to as Architecture Description Languages, or simply ADL-that make it possible to analyze a system right from the design phase.

In this paper, we describe a model-checking toolchain for the behavioral verification of the Architecture Analysis and Design Language (AADL), an ADL standardized by the SAE that can describe both the hardware and software components of a system. The AADL standard address the problem of specifying and analyzing safety-critical, realtime embedded systems and is designed to support a Model-Driven Engineering approach. A key extension to this standard is the addition of a Behavioral Annex that refines the description of AADL threads behavior and that can therefore be used to describe more precisely the dynamic architecture of a system.

An advantage of AADL, compared to many other ADL, is to be based on a precise, unambiguous semantics. Indeed, the AADL standard describe precisely the behavior of all its components, such as: when can messages be exchanged; how do periodic and sporadic threads interact; how threads interact with communication or memory resources, such as registers or communication buses; . . . Another motivation for choosing AADL is the fact that it relies on classical hypothesis taken when building realtime systems for its runtime; that is, AADL favors implementability over expressiveness. This is an interesting characteristic, since it means that every feature of the language can be defined without resorting to any "unrealistic" primitives (like, e.g., the need for a global consensus primitive). Those characteristics are very helpful for developing semantics related tools, like automatic code generators, schedulability analysis or formal verification tools.

Our model-checking toolchain is based on a transformational approach, that is, on the interpretation (the translation) of an AADL model into a formal specification language that will take into account the behavior of the model but also the dynamic semantics related to the AADL standard. We give a highlevel view of the tools and transformations involved in the verification process and focus on the support offered by our framework for checking user-defined properties. We also report on some initial experiments carried out in order to evaluate our framework and give the first experimental results obtained on significant avionic demonstrator that models a network protocol in charge of data communications between an airplane and ground stations.

Our toolchain (see Fig. 1) is connected for its input to Adele [START_REF] Dissaux | ADELE: a versatile system architecture graphical editor based on AADL[END_REF], a semantic editor for the elaboration of AADL models. At the other end, verification activities ultimately relies on the Tina toolset [START_REF] Berthomieu | The tool TINA -Construction of Abstract State Spaces for Time Petri Nets[END_REF], that provides state-space generation and model-checking algorithms for timed Petri Nets. In-between, the generation of Tina models from an AADL description relies on the use of an intermediate formal specification language, named Fiacre [START_REF] Berthomieu | Fiacre: an Intermediate Language for Model Verification in the Topcased Environment[END_REF]. Fiacre offers a formal framework to express and inspect the behavioral and timing aspects of the system. The intermediate Fiacre model provides a formal representation of a system behavior that is suitable for analysis using a model-checking tool. Actually, most of the same toolchain can be used to derive formal specifications for the Tina and the CADP model-checker [START_REF] Garavel | Cadp 2010: A toolbox for the construction and analysis of distributed processes[END_REF].

The transformation from AADL to Fiacre is based on a Model Driven Engineering approach-where the adaptation and integration between tools is ensured by model-based techniques-and has been integrated into an Eclipse-based toolkit for system engineering called Topcased [START_REF] Farail | The TOPCASED project: a Toolkit in Open source for Critical Aeronautic SystEms Design[END_REF]. Topcased provides an open source, model oriented set of tooling and standard implementations and AADL was among the first languages supported in this project.

Our current toolchain is the result of the refinement and maturation of several previous versions of the AADL2Fiacre interpretation [START_REF] Berthomieu | Formal verification of aadl specifications in the topcased environment[END_REF][START_REF] Berthomieu | Formal Verification of AADL models with Fiacre and Tina[END_REF]. In this most recent iteration of our tool, we have focused on the modularity of the transformation with the goal to increase its maintainability and to simplify the proof of its correctness. Indeed, our previous implementation were based on a monolithic interpretation, that is supposed to generate fewer states but that was more delicate to debug and extend. One of the results obtained from our experimentations is that it is possible to follow a compositional approach for the encoding without degrading the performances; actually, we observe that following a more compositional approach makes it is easier to take benefit from symmetries in the system and to recover static dependencies than can help reduce the number of interleaving in the generated state space.

Outline:. We briefly describe the AADL execution model in Sect. 2 and focus on the behavior of threads and their interactions with communication events. Next, we give a high-level view of the tools and languages involved and illustrate the successive transformations required by our verification process. We describe the Fiacre language and its support for checking user-defined, realtime properties. In particular, we show how to use realtime specification patterns to check properties on the interpretation of an AADL model. Before concluding, we describe in Sect. 5 the results obtained on an AADL demonstrator.

AADL Execution Model and the Behavioral Annex

The AADL standard has been designed with the goal to provide a precise description of both the software components of a system (such as processes, threads, data, . . . ) as well as the execution platforms supporting them (processors, devices, buses, memory, . . . ). The language has both a graphical and a textual syntax and includes all the usual concepts found in a component-based languages: components are typed and are described using a semi-structured set of properties; the interface of a component can be defined using the notion of features; connections between components can be described using a notion of links.

The AADL execution model is suitable to describe real-time systems because it includes the main types of dispatch protocols for threads (periodic, aperiodic, sporadic, background) and the standard scheduling properties (period, priority, deadline, WCET, scheduling policy, . . . ). The language also includes the basic methods for interaction; components can communicate through ports, synchronous calls, and shared data. The AADL notion of process is the unit for describing the dynamic semantics of a system. A process represents a virtual address space, or a partition, that includes a program and all its sub-components. A process must contain at least one thread (or thread group) that represents a sequential flow of execution. Threads are the only AADL components that can be scheduled. The AADL Behavioral Annex is used to add specific real-time properties to each component of the dynamic design model and to define the software behavior at the thread level. We can define the real time properties of threads by setting specific properties in the AADL specification, like for instance the dispatch protocol (periodic or sporadic), the period (time) and the deadline (time). An example of thread declaration using the behavioral annex can be seen in the AADL code snippet of Listing 1. (An example of AADL graphical diagrams is given in page 16.) AADL is supported by several tools like the OSATE initial framework, which has been integrated into the Topcased environment and extended with OSATE-BA, the behavioral annex syntax analyzer. For editing models, Adele is a graphical editor which permits to create (graphical) AADL diagrams in Topcased and to generate AADL source code. Beside this set of tools for the generation and lexical analysis of AADL models, we describe a methodology and a set of tools for the formal verification of AADL specifications. For behavioral verification, we can only focus on a subset of AADL (In particular we do not take into account hardware components). We briefly describe the semantics of threads, their scheduling, and the communication through ports and shared data. Modes are not modeled yet, but we plan to integrate them in our tool.

T H R E A D t h A p p l i s F E A T U R E S { . . . } E N D t h A p p l i s ; T H R E A D I M P L E M E N T A T I O N t h A p p l i s . o t h e
Communication through ports. Communication, and the way it interacts with the scheduling of processes, is an important part of the AADL standard. AADL provides three types of ports-data, event and event data ports-that can be used to transmit data and control and describe the interface of a component. Data transmitted through ports is typed. Each input port is associated with a fresh variable that describes the state of the port. If a port has received nothing between two thread dispatches this variable is set to false. Each event or event data input port is also associated with a buffer that stores the dataor the number of events-sent through connected output ports. On thread dispatch, these inputs buffers are copied into the local memory of the thread. Properties can be used to customize the behavior of event and event data ports. For instance, the property Queue_size determines the maximum number of events or event data that can be received, while Overflow_handling_protocol describes the behavior of the port in case of overflow. (There are two default policies for overflow, drop newest and drop oldest.) The use of the Queue_size property is useful to generate a finite-state system from a model.

The diagram in Fig. 2 depicts the typical interaction between data communication through ports and thread dispatching. The axis on this diagram list the four possible state of a periodic thread: dispatch (the scheduler allows the thread to run); start; complete (the thread starts, respectively en, its computation); and deadline (that should always occur after a complete event, if the system is schedulable). Data ports have the simplest behavior: data is sent at the end of the thread execution, or at deadline, and is received at the next dispatch of the receiving thread. At the opposite, event and event data ports can send an event (resp. an event data) anytime during the execution of a thread. Events and event data are queued in the destinations ports. Input event and event data ports are delivered at the dispatch of the thread. Data communications between periodic threads can be declared as immediate or delayed. If the connection is delayed, data is sent at the deadline of the sending thread. If the connection is immediate, the receiving thread must wait the sending thread to complete. The received data will be available at the start of its (next) execution. All the possible combination of communication behaviors have been taken into account in our formal interpretation of AADL.

Communication through shared variables. As with all AADL components, data has a type and an implementation. The internal structure of the data is described in the data implementation. It is possible to specify whether different components have a shared access to a data subcomponent using the require_data_access connector. Correspondingly, the provide_data_access connector is used to state that a component allows other components access to one of its data subcomponent. The concurrency protocol used to access a data is defined by a data property called concurrency_control_protocol. This concurrency protocol can be implemented through different concurrency control mechanisms such as mutex, semaphore . . . Concurrency protocols are a significant source of variability in the definition of the AADL syntax. We take into account this variability in our interpretation of AADL to Fiacre (and the possibility to extend the language with new, user-defined, protocols) by providing an extensible library of protocols and providing supports for checking the correctness of these protocols. That is, support to prove that the semantics of a protocol (such as mutual exclusion) is preserved by our interpretation.

The Fiacre Specification Language and Realtime Properties

Our verification toolchain is based on a transformation from AADL into an input format suitable for our model-checking tools. This transformation relies on the use of the Fiacre specification language to facilitate the processing; simplify the maintainability of our tool (e.g. when the AADL standard is revised); and simplify the reasoning on the correctness of the transform.

The Fiacre language has been designed in the context of the Topcased project [START_REF] Farail | The TOPCASED project: a Toolkit in Open source for Critical Aeronautic SystEms Design[END_REF] to serve as an intermediate format between high-level description languages and formal verification tools. The use of a formal intermediate modeling language has several benefits. First, it helps reduce the semantic gap between high-level models and the input format of verification tools that often relies on low level formalisms, such as Petri Nets or process algebra. Second, the use of a formal language makes it possible to define precisely the semantics of the input language "only once" and to share this work among different verifi-cation toolchains. This is particularly helpful when we try to address emergent system modeling language, whose semantic evolves rapidly.

An Example of Fiacre Specification: the Periodic Thread Controller

Fiacre is a formal specification language designed to represent both the behavioral and timing aspects of real-time systems. Fiacre supports two of the most common communication paradigms: communication through shared variable and synchronization through (synchronous) communication ports. In the latter case, it is possible to associate time and priority constraints to communication over ports. The design of Fiacre is inspired from decades of research on concurrency theory and real-time systems theory. For instance, its timing primitives are borrowed from Time Petri nets, while the integration of time constraints and priorities into the language can be traced to the BIP framework [START_REF] Basu | Modeling heterogeneous real-time systems in BIP[END_REF]. For composing components, Fiacre incorporates a parallel composition operator and a notion of gate typing which were previously adopted in Lotos-NT. We briefly describe the language. The detailed syntax and formal semantics of the Fiacre can be found in [START_REF] Berthomieu | Fiacre: an Intermediate Language for Model Verification in the Topcased Environment[END_REF].

Fiacre programs are stratified in two main notions: processes and components. Processes describes the behavior of sequential components. A process is defined by a set of control states, each associated with an expression that specifies state transitions (introduced by the keyword from). Expressions are built from deterministic constructs available in classical programming languages (assignments, conditionals, sequential composition, ...); non-deterministic constructs (choice and non-deterministic assignments); communication events on ports; and jump to next state (introduced by the keywords loop and to). Components describes the composition of processes, possibly in a hierarchical manner. A component is defined as a parallel composition of components and processes communicating through ports and shared variables. A component can be used to restrict the access mode and visibility of shared variables and ports, to associate timing constraints with communication ports and to define priority between communication events. We give an example of Fiacre specification in Listing 2.

The process periodic, defined in Listing 2, models the behavior of an AADL periodic thread. We consider the simplest case, where the period is equal to the deadline and where no data is exchanged (the ports have the type none). The process may interact with its environment through four external ports, passed as parameters of the process declaration (line 3 of Listing 2): a port for dispatch (d), complete (c) and deadline events (dl) and a port (w) that is used to check that the thread has stopped executing-it is idle (s = p_idle)-before it reaches a new period. The periodic process loops on the state s0 and relies on a local variable (st) to encode the current condition of the thread (idle, ready or error). The select operator is used to model a non-deterministic choice between several transitions, separated by the symbol [], whereas the keyword unless is used to assign the highest priority among a set of transitions. Hence, if st has the value p_err, the process necessarily goes to the state sched_error where it blocks (line 13). In this transition, the wait operator is used to express the fact that the change is instantaneous (it takes a duration in the time interval [0, 0]).

The component main is used to create several instances of the periodic thread. In our encoding of periodic threads, we declare a new port w for every instance of the process periodic; this port is associated to a temporal constraint of the form [T ; T ], where T is the period of the thread (in our example, T = 20). On the opposite, the ports d, c and dl are instantaneous (they are associated to the time constraint [0; 0]) and constrained by a priority relation of the form c > dl > d.

We can express (a very weak form of) the real-time requirements of the periodic thread using formulas in a temporal logic, like LTL for instance. For example, we can express the requirement that-in the absence of scheduling errors-a deadline event is always followed by a dispatch. This property can be easily expressed in LTL with a formula of the form:

deadline ⇒ ♦ dispatch (1)
A strong limitation of an approach based on LTL model-checking is that it is not possible to express timing constraints like, for example, that the dispatch should happen before T time units of the deadline (where T is the period of the thread). Another limitation is that it is necessary to understand how events from the initial AADL model are translated into events or states in the Fiacre model. In the following section, we show an extension to the Fiacre language that makes it easier to express timed temporal properties. This extension was specially added to alleviate the two limitations that we just pointed out.

Expressing Real-Time Requirements in Fiacre

The chief purpose of the Fiacre language is to express the behavior of realtime, reactive systems. Nonetheless, it is also possible to declare, inside a Fiacre model, a set of properties that should be valid on the model. Each property is declared in the Fiacre model using the keyword property; for example, line 21 of Listing 2 declares a requirement equivalent to the LTL property [START_REF] Dissaux | ADELE: a versatile system architecture graphical editor based on AADL[END_REF].

In this section, we briefly describe the set of realtime specification patterns available in our framework. A complete description of the language is given in [START_REF] Abid | Real-Time Specification Patterns and Tools[END_REF]. Our language extends the property specification patterns of Dwyer et al. [START_REF] Dwyer | Patterns in property specifications for finite-state verification[END_REF] with the ability to express time delays between the occurrences of events. The result is expressive enough to define properties like the compliance to deadline, bounds on the worst-case execution time, etc. The advantage of this approach is to provide a simple formalism to non-experts for expressing properties. Another benefit is that properties expressed with this pattern language can be directly used with our model-checking tools. The pattern language follows the same classification that in Dwyer's work, with patterns arranged in categories such as occurrence or order patterns. In the following, we study examples of response and absence patterns.

Response pattern with delay. This category of patterns can be used to express delays between events, like for example constraints on the Worst Case Execution Time of a task. The typical example of response pattern states that every occurrence of an event, say e 1 , must be followed by an occurrence of an event e 2 within a time interval I. This pattern is denoted: e 1 leadsto e 2 within I .

(leadsto-within)

Events that are observable at the Fiacre level are: a process entering or leaving a state; a variable changing value; a communication through a port. Therefore, considering the (sketch of the) interpretation of AADL threads in Fiacre given in the previous section, we can use the notation t/evente to refer to a synchronization over the port e on the controller process for the thread t. Hence, we can check that the execution time of the thread periodic is less than T units of time with the following requirement, meaning that the time between a dispatch and a completion is always less than T :

property req2 is (main/1/event c) leadsto (main/1/event d) within [0; T]
Absence pattern with delay. This category of patterns can be used to specify delays within which activities must not occur. A typical pattern in this category can be used to assert that an activity, say e 2 , cannot occur between d 1 -d 2 units of time after the occurrence of an activity e 1 . This requirement corresponds to a basic absence pattern in our language: absent e 2 after e 1 within [d 1 ;

(absent-after)

An example of use for this pattern is the requirement that we cannot have two dispatch events for the same periodic thread in less than the period, say T :

property req3 is absent (main/1/event d) after (main/1/event d) within ]0; T[ A more complicated example of requirement is to impose that, in every run such that a dispatch is followed by a completion in less than T , then there are no scheduling error. This requirement can be expressed using the composition of the properties req2 and req4: property req4 is absent (main/1/state sched_error)

Behavioral Verification with Tina

The "meaning" of a Fiacre program can be expressed as a Timed Transition System (TTS) [START_REF] Henzinger | Timed Transition Systems[END_REF], defined from the states of the system processes and from timed transitions between these states. The frac compiler can be used to build a TTS from a Fiacre program. The Tina verification toolbox [START_REF] Berthomieu | The tool TINA -Construction of Abstract State Spaces for Time Petri Nets[END_REF] offers several tools to work with TTS files. For instance, for verification purposes, TTS specifications can be used by selt-a model-checker for a State-Event version of Linear Temporal Logic (LTL)-and by muse-a model-checker for the µ-calculus.

Beside the usual analysis facilities of similar environments, the essential components of the Tina toolbox are state space abstraction methods and model checking tools that can be used for the behavioral verification of systems. This is in contrast with the broader notion of functional verification, in that we attempt to use formal techniques to prove that requirements are met, or that certain undesired behaviors cannot occur-like for instance deadlocks-without resorting to actual tests on the system. In this context, state space abstractions are vital when dealing with timed systems, that exhibit a potentially infinite state spaces. Tina offers several abstract state space constructions that preserve specific classes of properties like absence of deadlocks or bisimilarity. A variety of properties can be checked on abstract state spaces: general properties-such as reachability properties, deadlock freeness, liveness, . . . -specific properties relying on the linear structure of the concrete space state-for example LTL formulas, test equivalence, . . . -or properties relying on its branching structure.

Instead of requiring end-users to provide properties written in a temporal logic, we propose a set of high-level validation patterns that simplify the elicitation of formal requirements. This pragmatic approach help us mitigate some of the complexity that is associated with the use of model-checking tools by novice users. We have implemented an extension to the frac compiler that accepts the declaration of realtime specification pattern. Currently, timed patterns, such as the "leadsto property", are compiled into an observer that is automatically composed with the system at the level of the Timed Transition System. In the case where the pattern is not valid, we obtain a counter-example, that is a sequence of events (with time information) that leads to a problematic state.

Overview of the AADL Translation and Verification of Libraries

We do not describe precisely the structure of the generated code. In a nutshell, we associate a pair of Fiacre processes to each AADL thread and map each AADL port to a communication port in Fiacre. (Since we focus on the behavior of the system and not its hardware architecture, we take a flattened view of the AADL model as a set of communicating threads.) Timing information, such as the period of threads, are modeled using the time constraints mechanism provided by Fiacre ports.

The transformation of AADL into Fiacre relies on AADL properties and on the behavioral annex of AADL that has been developed and integrated to the OSATE environment. We follow a model-driven approach. Alongside a metamodel of AADL, we have developed a meta-model of the Fiacre language that is integrated in the Topcased toolchain. Hence the transformation from AADL to Fiacre can be obtained through model transformation.

Our interpretation is fully compositional. Every thread is encoded using two Fiacre processes, one for its controller and another for encoding its behavior. Additional process instances are created to model the scheduler and the communication resources. The controller process is in charge of the interaction between the thread and its scheduler (through the ports for the dispatch, complete and deadline events) and for recovering data from its event data ports at the right moment. The controller process is also in charge of the "concurrency protocols" associated with the shared variables accessed by the thread (see the discussion at the end of Section 2). Conversely, the behavior process is used to model the part of the thread definition associated to its behavior specification (given using the AADL Behavioral Annex), if any. For the behavior process, the interpretation of the AADL BA is quite straightforward, since the behavioral annex is essentially a glorified syntax for a state transition system. For the controller process, our interpretation relies on a library of components similar to the code of the periodic controller given in Listing 2. We provide one process for every kind of behavioral resource: threads (periodic, sporadic, . . . ), event and event data port, data connection, processes and sub-programs (that is schedulers).

The translation takes into account a substantial subset of the AADL standard and all basic properties are considered when generating a Fiacre model. More particularly, we take into account AADL priorities, as well as access to shared variables. For the moment, while periods can change, we assume that priorities are fixed. Also, we do not take into account preemption or support for multiprocessor architecture (in particular we do not take into account the value of the Actual_Processor_Binding property).

Next, we show how we can use our support for expressing user-defined properties in Fiacre to check the consistency of our interpretation of AADL models into Fiacre processes. The correctness of our interpretation heavily relies on the library of AADL components that describe the communication and synchronization protocols used to model the underlying execution model. This library is made of several patterns of Fiacre code that are parameterized by types (the types of the values exchanged on the communication channels transferred data); integers (e.g. the size of the communications queues); and even functions (used for data encoding). We do not necessarily know how to check these patterns of Fiacre code automatically. Therefore, several techniques and tools can be used, depending on the nature of the component in question: model-checking can be used in the case of "finite-state" code, while theorem proving techniques may be necessary in the most complex cases. (In a separate paper [START_REF] Bodeveix | On the Mechanization of an AADL Subset[END_REF], some of the authors describe the framework necessary to carry out proofs on Fiacre specifications using the Coq assistant prover.) Another source of complexity lies in the fact that we need to close each code pattern and put it into an environment that models the context where an AADL component can be used.

In some cases-like with the controller for AADL periodic threads-it is possible to generate properties of our embedded requirement specification language that are enough to prove the correctness of the code pattern. To avoid the quantification over all possible context where the code can be inserted, these properties have to be checked each time a new instance of the AADL component is created. For example, when checking the correctness of the interpretation, we need to prove that the system is schedulable; meaning that the component enters the error state (sched_error) if and only if c (the complete event) is absent between a d and dl event. This is a consequence of the following property, (P0a), where t stands for the identifier of the thread instance. Our current toolchain is the result of the refinement and maturation of several previous versions of the AADL2Fiacre interpretation [START_REF] Berthomieu | Formal verification of aadl specifications in the topcased environment[END_REF][START_REF] Berthomieu | Formal Verification of AADL models with Fiacre and Tina[END_REF]. In this most recent iteration of our tool, we have focused on the modularity of the transformation with the goal to increase its maintainability and to simplify the proof of its correctness. Indeed, previous versions of our tool where based on a monolithic interpretation of AADL, where events and data exchanges were mediated by a specific glue process that manage communication and scheduling protocols. Another major contribution of this work is to define a framework for declaring user-defined properties at the AADL-level. The same framework is used to generate "proof-obligations" that can be checked using our model-checking toolchain and that ensure that every code pattern is faithful to its intended semantics.

Experiments

In this section, we report on experiments carried out [START_REF] Dissaux | ADELE: a versatile system architecture graphical editor based on AADL[END_REF] for schedulability analysis through model checking and (2) on the dynamic architecture for a network protocol (NPL) in charge of data communications between an airplane and ground stations. For the first study, we observe that model checking allows for a more precise problem analysis. For the second study, we describe the architecture of a communication system, the properties that have been checked and give some quantitative information.

Schedulability analysis

Analytic methods are well known and extensively applied to schedulability analysis. In order to illustrate their limits, we have compared the results provided by the Chedar tool [START_REF] Singhoff | Cheddar: A flexible real time scheduling framework[END_REF] and our model-checking based tool. The considered example is a typical non-conservative case which combines dispatch offsets, non preemptive scheduling and non deterministic execution time. It has been modelled in AADL but can be summarized by the following As Cheddar does not know how to manage a BCET..WCET interval, the simulation is done using the WCET bound and the system is declared to be probably schedulable. However, the Fiacre-based analysis, through the expression of schedulabilty by absence of deadlock in some specific state, finds the system schedulable if the execution time is exactly the WCET and non schedulable otherwise. Consequently, the Fiacre-based analysis is more precise. Furthermore, it allows to take into account the precedence specified by the AADL execution model (linked to immediate communications). In usual analytic-based schedulability tools like Cheddar, this would require to encode precedence as priorities and to duplicate threads of which precedence depends on the task instance. Lastly, the Fiacre-based tool can take into account data (of finite domain) to make even more fine grain analysis. However, this method comes at the cost of the model-checking state exploration.

Network protocol

The considered network protocol, named NPL, implements a communication protocol based on the Trivial File Transfer Protocol (TFTP) allowing a pilot and ground stations to receive and send information relative to the plane: weather, speed, destination, . . . On the hardware side, the NPL software is running on an IMA computer and consists of one ARINC 653 partition [START_REF]ARINC 653 -avionics application software standard interface, specification 653[END_REF] that communicates with several other embedded computers through an AFDX field bus. The dynamic semantics of these IMA components are taken into account in the AADL model. On the software side, the protocol layer of the NPL is in charge of handling messages exchanged between on-board applications and lower ground systems. Messages are exchanged using a realtime extension of TFTP in order to ensure predictable response time. For instance, the transport layer can withstand the loss of messages, which are automatically re-emitted after a timeout. Consequently, the NPL stack can be described using three different layers: a first layer for the high-level APplications Protocols (APP); the underlying transfer protocol layer (TFTP in this case); and an intermediate, MiddleWare Protocol (MWP) layer that mediates the communication between APP and TFTP.

The overall behavior of the MWP layer can be modeled by a communicating automaton with three main states (closed, opening and open) that correspond to the states of the "virtual communication" channel between the aircraft and the ground. While the number of states is small, the dynamics of the system is quite complex as it requires about sixty transitions: inputs and outputs actions of the automaton correspond to requests received or sent from/to the on-board applications or the lower ground layers. The complete NPL system is composed of several applications, and every data-link application has its own instance of the communication automaton. The main property that should be checked in this context is the potential accessibility of each state, meaning that the protocol can always proceed to completion.

The behavior of the NPL was originally defined by means of sequence diagrams describing usage scenarios in nominal and default cases. These sequence diagrams have all been checked against our automata-based specification in order to assert the correctness of our modeling. A typical usage scenario is given in Figure 3 that details a registration sequence between an application protocol (APP); the MiddleWare Protocol (MWP); the transfer protocol; and ground layers tasks (the dashed, vertical line). This is the most significant activity in the NPL since every application has to register before starting any data exchanges with ground stations. The scenarios illustrates two modes of the system. If the MWP is in state closed and receives a registration_request message from the APP, it initiates a connection (the MWP goes into state opening). If the MWP is in the opening state and receives a data_indication message from TFTP then the connection is established (the MWP enters state open).

Protocol Modelling with AADL

The NPL software subset has been modeled as a single application composed of one main AADL component. This model is mainly derived from an implementation of the system in the C language provided by Airbus (see e.g. [START_REF] Berthomieu | Formal Verification of AADL models with Fiacre and Tina[END_REF]). The AADL model specifies both the hardware and software architecture of the component and is composed of: an AADL processor with its memory (AADL hardware component types); and one main AADL process that encloses five AADL threads (AADL software component types). The diagram in Fig. 4 details the architecture of the main AADL process using the AADL graphical syntax. (This diagram has been edited with the ADELE graphical modeler [START_REF] Dissaux | ADELE: a versatile system architecture graphical editor based on AADL[END_REF].) We have highlighted the five threads of the NPL component, which carry out the main functions of the application. A first thread takes care of the data-link applications (thApplis) while there is another thread for the message scheduler (thSeqMsgMWP). The remaining threads are used for: implementing the MWP state automaton (thMWP); supporting the Timer functions (thTIMER); and supporting the underlying TFTP protocol (thTFTP). In our model, all these threads are periodic with periods ranging from 5 ms to 20 ms.

The architecture of data connections between threads is regular. Each pair of threads (excluding the timer thTIMER) is connected through at least two memory buffers that are used to store the data exchanged between the threads over asynchronous communication channels. A first buffer is used to hold a wakeup signal while the other carries the message part. For instance, the buffer Wkup_Appli is used to store the "wake-up" signal from the MWP controller, thMWP, to the data-link applications. While this choice complicates the description of the system, we chose to model communication between threads using All the threads adhere to a common communication protocol. When a thread needs to communicate with another thread, it first put its message into the dedicated buffer (for instance Prim_Appli) and then put its identifier into the associated wake-up buffer. When a thread receives an identifier into its wake-up buffer (pooling), it reads the message and then clear the identifier. Some threads have also access to data generated outside the MWP, like for example message frames exchanged with the environment, or are connected through specific event ports (for instance, the timer and the MWP controller threads). Data exchanged with the environment are defined as structured, composite data formed from several integer fields.

In our model, the behavior of each thread is expressed using the AADL Behavioral Annex syntax. The complete AADL specification of the MWP system requires eight graphical diagrams (of the same complexity than the one given in Figure 4). In its textual format, this amounts to about 800 lines of AADL source code with more than half of this code automatically generated from the graphical specification. On these 800 lines, the behavior of the MWP controller amounts to about 300 lines of code. This specification can be easily reused. Hence, several applications and MWP threads could be modeled by using several instances of the same AADL specifications with update connections between them.

Functional Verification by Model-Checking

We used our verification toolchain to check properties on the AADL specification of the Air Traffic Control system. These properties corresponds to requirements expressed by the system engineers. Our experiments were successful as it is possible to verify a substantial architecture model extracted from the ATC. The main properties automatically checked on this model can be grouped into three main categories: (1) absence of deadlocks, e.g. the system can not lock himself due to a wrong synchronization; (2) healthiness, e.g. every thread (task) can run and compute infinitely often; and (3) absence of dead states, e.g. every internal behavior state of every thread is reachable. We also checked several properties related to the correctness of our interpretation, e.g. to check that the AADL semantics is preserved in our translation to Fiacre.

The use of formal verification techniques at the model-level is particularly interesting in the case of the ATC system. Indeed, the design used in the definition of the communication architecture is prone to concurrency access problems since all threads must agree on the same order when accessing data.

We give more details on the properties that have been formally checked on the model. The goal was to defined a set of simple "property patterns" for dynamic architecture verification and to give them to avionics software engineers with no previous knowledge of model-checking or temporal logic. We defined three (untimed) patterns that were used by system engineers to detect real-time pathologies and that correspond to the three categories of requirements listed before.

• NoGlobalDeadlock, applies to the whole model. This pattern checks for absence of global deadlocks, that is, the system can not lock himself due to a wrong synchronization;

• Unreachable (exp), applies to an internal state. This pattern checks for the presence of dead states. This is useful to check wether a thread may reach a given behavior state;

• Resettable (exp), applies to a thread dispatch state. This pattern checks for healthiness, that is the fact that a given thread can be dispatched infinitely often.

These three patterns can be directly encoded in terms of the LTL-dialect used by the selt model-checker. The pattern NoGlobaldeadlock is expressed by the formula [] -dead, meaning that for every reachable state (always) it is false that no transitions can be taken from this state. The pattern Unreachable (exp) is equivalent to the formula []-exp (or absent exp), meaning that always, the property exp is false. Finally, the pattern Resettable (exp) is equivalent to the formula []<>(exp), meaning that always, we will eventually (after a finite number of transitions) enter in a state where the property exp is satisfied. For example, the pattern Resettable (thApplis/event d) can be used to test whether the thread thApplis will (always) eventually be dispatched. In addition to these simple (untimed) patterns, we have also used the leadsto pattern to find an upper limit on the time needed for the completion of the sequence diagram given in Fig. 3.

With respect to performances, our verification toolchain is able to handle the generation of the complete state space of the demonstrator -which amounts to about 110 000 states and 150 000 transitions for the Fiacre intermediate modelwithout any memory overflow on a typical basic development computer (Intel dual-core processor at 2 GHz clock frequency, and 2 Go of RAM memory). The abstract state space construction and system compiling are performed, on the same computer, in less than 5 minutes with a memory footprint in the order of 500 Mo of RAM. On examples of this size, the model checker included in Tina is able to generate the whole state space of the system in 15 s and to prove a formal properties in a few seconds. For example, it takes less than 2 minutes to check the 22 properties derived from the patterns listed before: one test for NoGlobalDeadlock; 5 resettable property (one for each thread in the system); and 16 reachability test (one for each state of each thread).

The state space obtained with our new, modular implementation of the AADL2Fiacre generator is slightly smaller than the one obtained with our previous, monolithic approach [START_REF] Berthomieu | Formal Verification of AADL models with Fiacre and Tina[END_REF]. This is a nice surprise, since a monolithic interpretation is supposed to produce a system with less interleaving (and therefore fewer states). The reason behind this surprising result is that we can use a finer treatment of priorities between independent threads with a modular approach and therefore actually reduce the number of interleaving in this case.

This experimentation, while still modest in size when compared to a fullblown avionic protocol, gives a good appraisal of the use of formal verification techniques for real industrial software. These experimental results are very encouraging. In particular, we can realistically envisage that system engineers could evaluate different design choices for the MWP protocol stack in a very short time cycle and test the safety of their solutions at each iteration.

Related works

Related work concerning the verification of AADL models is organized in three subsections: model-checker-based tools for verifying AADL models through their translation to the input language of existing tools, model-checking-based verification of the translation to check intrinsec AADL semantics properties, and analytic methods applying scheduling analysis techniques to high level abstractions.

AADL subsets

A number of studies have explored how to interpret the AADL standard in a formal setting.

A specification of the AADL execution model in the Temporal Logic of Actions (TLA) is given in [START_REF] Rolland | Towards a formal semantics for AADL execution model[END_REF] that defines one of the earliest formal semantics for AADL. This encoding takes into account a fixed priority scheduling protocol with preemption, the management of modes and communication through ports and shared data. Our approach is based on an interpretation of AADL specifications, including the Behavioral Annex, in the Fiacre language.

A direct encoding from AADL to Petri net is studied in [START_REF] Vergnaud | Modélisation des systèmes temps-réel répartis embarqués pour la génération automatique d'applications formellement vérifiées[END_REF] that takes into account a more limited subset of AADL (it restricts the behavior of software components and omits realtime properties of elements).

Other target formalisms have also been studied. An encoding of AADL in BIP is presented in [START_REF] Bozga | Modeling synchronous systems in BIP[END_REF] that focuses on the behavioral annex as well as on threads, processes and processors. The approach is improved in [START_REF] Pi | Modeling AADL Data Communication with BIP[END_REF] by taking into account the management of AADL communication protocols. When compared to BIP, the current version of Fiacre provides less high-level constructstherefore encodings are less direct-but offers better compositional and real-time properties. The library of AADL component defined in our approach is a first step toward providing higher-level modeling construct in Fiacre.

Some works consider different technologies for defining the behavior of software components. In [START_REF] Jahier | Virtual Execution of AADL Models via a Translation into Synchronous Programs[END_REF], the authors study the case where behaviors are described in a synchronous language, such as Scade or Lustre. In this case, they define a direct translation that generate an executable model of the software behavior. Such a model is usable for early simulation, but also for formal verification, using tools available for Scade and Lustre.

Within the COMPASS project, [START_REF] Bozzano | A model checker for aadl[END_REF] propose the verification of linear or branching time properties on AADL-like models with hybrid behaviors. Probabilistic properties are also considered. However, the semantics of AADL is not precisely considered, while it is one of the main features of our proposal, together with the management of time.

The ABV-A verifier [START_REF] Björnander | Abv -a verifier for the architecture analysis and design language (aadl)[END_REF] does not translate the AADL model to an existing modelling language. It directly evaluates temporal logic formulas (written in CTL) on a state space generated from the AADL model, including the behavior annex. However, timing information are ignored and the adequacy with the AADL runtime semantics is not discussed.

In [START_REF] Ölveczky | Formal semantics and analysis of behavioral aadl models in real-time maude[END_REF], the semantics of AADL models in specified in real-time Maude: timed rewriting rules specify the update of the system configuration. The time domain can be discrete or dense. Time advances non deterministically until reaching the date of the next event. Quantitative linear time properties can be defined and verified by the Maude model checker. However, the compositional Maude-based semantics introduces to much asynchrony and leads to inefficient model-checking. For this purpose a synchronous variant of the tool has been developped [START_REF] Bae | Synchronous aadl and its formal analysis in real-time maude[END_REF], but takes as input a subset of AADL (only periodic and synchronous threads, restricted communication patterns).

Finally, other works [START_REF] André | Modeling of immediate vs. delayed data communications: from AADL to UML Marte[END_REF][START_REF] Feiler | Efficient embedded runtime systems through port communication optimization[END_REF] have focused on AADL data communication handling but leave the connection with a formal verification tool as a perspective.

Translation verification

Another distinctive feature of our work is the concern for checking the correctness of our interpretation. In this paper, we concentrate on the definition of ways to check properties on a AADL specification using model-checking, how to express properties and what kind of properties can be expressed. In another related work [START_REF] Bodeveix | On the Mechanization of an AADL Subset[END_REF], we describe the semantical framework used for the transformation of AADL into Fiacre and how to check the correctness of this translation using proof assistant. This companion paper gives more details on the formal semantics of subsets for both AADL and Fiacre and gives a high-level description of the translation from one framework to the other.

Analytic methods

Finally, we have also compared our approach with other AADL related tools, outside the domain of formal verification, for example with scheduling analysis tools, such as Cheddar [START_REF] Kerboeuf | Comparison of six ways to extend the scope of cheddar to aadl v2 with osate[END_REF], that need to analyze the behavior of (or even simulate) AADL models. Even if analytical methods outperform model-checker when the scheduling policy and the analyzed model fall into one of the cases covered by the tool, we have easyly illustrated the limitations of analytical and simulation-based approaches using a simple, non-conservative model combining offsets and non-preemptive scheduling.

Conclusion

This paper describes a formal verification toolchain for AADL that takes into account the Behavioral Annex. We give a high-level view of the tools and the transformations involved in our verification process. While the methodology of our verification toolchain has already been described in previous works [START_REF] Berthomieu | Formal verification of aadl specifications in the topcased environment[END_REF], this paper is the first occasion to report on a experimental study that was conducted on a significant avionic demonstrator. It is also the first time that we describe our modular interpretation approach as well as the use of specification pattens to check basic properties on the correctness of our encoding (such as the schedulability of the resulting system). This study gives some interesting directions for further studies. There are several areas for improvements, such as: enhancing and standardizing our library of AADL component and validation patterns; improving the behavioral modeling capabilities of the Adele editor (e.g. with a graphical representation of the behavioral annex); and improving the integration of the transformation toolchain in Topcased, in particular with respect to a better presentation of the verification results to the end user.

Work is still ongoing to improve the tools involved in our verification framework. A number of extensions to Tina are being evaluated, concerning new tools, new front-ends, and new back-ends. For instance, we are experimenting with the addition of suspension/resumption of actions to Time Petri nets, which is of great value for modeling scheduled real-time systems. Alongside these works on tools, our current efforts are directed toward three main objectives:

(1) Simplifying the definition of logical properties. End users of verification tools should not be required to master temporal logic. To improve the usability of our approach, we are currently investigating the proposition of a kit of predefined AADL requirements or the integration with an AADL-based requirement specification framework.

(2) Improving error reporting. We plan to provide a "debugging" procedure, which should take as input a counter-example produced during the modelchecking stage and convert it to a trace model of the initial AADL description. These traces should be played back using simulation tools.

(3) Improving the Verification Process. We are currently investigating extensions to the Fiacre language in order to ease the interpretation of high-level description languages and to optimize the verification process. One welcome addition would be to integrate the notion of modes directly in Fiacre. We also plan to address the problem of specifying scheduling and time-constrained behaviors within Fiacre. These aspects should have a great impact on the overall performance of the analysis tool.

Figure 1 :

 1 Figure 1: AADL to Tina toolchain

Listing 1 :

 1 r s S U B C O M P O N E N T S a p p _ m s g : D A T A t y p e s : : m s g . i m p l ; { . . . } P R O P E R T I E S D i s p a t c h _ P r o t o c o l => P e r i o d i c ; D e a d l i n e => 10 m s ; P e r i o d => 10 m s ; { . . . } A N N E X behavior_specification { * * s t a t e s --S t a t e s D e c l a r a t i o n s t a r t : i n i t i a l s t a t e ; p e n d i n g : complete s t a t e ; r e g i s t e r : complete s t a t e ; d i s r e g : complete s t a t e . . . t r a n s i t i o n s s t a r t -[ ]→ p e n d i n g { a p p _ m s g . r e q := 0 ; a p p _ m s g . d a t := 0 ; } ; p e n d i n g -[ on a p p _ m s g . r e q = R e g ]→ r e g i s t e r { a p p _ m s g . r e q := 0 ; } ; p e n d i n g -[ on a p p _ m s g . r e q = D i s r e g ]→ d i s r e g { a p p _ m s g . r e q := 0 ; } ; { . . . } * * } ; E N D t h A p p l i s . o t h e r s ; Example of AADL behavior description

Figure 2 :

 2 Figure 2: communication through ports in AADL.

  type p _ s t a t e i s u n i o n p _ i d l e | p _ r d y | p _ e r r end process p e r i o d i c [ d : none , c : none , d l : none , w : none ] i s s t a t e s s0 , s c h e d _ e r r o r var s t : p _ s t a t e := p _ r d y i n i t to s 0 from s 0 s e l e c t c ; s t := p _ i d l e ; l o o p ( o n s t=p _ r d y ) ; d l ; l o o p d ; l o o p w ; s t := ( s t=p _ r d y ? p _ e r r : p _ r d y ) ; to s 0 u n l e s s ( o n s t=p _ e r r ) ; w a i t [ 0 , 0 ] ; to s c h e d _ e r r o r end component m a i n i s port w : none in [ 2 0 , 2 0 ] , d : none in [ 0 , 0 ] , . . . p r i o r i t y c > d l > d , c ' > dl ' > d ' , . . . par p e r i o d i c [ d , c , dl , w ] | | p e r i o d i c [ d ' , c ' , dl ' , w ' ] | | . . . end property r e q 1 i s l t l ( ( m a i n /1/ e v e n t d l ) ⇒ ♦( m a i n /1/ e v e n t d ) )Listing 2: Example of Fiacre process (interpretation of AADL periodic threads)

Figure 3 :

 3 Figure 3: APP registration sequence diagram

Figure 4 :

 4 Figure 4: Graphical representation of the NPL component

  More specifically, in the case of the periodic thread, we also prove the following list of five requirements. More generally, in our framework, we provide a specific list of properties for every AADL component in the library (if it corresponds to a finite state verification problem).

	(P0b) scheduling error implies late completion:
	property P0b is ltl ( ( ( ( t/ event d ⇒
	( ( not t/ event dl ) until t/ event c ) ) ) )
	⇒	( not ( t/ state sched_error ) ) )
	(P1) completion is accepted immediately until scheduling error:
	property P1 is t/ event c leadsto ( ( t/ value ( st=p_rdy ) ) or
	t/ state sched_error ) within [ 0 , 0 ]
	(P2) dispatch is periodic until scheduling error:
	property P2 is ( t/ event dl leadsto ( t/ event dl or
	t/ state sched_error ) within [ 1 , 1 ] )
	(P3) deadline is periodic until scheduling error (the event t/start stands for the
	initial state of the thread). We need to prove property (P3) for every possible
	period T . Nonetheless, since T is the only timed parameter in this case, it is
	enough to consider only one non-null value, say T = 1.
	property P3 is ( t/ event dl or t/ start ) leadsto
	( t/ event dl or t/ state sched_error ) within [ 1 , 1 ]
	(P4) dispatch occurs immediately after deadline:

property P0a is ltl ( ( t/ event d and ( ( not t/ event c ) until t/ event dl ) ) ⇒ ♦ t/ state sched_error ) property P4 is t/ event dl leadsto t/ event d within [ 0 , 0 ]

table :

 :

		Task 1	Task 2 Task 3
	period	20 ms	20 ms	20 ms
	offset	0	3 ms	0
	deadline	20 ms	10 ms	20 ms
	priority	1 (high) 2	3 (low)
	BCET..WCET 1..3 ms	2 ms	10 ms


Abdelhak Skender

Amel Hadj-Ziane-Zafour

Emmanuel Flahaut
email: flahaut@chimie.ups-tlse.fr

Chemical functionalization of Xanthan gum for the dispersion of double-walled carbon nanotubes in water

Achieving stable suspensions of carbon nanotubes (CNTs) in water is still a challenge. Addition of surfactants is desirable as it allows keeping intact the intrinsic properties of the CNTs. However, for different applications, the potential toxicity of the surfactant is an important issue. Polysaccharides are among the best candidates and chemical modification can improve their intrinsic features. They can thus combine the properties of added synthetic counterparts with their intrinsic biocompatibility. In this work, we focused on the synthesis of hydrophobically modified Xanthan (Xan) with three derivatives (Diphenylmaleic anhydride, Phtalic anhydride, Epichlorhydrin-Phenol) to disperse CNTs. The dispersion and the stability against sedimentation of double walled carbon nanotubes (DWCNTs) have been investigated (rheological properties, zeta potential) as a function of pH and Xan concentration. Our results show that stable suspension of DWCNTs for 0.5% (w/w) could be obtained with the three derivatives of modified Xanthan gum in acidic and alkaline media while Xan itself is a very poor dispersing agent for CNTs, giving good evidence of the validity of our approach.

Introduction

Due to their exceptional physical and chemical properties, such as excellent mechanical strength, high electrical and thermal conductivities, high specific surface area, low density, and high aspect ratio [START_REF] Ajayan | Nanotubes from carbon[END_REF][START_REF] Peigney | Specific surface area of carbon nanotubes and bundles of carbon nanotubes[END_REF], CNTs have attracted considerable attention of researchers in various fields of research. Nevertheless, their insolubility in organic or aqueous media is a major bottleneck in the exploitation of these excellent properties because CNTs tend to agglomerate into bundles due to strong Van der Waals attractions forces. The poor solubility of CNTs turns dispersion into a challenge and several studies have already been published to achieve a uniform dispersion in aqueous or organic media. Both covalent [START_REF] Zhu | Improving the dispersion and integration of single-walled carbon nanotubes in epoxy composites through functionalization[END_REF][START_REF] Che | Epoxy composite fibers reinforced with aligned single-walled carbon nanotubes functionalized with generation 0-2 dendritic poly(amidoamine)[END_REF][START_REF] Chen | Solution properties of single-walled carbon nanotubes[END_REF][START_REF] Park | Preparation of transparent conductive multilayered films using active pentafluorophenyl ester modified multi-walled carbon nanotubes[END_REF] and noncovalent [START_REF] Chen | A versatile, molecular engineering approach to simultaneously enhanced, multifunctional carbon-nanotube-polymer composites[END_REF][START_REF] Zou | Dispersion of pristine carbon nanotubes using conjugated block copolymers[END_REF] functionalizations of CNTs have been reported. However, a major drawback of covalent functionalization such as oxidizing treatment by the use of appropriate acids at high temperature (nitric acid alone, or in combination with sulfuric acid) is the disruption of the extended p-conjugation in CNTs, resulting into structural defects on the nanotubes and leading to decreased (or at least modified) electrical and mechanical properties [START_REF] Dyke | Covalent functionalization of single-walled carbon nanotubes for materials applications[END_REF][START_REF] Liu | Comparison of covalently and noncovalently functionalized carbon nanotubes in epoxy[END_REF]. In contrast, the non-covalent approaches usually involve ultrasonication, centrifugation and filtration, focus on spurring non-disruptive interactions such as p-p stacking, adsorption, or Coulomb interactions through insertion of a chemical bridging agent [START_REF] Clark | Understanding surfactant aided aqueous dispersion of multi-walled carbon nanotubes[END_REF], with surfactants, carbohydrates, proteins, and nucleic acids [START_REF] Lin | Advances toward bioapplications of carbon nanotubes[END_REF][START_REF] Nakashima | Fundamentals and applications of soluble carbon nanotubes[END_REF]. Thus, these approaches achieved by physical adsorption are usually relatively weak, keeping the structure of the native tubes. Therefore, the delocalized p-electron network of the CNTs sidewall is preserved ensuring a minimal perturbation of their properties [START_REF] Vaisman | The role of surfactants in dispersion of carbon nanotubes[END_REF]. Most available experimental methods to disperse CNTs in common solvents or polymers require using surfactants [START_REF] Rastogi | Comparative study of carbon nanotube dispersion using surfactants[END_REF][START_REF] Yu | Controlling the dispersion of multi-wall carbon nanotubes in aqueous surfactant solution[END_REF]. Recent reports suggest the use of ionic surfactants with high HLB (Hydrophilic-Lyphophilic Balance) for dispersion and stabilization of CNTs in water. There is no preferred ionic one when organic solvents have to be used [START_REF] Vaisman | The role of surfactants in dispersion of carbon nanotubes[END_REF]. As a starting point in understanding CNTs dispersion in water and organic media, several parameters must be known, such as the nature of the surfactant, its concentration and type of interactions in the stabilized phase [START_REF] Vaisman | Dispersions of surfacemodified carbon nanotubes in water-soluble and waterinsoluble polymers[END_REF]. Previous works show no clear conclusion on the dispersive efficiency of either anionic or cationic surfactants [START_REF] Vaisman | Dispersions of surfacemodified carbon nanotubes in water-soluble and waterinsoluble polymers[END_REF][START_REF] Chatterjee | Single walled carbon nanotube dispersions in poly(ethylene oxide)[END_REF]. Therefore, knowing the surface charge of CNTs is absolutely required to understand the adsorption mechanism with ionic surfactants and to predict colloidal stability of CNTs suspensions. Zeta potential analysis seems a useful tool to achieve this task. Thus, Jiang et al. [START_REF] Jiang | Production of aqueous colloidal dispersions of carbon nanotubes[END_REF] have shown that the surface of multi-walled carbon nanotubes (MWCNTs) in aqueous media is negatively charged. However, to shed some understanding on the behavior of single-walled carbon nanotubes (SWCNTs), Ausman et al. [START_REF] Ausman | Organic solvent dispersions of single-walled carbon nanotubes: toward solutions of pristine nanotubes[END_REF] have shown that highly polar solvents such as dimethylformamide (DMF), methylpyrrolidine (MP) and hexamethylphosphoramide (HMPA) are rather efficient to properly wet SWCNTs. Islam et al. [START_REF] Islam | High weight fraction surfactant solubilization of single-wall carbon nanotubes in water[END_REF] have obtained a stable dispersion in aqueous media of SWCNTs using dodecyl(trimethyl)azanium bromide. Anionic surfactants such as sodium dodecyl sulfate (SDS) [START_REF] Jiang | Production of aqueous colloidal dispersions of carbon nanotubes[END_REF][START_REF] O'connell | Bandgap fluorescence from individual single-walled carbon nanotubes[END_REF][START_REF] Yurekli | Small-angle neutron scattering from surfactant-assisted aqueous dispersions of carbon nanotubes[END_REF][START_REF] Hertel | Spectroscopy of single-and double-wall carbon nanotubes in different environments[END_REF][START_REF] Poulin | Films and fibers of oriented single-wall nanotubes[END_REF][START_REF] Steinmetz | Production of pure nanotube fibers using a modified wetspinning method[END_REF][START_REF] Sano | Role of polymers in fabrication of carbon nanotube fibers using flow-induced condensation method[END_REF][START_REF] Vigolo | Macroscopic fibers and ribbons of oriented carbon nanotubes[END_REF][START_REF] Dyke | Overcoming the insolubility of carbon nanotubes through high degrees of sidewall functionalization[END_REF] and dodecyl-benzene sodium sulfonate (NaDDBS) [START_REF] Camponeschi | Uniform directional alignment of singlewalled carbon nanotubes in viscous polymer flow[END_REF][START_REF] Tan | Dispersion of single-walled carbon nanotubes of narrow diameter distribution[END_REF][START_REF] Rhoads | Dispersion of single-walled carbon nanotubes in aqueous solutions of the anionic surfactant[END_REF] have been widely used due to charge repulsion to limit the agglomeration tendency of CNTs [START_REF] Vaisman | Dispersions of surfacemodified carbon nanotubes in water-soluble and waterinsoluble polymers[END_REF]. Therefore, the former approach and the main driving force for surfactant-stabilized CNTs dispersions, the p-p stacking interaction [START_REF] Zhang | Photoluminescence and electronic interaction of anthracene derivatives adsorbed on sidewalls of single-walled carbon nanotubes[END_REF][START_REF] Fernando | Diminished band-gap transitions of single-walled carbon nanotubes in complexation with aromatic molecules[END_REF][START_REF] Hedderman | Solubilization of SWNTs with organic dye molecules[END_REF] between the benzene ring and the CNTs surface, is believed to significantly increase the binding of surfactant molecules onto CNTs [START_REF] Dong | Dispersion of carbon nanotubes by carbazole-tailed amphiphilic imidazolium ionic liquids in aqueous solutions[END_REF]. Thus, by this approach, various aromatic molecules have been used, such as polycyclic aromatic compounds carrying pyrene moieties [START_REF] Petrov | Noncovalent functionalization of multi-walled carbon nanotubes by pyrene containing polymers[END_REF][START_REF] Etika | Temperature controlled dispersion of carbon nanotubes in water with pyrene-functionalized poly(N-cyclopropylacrylamide)[END_REF][START_REF] Paloniemi | Water-soluble full-length single-wall carbon nanotube polyelectrolytes: preparation and characterization[END_REF][START_REF] Tomonari | Solubilization of single-walled carbon nanotubes by using polycyclic aromatic ammonium amphiphiles in water-strategy for the design of high-performance solubilizers[END_REF]. Furthermore, dispersed CNTs show great potential in the biomedical area, but the use of such aromatic surfactants in drug delivery applications is not recommended as they are toxic by inducing, for example, denaturation of proteins present in the blood [START_REF] Gudiksen | Differentiation of proteins based on characteristic patterns of association and denaturation in solutions of SDS[END_REF]. Hence, as an alternative to potentially lowering this effect, biopolymers such as gum arabic or gelatin have been used to promote a good dispersion of CNTs in this field of application [START_REF] Zheng | Gelatin-functionalized carbon nanotubes for the bioelectrochemistry of hemoglobin[END_REF][START_REF] Bandyopadhyaya | Stabilization of individual carbon nanotubes in aqueous solutions[END_REF]. Iamsamai et al. [START_REF] Iamsamai | The effect of the degree of deacetylation of chitosan on its dispersion of carbon nanotubes[END_REF] have used modified chitosan for the non-covalent surface modification of MWCNTs in aqueous media for drug delivery applications. Also, cellulose as an inexpensive, nontoxic, environmentally friendly and mass produced renewable material, has been used to form stable complexes with SWCNTs for pH varying between 6 and 10 [START_REF] Adsul | Combined strategy for the dispersion/dissolution of single-walled carbon nanotubes and cellulose in water[END_REF]. Whether for sensing or for any other intended application, bridging CNTs with biological systems should be essential in designing life sciences-related tools employing these nanomaterials. More recently in this context, as an alternative method for produc-ing MWCNTs dispersions, one type of non-covalent functionalization has received considerable attention involving biocompatible polymers (gum arabic and carboxymethylcelulose) to investigate their ecotoxicity on the amphibian larvae [START_REF] Bourdiol | Biocompatible polymer-assisted dispersion of multi-walled carbon nanotubes in water, application to the investigation of their ecotoxicity using Xenopus laevis amphibian larvae[END_REF]. Also, Roman et al. [START_REF] Roman | Amino acid adsorption on single-walled carbon nanotubes[END_REF] have demonstrated that amino acids can adsorb through non-covalent interactions with CNTs through favorable adsorption pathways. Biopolymers, such as polysaccharides with a good toxicological profile, bring both steric repulsion and better stabilization (as thickeners) of the aqueous phase behavior of these colloids. Besides being renewable, the unique structure of polysaccharides offers many interesting properties like hydrophilicity, biocompatibility, biodegradability (at least in the original state), stereoregularity, multichirality, and polyfunctionality, i.e. reactive functional groups (mainly OH-, NH-, and COOHmoieties) that can be modified by various chemical reactions [START_REF] Heinze | Esterification of polysaccharides[END_REF]. Therefore, in the general context to achieve the stabilization of double-walled carbon nanotubes (DWCNTs) dispersion in aqueous media, we focused on the synthesis of hydrophobically modified polysaccharide. We first propose the hypothesis that the benzene ring can interact strongly with CNTs yielding a homogeneous dispersion. Thus, among water-soluble biopolymers, Xanthan gum (Xan), a microbial biopolymer produced by the Xanthomonas campestris with a high molecular weight (Fig. 1) [START_REF] Jansson | Structure of the extracellular polysaccharide from Xanthomonas campestris[END_REF][START_REF] Melton | Covalent structure of the extracellular polysaccharide from Xanthomonas campestris: evidence from partial hydrolysis studies[END_REF] seems a promising candidate.

The main goal of this paper is thus to synthesize new Xan derivatives, based on the grafting of hydrophobic moieties (benzene ring) along the polysaccharidic chain and to investigate how such derivatives of Xan should prevent the agglomeration of DWCNTs in water through steric stabilization via hydrophobic interactions, and thus result in improved dispersibility of suspensions. In the present letter, we report on the synthesis of three derivatives of Xan (Diphenylmaleic anhydride, Phtalic anhydride, Epichlorhydrin-Phenol) (XDPMA, XPA, XEPH) and we compare their efficiency to disperse and stabilise DWCNTs in water using Zeta potential and viscosity measurements of the supernatant of centrifuged dispersions versus pH. Other parameters such as the number of walls and the length of CNTs of course also play an important role in terms of stability of the suspensions, as they respectively increase the density of the CNTs or the chances of contacts between the nanotubes, and thus potentially lead to more Fig. 1 -Chemical structure of Xanthan [START_REF] Jansson | Structure of the extracellular polysaccharide from Xanthomonas campestris[END_REF][START_REF] Melton | Covalent structure of the extracellular polysaccharide from Xanthomonas campestris: evidence from partial hydrolysis studies[END_REF]. sedimentation and agglomeration. However, our approach is based here on the surface modification of the CNTs in order to enhance the interaction between the CNTs and the dispersing agent, and in this case, only the outer wall is concerned. With this hypothesis, the conclusions of this study should be very general and could be transposed to any kind of pristine carbon nanotube (excluding oxidized carbon nanotubes and other surface functionalization). The originality of this work is also to open a path for a family of new macromolecules to enhance the dispersion of CNTs in aqueous media, which could be very useful for the investigation of their toxicity in biological systems.

Experimental

Chemicals and DWCNTs synthesis

DWCNTs (ca. 80%) were synthesized by catalytic chemical vapour deposition (CCVD) with an outer diameter ranging between 1.2 and 3.2 nm; they are individual or gathered in small-diameter bundles (10-30 nm) which can be up to ca. 100 lm in length [START_REF] Flahaut | Gram-scale CCVD synthesis of double-walled carbon nanotubes[END_REF]. Xanthan gum fine powder, cream colored (Rhodia, Standard 50-mesh), zinc-tetrafluoroborate hydrate crystallized salt; 2,3diphenylmaleic anhydride (DPMA), phthalic anhydride (PA); N,N-dimethylformamide (DMF), acetone (ACT), ethanol (EA), epichlorhydrin and phenol were purchased from Sigma-Aldrich and were used as received.

Synthesis of XDPMA, XPA and XEPH

The most probable pathway of reactions of Xan derivatives, are either in heterogeneous (Fig. 2(a andb)) or homogeneous medium (Fig. 2(c)). Two working methods have been applied as described elsewhere by Hamcerencu et al. [START_REF] Hamcerencu | New unsaturated derivatives of Xanthan gum: synthesis and characterization[END_REF], Rogovin et al. [START_REF] Rogovin | Study of the synthesis of dextran derivatives[END_REF] and Fournier et al. [START_REF] Fournier | Coating polystyrene particles by adsorption of hydrophobically modified dextran[END_REF]. Moreover, leading to a stepwise increase in the hydrophobicity of Xan derivatives might be not as easy, mainly due to the insolubility of Xan in a suitable medium and the conformational structure at supermolecular level [START_REF] Hamcerencu | New unsaturated derivatives of Xanthan gum: synthesis and characterization[END_REF]. Thus, the synthesis strategy we proposed, based on the grafting of hydrophobic groups (benzene ring) along the polysaccharidic chain (hydroxyl groups), relies on the use of excess reactants to enhance the reactions. Therefore, a possible approach is to use 11 mol of each reactant per mole of Xan (11 hydroxyl groups per Xan macromolecule (Fig. 1)). The main procedures reported for the synthesis conditions of Xan derivatives are summarized on Fig. 2.

Dispersion procedure of DWCNTs in water

DWCNTs suspensions in water were prepared as follows. First, three stock solutions of the required amount of the three derivatives of Xan (0.5%, w/w) were prepared in deionized water by dissolving the required amount under magnetic stirring for 48 h (25 °C) to ensure the total hydration of the biopolymers. Second, appropriate masses of DWCNTs (initial amount of 0.02% (w/w)) were added to the vials (25 ml) with XPA, XDPMA and XEPH at 0.5% (w/w). To further evaluate the nanotubes'dispersion, the mixtures were then bath sonicated (Bioblock T570, 35 KHz, 160 W) for 30 min, after which the resulting mixtures were also ultrasonicated with an ultrasonic probe (Model Vibra cell 75042, 20 kHz, 500 W) for 15 min at 25% amplitude with a pulse of 5s on, 5s off to prepare homogeneous dispersions. Afterwards, each prepared suspension was centrifuged at 16,000 rpm for 30 min in order to separate the sediment from the supernatant. Finally, the as-prepared suspensions were left to stand for 10 h and the resulting supernatants were collected. The successful chemical modification of Xan by the aromatic moieties was confirmed by 1 H NMR spectra (Fig. 3(b-d)) compared with the spectrum of Xan (Fig. 3a); the spectra show signals for characteristic peaks of aromatic moiety protons present at d between 7.0 and 8.6 ppm for the three derivatives of Xan (Fig. 3: (b) XDPMA, (c) XEPH (d) XPA). Moreover, the weakly developed peaks are likely to be due to the low efficiency of the reactions. Indeed, the polysaccharidic chain of Xan, presents a conformational transition in Fig. 2 -Procedures for the modification of Xanthan: (a) and (b) heterogeneous media [START_REF] Hamcerencu | New unsaturated derivatives of Xanthan gum: synthesis and characterization[END_REF]; (c) homogenous media [START_REF] Rogovin | Study of the synthesis of dextran derivatives[END_REF][START_REF] Fournier | Coating polystyrene particles by adsorption of hydrophobically modified dextran[END_REF]. solution [START_REF] Milas | Conformational investigation on the bacterial polysaccharide xanthan[END_REF][START_REF] Milas | Properties of xanthan gum in aqueous solutions: role of the conformational transition[END_REF]. Therefore, the access of aromatic moieties to hydroxyl groups maybe to a rather low extent [START_REF] Hamcerencu | New unsaturated derivatives of Xanthan gum: synthesis and characterization[END_REF], yielding to a low degree of substitution.

1 H NMR Characterization

Zeta potential measurements

Zeta potential (n) measurements were carried out with zetasizer (Model ZEN 3691, Malvern Instruments). All the measurements were performed in optically clear suspensions, so it was necessary to make these measurements with samples having a much lower concentration of dispersing agent (Xan derivative) than these used in the rheological studies. The effective charge of colloidal particles is typically affected by some physicochemical parameters, among them the ionic strength and pH. Therefore, the n-potential of samples having 0.1% (w/w) of the three derivatives of Xan as a function of pH in both acidic and basic medium were determined by automatically adding the required amount of HCl and NaOH. It should be noted that the values were measured from pH around 1.5 to 10 in order to obtain a better approximation and auxiliary information on the size distribution of dispersed DWCNTs.

Viscosity measurements

The shear rate dependent viscosity measurements were staged with a controlled strain rheometer (Physica Anton Paar, Germany), operating in concentric cylinder geometry and connected to a water bath in order to ensure a constant temperature of 25 °C. At this temperature the system was left to equilibrate for 30 min. The apparent viscosity was determined by measuring the viscosity at each shear rate, and all the experiments were done using samples from the resulting supernatants (Section 2.3) at neutral pH.

Results and discussion

Three derivatives of hydrophobically modified Xan, XPA, XPDMA and XEPH were used at 0.5% (w/w) to disperse DWCNTs in water. As shown on Fig. 4, the n-potential of the dilute suspensions of DWCNTs versus pH for the three derivatives was extremely pH dependent and decreased significantly (absolute value) for pH < 5, reaching values ranging from À30 to À40 mV for pH above 5. These results can be attributed to strong adsorption ability of the hydrophobic tails of the Xan derivatives (benzene moiety) on the surface of DWCNTs. This is in agreement with Liu et al. [START_REF] Liu | Dispersion of multi-walled carbon nanotubes by ionic liquid-type gemini imidazolium surfactants in aqueous solution[END_REF], who reported that for CNTs dispersion in aqueous media, the relatively high value of n-potential make them stabilize due to Coulomb forces. Moreover, particles with zeta-potentials smaller than À15 mV or larger than 15 mV are deemed to be stabilized by electrostatic repulsion interactions [START_REF] Hiemez | Principles of colloid and surface chemistry[END_REF]. As shown in Fig. 4, for the XEPH/DWCNTs, it is clear that increasing pH from acidic to basic media, the n-potential reached $ À30 mV. The difference of the dispersion efficiency is shown on Fig 5A (a), the solution of XEPH (0.5%)/DWCNTs for pH around 1.6 appears more clear with DWCNTs agglomerated for n-potential near À5 mV. Important information is obtained from this result, in particular the chemical structure of the aromatic moiety of the XEPH because this finding is in agreement with previous study by Clark et al. [START_REF] Clark | Understanding surfactant aided aqueous dispersion of multi-walled carbon nanotubes[END_REF] who have demonstrated that the dispersion of CNTs in water is pH dependent due the chemical structure of the dispersing agent. Hydroxyl groups become ionized only under basic conditions while carboxylic acid groups are protonated at low pH. Hence carboxyl and hydroxyl groups bound to the aromatic moiety in the case of XPDMA and XPA which will allow for both protonated and ionized states to exist over the pH range from acidic to alkaline media, while hydroxyl groups presents in XEPH become ionized only under basic conditions. Thus, it is important to point out that the enhanced dispersions observed are pH dependent. Therefore, extending the pH from acidic to alkaline conditions, more oxygenated groups become ionized resulting in a more negatively charged surface.

In view of our results, the non-covalent functionalization of DWCNTs in aqueous media were found to have n-potential ranging from À30 to À40 mV which confirms the successful immobilization of Xan derivatives on DWCNTs by adsorption of the benzene moiety of the modified biopolymer on the surface of DWCNTs which have a superior ability of dispersing than native Xanthan (Fig. 5C), via p-p stacking interactions between the benzene ring and the CNTs with pH values above 5 as shown on Fig. 5B. Fig. 6 illustrates the good agreements between the size distribution particles by numbers, and the surface charge density of colloidal particles dispersed by the three derivatives of Xan, leading to complex colloids with DWCNTs in aqueous media (pH $ 7), with size distributions by number ranging from 10 to 1000 nm.

Results suggest that a higher surface charge density provides a better stability of the suspensions. However, plotting the viscosity as a function of shear rate revealed that the presence of the benzene ring in the back bone of the modified xanthan increased the hydrophobic interactions, therefore, leading to a drop of the viscosity of the solutions at low shear rate, as shown on Fig. 7. Consequently, the observed changes in viscosity of the native Xan and their derivatives (more pronounced in the case of XEPH) could be due to conformational changes of the macromolecules and the cross-linking, herein, the most significant change of the viscosity seems to be due to the hydrophobic moiety (benzene ring) (Fig. 7). In addition, from a comparison with the modified xanthan solutions viscosity of the samples supernatants (Section 2.3) as a function of shear rate, it seems that the presence of DWCNTs particles reduces the viscosity of the system as shown on Fig. 8; hence, the presence of DWCNTs is associated to more pronounced shear thinning behavior. Overall, it is also obvious from the viscosity measurements, especially at low shear rate, at 0.5%, that all the Xan derivatives/DWCNTs dispersions showed a strongly lower viscosity than samples of the three derivatives alone (Fig. 8(a-c)). Moreover, XEPH/DWCNTs showed lower viscosity than XPA/DWCNTs and XDPMA/ DWCNTs which presented relatively similar profiles (Fig. 8d). However, according to n-potential measurements (Fig. 4), samples of XPA and XDPMA showed n-potential smaller than XEPH for pH above 5. Meanwhile, the hydrophobic interactions between the DWCNTs and the aromatic moiety through p-p stacking are more pronounced in the case of XPA and XDPMA compared to XEPH, thus resulting in better disper- sions, as confirmed by the previous results by Liu et al. [START_REF] Liu | Dispersion of multi-walled carbon nanotubes by ionic liquid-type gemini imidazolium surfactants in aqueous solution[END_REF]. Finally, this effect can be interpreted in terms of the discrepancies in their chemical structures. Henceforth comparing the viscosity of samples, in all cases the solutions were shear thinning at all shear rates and the viscosity of DWCNTs-free samples is relatively higher. Consequently, DWCNTs are responsible for this effect, by acting as inter-molecular interactions (hydrophobic interactions) yielding therefore, conformational change of the macromolecules (Xan derivatives) of the continuous-phase. In order to disperse CNTs in water, hydrophobic tail groups orient themselves face toward the nanotubes surface while hydrophilic head groups extend into the water [START_REF] Vaisman | The role of surfactants in dispersion of carbon nanotubes[END_REF][START_REF] Rastogi | Comparative study of carbon nanotube dispersion using surfactants[END_REF][START_REF] Wang | Dispersing carbon nanotubes using surfactants[END_REF]. Hence, better charge repulsion between the hydrophilic groups of Xan derivatives prevents their agglomeration, and therefore a drop of viscosity is observed at low shear rate.

Conclusion

In summary, DWCNTs have been successfully dispersed in aqueous media via non-covalent modification with new hydrophobically modified derivatives of Xanthan gum containing aromatic moieties. Our results show strong interactions between the modified derivatives and DWCNTs in water. The intensity of interactions depends especially on the chemical structure of the hydrophobic head. However, resulting suspensions of DWCNTs have quite a high stability against agglomeration resulting from the high hydrophobic interaction between the benzene ring and the tubes through p-p stacking. Moreover, XPA and XDPMA confirm the successful immobilization of DWCNTs for very acidic media compared to XEPH. It was found that, above pH 5, the three derivatives allow obtaining stable suspensions. Thus, these results indicate that the introduction of an aromatic moiety into the backbone of Xanthan enhances the dispersibility of CNTs in water via p-p stacking interaction; hence this noncovalent method may be beneficial to contribute for many CNTs applications. Moreover, these results also open interesting perspectives for the toxicity assessment of dispersed CNTs and we are currently investigating the use of our modified biopolymers in this context.

1 H

 1 NMR spectrum of the derivatives of Xanthan was recorded on Bruker advance (400 MHz) instrument equipped with a 5 mm probe type TBO, using D 2 O solutions having a biopolymer concentration around 3 g L À1 . The Strategies of the experiments are explained in detail elsewhere[START_REF] Hamcerencu | New unsaturated derivatives of Xanthan gum: synthesis and characterization[END_REF][START_REF] Callet | Influence de la structure, de la conformation et des traitements post fermentation sur les proprie ´te ´s du xanthane en solution[END_REF][START_REF] Morris | Orderdisorder transition for a bacterial polysaccharide in solution. A role for polysaccharide conformation in recognition between Xanthomonas pathogen and its plant host[END_REF].

Fig. 4 -

 4 Fig. 4 -Plot of the n-potential as a function of pH of the dispersions samples.

Fig. 3 - 1 H

 31 Fig. 3 -1 H NMR spectra in D 2 O of Xan (a), XDPMA (b), XEPH (c) and XPA (d).

Fig. 5 -Fig. 6 -

 56 Fig. 5 -Typical images of the dispersion efficiency of DWCNTs with XEPH; XPA; XDPMA; at 0.5%; (A): pH 1.6; (B): pH > 5, and (C) native Xan.

Fig. 7 -Fig. 8 -

 78 Fig. 7 -Plots of viscosity versus shear rate at 0.5% of Xan; XPA; XPDMA; XEPH at 25 °C, pH 7.

Acknowledgments

The authors gratefully acknowledge the Ministry of High Education and Scientific Research (Algeria) and the French Ministry of Foreign and European Affairs for financial support of PHC-TASSILI 10MDU797 project.

R E F E R E N C E S