Stéphane Chatty

Mathieu Magnaudet

Daniel Prun

Stéphane Conversy

Stéphanie Rey

Mathieu Poirier

Designing, developing and verifying interactive components iteratively with djnn

Keywords: ACM Classification Keywords: H5.2 Information Interfaces and presentation: User Interfaces, D2.2 Software Engineering: Design Tools and Techniques, D3.3 Programming Languages: Language Constructs and Features interactive software, design process, development process, interactive component, software verification

Introducing iterative user interface design methods into the development processes of safety-critical software creates technical and methodological challenges. This article describes a new programming paradigm aimed at addressing some of these challenges: interaction-oriented programming. In this paradigm any piece of software consists of a hierarchical collection of components that can interact among themselves and with their environment, and its execution consists in propagating activation through interactions between components. We first describe the principles of interactionoriented programming, and illustrate them by describing the basic components provided by the djnn programming framework to create interactive software. We then show how interactive programming provides a basis for formulating and checking properties that capture requirements on interactive components. The rest of the article is dedicated to example design and development scenarios that illustrate how development environments could leverage interactive programming in the future so as to jointly address the requirements of modern user interface design and safety-critical software development.

INTRODUCTION

There are well established methods for developing safety critical software, such as those prescribed in the DO178 standards. In some domains, solutions have been developed to apply these methods to user interfaces as well. For instance, in aeronautics the ARINC 661 standard defines a collection of well known interactive components (or widgets), such as lists and menus. The protocol of these components is defined in such a way that they can be developed and certified individually, then reused at will. Industrial tools have even been introduced to assemble them graphically, then generate the corresponding code.

However, with ongoing plans to introduce more modern user interfaces in these safety critical settings, new questions appear. Not only are the envisaged interactive components often more complex and more difficult to specify than their predecessors, there is also a trend toward interface customization. Each aircraft or car manufacturer wants to have its own distinctive signature, in terms of interaction and not only graphical appearance. Consequently, they expect equipment providers to deliver products whose behavior and appearance can be modified. This means that one cannot rely solely on industry standards that define interactive components, and that methods must be proposed for designing and developing custom components, usually as a collaboration between an equipement provider and an integrator.

The user interface industry has developed and validated methods for designing custom interactive software, and recent R&T projects have shown that they can be applied successfully by the aeronautics industry. However these methods involve various actors, including human factors experts and designers, and are iterative by nature. Integrating them in industrial development processes brings new challenges, and appropriate tool chains are not yet available to support this. In addition, the state of the art in interactive software development has not yet reached the same level of maturity as other branches of computer science. Interactive software is still complex and costly to produce [START_REF] Myers | Separating application code from toolkits: Eliminating the spaghetti of callbacks[END_REF][START_REF] Myers | Survey on user interface programming[END_REF], and model driven engineering methods are not yet widely used. This does not provide a favorable context for developing and validating custom components on a repeated basis. In particular, validating interactive software that contains code written in a traditional programming language is very costly.

In this article, we propose a theoretical and practical contribution towards the resolution of these two issues: the convergence of user interface design methods and critical software development processes, and the validation of custom interactive software. This contribution consists of a software execution model and a software architecture, whose combination provides the basis of what we call interaction-oriented programming. This allows to organize interactive software as a collection of components whose execution can be analyzed and whose definition can be incrementally refined. The proposed execution model and component architecture are implemented in a development framework named djnn, that has been used successfully in various projects.

We first analyze reasons why it is important to account for interactive software design methods. Doing so, we outline requirements for future design processes and tools that would combine the needs of interactive and safety critical systems. We then stress the key role of software architecture and execution models in fulfilling these requirements. After reviewing the state of the art on these topics, we introduce a theoretical framework for interactive components that defines a software architecture and an execution model. We then describe the djnn framework and use a simple aeronautical component (a primary flight display) and a series of idealized development scenarios to illustrate how new processes and tools for designing interactive software can be derived from this work.

ANALYSIS: WHY IS INTERACTIVE SOFTWARE SPECIAL?

Managing hidden requirements

One of the keys to successfully developing complex systems is the management of requirements. Gathering requirements, analyzing them, and tracing them in products represent an important part of the development effort. Various development methods and tools have been proposed for this purpose, and for supporting certification processes. Unfortunately, user interfaces suffer from a fatal flaw with this regard: requirements are impossible to gather in advance. There are hidden requirements that keep appearing during design and development processes, or even during the use of the final systems. As an example, consider an equipment in which two critical information fields are shown side by side. The two graphical representations may work perfectly when tested independently, and when using them together visual interferences or perceived inconsistencies between them can lead users to errors in reading them. It can also be discovered later that one of these representations does not work well when users are in particular mental conditions that had not been anticipated. Some of these emerging requirements, when not caught early enough, can be palliated by operational procedures or user training. Others can lead to safety flaws, or to outright rejection of the system by its intended users.

A day might come when cognitive sciences provide us with enough knowledge that requirements can actually be gathered in advance, but this is at best a long time goal. Until then, the best known solution for securing requirements is iterative design, a flavor of agile methods developed specifically for interactive software. Users are presented prototypes created by designers and usability experts, new requirements emerge from the confrontation, and new prototypes can be designed. During this process, two collections are incrementally created: a collection of design elements, and a collection of requirements. It is only after a number of iterations that the two collections can be considered sufficient. This iterative process is not intrinsically incompatible with the processes used in safety-critical developments. Nevertheless, not only does it require dedicated tools for the initial phases of design, it also interferes with further development phases. In theory, user interface design could be done prior to actual software development, so that the two processes are independent. In practice however, design generally continues in parallel with development, if only because hidden requirements keep showing up. This means that solutions must be proposed to manage how the two processes interact with each other.

Architecture of interactive software

The above provides a first set of requirements for tools dedicated to user interface design in critical systems: an architecture that allows the incremental refinement of design elements and their execution, as well as the incremental definition of requirements and their checking. The desire to create customizable user interfaces highlights additional requirements: the ability to separately define the behaviors of given components, and check that the resulting user interfaces still meets the requirements.

Interoperability and interchangeability of software components is actually a universal concern, and it is the essence of software architecture. There are various situations in which programmers need to change how components are combined in their software. This includes early design phases, in which prototypes are developed. And this also includes various refactoring phases, whether during initial development or when the software is reused to create new products. Each programming paradigm provides support for the interoperability of a certain type of components, and therefore for software architecture. For instance, functional programming makes it easier to refactor software that performs computations. Similarly process algebra makes it easier to refactor software that reacts to input. However, interactive software brings its own class of refactoring. There are many different ways to design a user interface for a given task. Take for instance the single pressing of a button to activate a function. The button can just change state visually, for instance by changing color. This atomic change can be expressed through an assignment, either of the color itself or of a symbolic state of the button. Alternatively, the button can change with an animation. This would require the state assignment to be replaced with a process that repeatedly modifies the visual state, and that can continues in parallel with further interactions. These two options are profoundly different in existing programming paradigms, and this makes refactoring costly. To compound matters further, user interfaces can make use of various interaction modalities such as graphics, sound, touch input, speech input, eye tracking, etc. Not only is each modality different from the others, they can also be combined in ways that require to manage interaction state, time intervals, and other complex execution patterns.

Various architecture patterns have been proposed to support the interoperability of components in interactive software. As exemplified above, some situations are easily expressed by simple constructs in existing programming languages, such as function calls, assignments or loops. Others require specific solutions such as events, data-flows, state machines. This diversity of control structures and component interconnection mechanisms, if not derived from a reduced set of primitives, hampers interoperability. It also limits the formulation of an execution semantics for programs, and therefore the ability to formulate and check properties on software components.

Another consequence is in the complexity for programmers. Each individual solution alleviates one source of complexity, for instance state machines make it easy to manage state dependencies. But as soon as several solutions are mixed, new sources of complexity appear. For instance, languages such are QML must be combined with traditional languages such as C++ to produce full applications, thus reintroducing in programs the traditional architecture patterns and control structures. Similarly, combining state machines with dataflows can rarely be performed without writing additional code in a traditional programming language. Programmers therefore end up manipulating independent concepts that each describe part of the program execution, and that do not have a clear common base.

Therefore, defining a minimal set of primitives from which the behavior of interactive software can be derived is required both for raising interactive software to the same level of manageability as other types of software, and for supporting development processes that rely on software refactoring.

STATE OF THE ART

Complexity

Various methods have been proposed over the last decades to make interactive software development less complex. The initial approach, mostly in the 1980s and 1990s, consisted in creating User Interface Management Systems and user interface toolkits on top of traditional programming languages. This approach evolved into two areas of research. On the one hand were collections of reusable interactive components such as dialogue boxes and buttons, that evolved into specialized languages and standards such as XAML, XUL, QML and ARINC 661.

On the other hand were software patterns aimed at managing the architecture requirements of interactive software, that differ significantly from those of computation-oriented software. Some of these patterns were aimed at separating the interactive code from the computation-oriented and data-oriented code. This includes the Seeheim and ARCH architecture, and the MVC, PAC and MVVM patterns. Other patterns were aimed at providing better support for the execution and control patterns encountered in interactive software. This starts with callback functions and the Inversion of Control pattern that account for the prevalence of external control in interactive software. But this also includes more complex patterns to support state management (state machines, hierarchical state machines, Statecharts) and dataflow (one-way constraints, functional reactive programming [START_REF] Elliott | Functional reactive animation[END_REF], dataflow bricks [START_REF] Chatty | Extending a graphical toolkit for two-handed interaction[END_REF]). However, as mentioned previously, these solutions provide only local complexity relief: they make some parts of the behavior easier to formulate, but the overall complexity remains high because of how heterogeneous constructs are combined.

Development process

Historically, two approaches have been taken to develop graphical user interfaces. The first consists in giving a functional specification to programmers, and rely on their graphical skills. The second, used when visual quality is desirable, consists in asking graphical designers to produce visu-als then asking programmers to reproduce them in their programs. Having programmers recode the graphics like this is both a waste of time and a cause of errors.

In contrast with this, traditional programmers can split their tasks and work in parallel, relying on well supported integration techniques such as separate compilation and linking. Interactive software developers could take advantage of similar solutions. First, they could to split their tasks and work in parallel with graphical designers. Then, they could also split tasks during iterative design phases with users and human factors specialists. Solutions have been proposed for this, leveraging on the similarities between the visual and logical structure of a user interface and the abstract syntax tree in traditional programming [START_REF] Chatty | Supporting multidisciplinary software composition for interactive applications[END_REF]. Considering graphics and interactive behaviors as nodes of a tree allows to produce them independently, then build the tree during a loading phase at compilation or execution time, and execute the resulting tree. This has been shown to yield significant improvements both in terms of effort and development time span[?]. However, this is only feasible for those parts of the software that can be consistently modeled as nodes in the execution tree. To be fully operational, this approach requires that 1OO% of programs can be modeled in the same framework.

Another approach consists in applying model-driven engineering methods to interactive software. In this approach, domain experts produce an abstract model of the task to be carried out by users, then all or part of the software is derived from this abstract model. However this only work for some classes of user activities, and the resulting user interfaces are stereotyped and of limited usability. More practical variants of this approach have also been tested, where the user interface is expressed using a theoretical model, but it is produced through a design process rather than generated from a task model. This allows to take advantage of the benefits of model-driven architectures without losing the interface quality brought by the design process. For instance in the Pet-Shop system, applications are created by combining Object Petri Net models with Java code [START_REF] Palanque | A model-based approach for supporting engineering usability evaluation of interaction techniques[END_REF]. However, like above this approach will reach its full potential only when 100% of the user interface can be expressed in the model.

Code verification

During the last decades, various methods dedicated to the verification of interactive system properties have been proposed. The widely used approach relies on the test of the final system (or a prototype of it) where end-users accomplish selected tasks in a dedicated environment. Observations and measurements performed during the execution are used to assess whether the system fulfills the expected properties or not. The main drawback of this approach lies in its lack of exhaustivity because properties cannot be checked against all possible executions of the system. Moreover, this approach can only be used after the development (the system must be available) which constitutes another negative point: bugs are way more expensive to locate and correct at this development stage.

Model-based methods have been proposed to minimize these issues: at design time, a model of the future system is built and properties are verified by studies performed on the model rather than on the final system itself. The underlying logic behind this approach is that if a property holds on the model, and if the final system is built according to the model, then the property holds on the final system. Model checking aims at verifying properties on the state-transition structure built during the simulation of the model [START_REF] Palanque | A model-based approach for supporting engineering usability evaluation of interaction techniques[END_REF]. This is very similar to methods used for safety-critical software (eg. Esterel: [START_REF] Berry | ESTEREL: A formal method applied to avionic software development[END_REF], Scade: [START_REF]Scade display HMI software design[END_REF]). Alternatively, proof-based methods consist in mathematically proving the preservation of properties (invariants, pre-conditions and / or post-conditions) during successive refinements of the model (VDM: [START_REF] Duke | Abstract Interaction Objects[END_REF], Z: [START_REF] Hussey | Specifying a Web Browser Interface Using Object-Z[END_REF] or B: [START_REF] Aït Ameur | Encoding a process algebra using the Event B method[END_REF]).

Although they have been shown to be very effective, such model-checking approaches suffer from their impossibility to encompass systems with infinite number of states or transitions which is a major limitation in the context of interactive systems. Moreover, the assumption that "the final system is built according to the model" is hard to reach for reasons explained previously: no available model describes 100% of a user interface. To palliate this, some authors introduce a simplified model called the abstract user interface, in which the totality of a user interface can be described. Properties can be checked on this model. However, the process of converting this into a concrete user interface by adding code to the abstract user interface limits the benefits that can be obtained from the model based approach.

Abstract interpretation ( [START_REF] Cousot | Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints[END_REF]) is a verification method based on static analysis of the software code. An abstract semantic is extracted from the code and can be used to verify properties and perform optimisations 1 . This approach has historically been used for the verification of various properties of programs. For instance, the static analyzer Astrée is able to prove the absence of some types of run time errors on C programs ( [START_REF] Blanchet | Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software[END_REF]), and has been used in safety-critical projects. For interactive properties, [START_REF] Charlier | Abstract interpretation and application to interactive system verification[END_REF] first proposed this approach with the objective of providing a unification canvas for verification techniques. [START_REF] González-Calleros | Advanced human-machine interface automatic evaluation[END_REF] described the verification of interactive Web pages through the static analysis of the user interface with ergonomic rules, encoded in UsiXML. [START_REF] Thimbleby | Applying graph theory to interaction design[END_REF] proposed to build and exploit a graph-oriented semantics of an interactive device to support the verification of properties. In this work, an existing device was analyzed and modeled with a graph whose arcs represent user actions and nodes observable states. It was then possible to compute some interactive properties on the graph that can be interpreted at the device level.

Abstract interpretation is an efficient application of the model checking approach: work is performed directly at the lowest level, that is the code of a concrete user interface, and therefore avoids the limitations of using an abstract model. Paradoxically, its main drawback for interactive systems lies in the impossibility to access to higher levels of description of the interface, such as those contained in the abstract user interface, because they usually have disappeared during implementation and compilation. It becomes impossible to check properties that would be expressed at these higher levels, such as "is this rectangle red when this button is pressed?". When the software is built with languages that do not capture the appropriate level of information (e.g. C ot Java), the missing information must be introduced by producing a model by hand.

Analysis and positioning

Most limitations of the state of the art derive from the same cause: the limited power of expression of the patterns, languages and models available. Each of the available solutions for expressing parts of interactive software have focused on a given requirement that was not fulfilled by traditional programming languages: supporting external control, or providing reusable dialogue boxes, or managing state, etc. Each alleviates one source of complexity in interactive software, but none provides a complete solution like modern programming languages do for computation-oriented software. This has consequences on software complexity, on development processes, and on the ability to verify code properties.

In this article, we describe an alternative solution that overcomes these limitations using an approach similar to Lustre or Esterel [START_REF] Halbwachs | The synchronous dataflow programming language Lustre[END_REF][START_REF] Berry | ESTEREL: A formal method applied to avionic software development[END_REF]: adopting an execution model dedicated to the category of software that is being developed, and using it to develop the totality of the concerned software. Like Lustre and Esterel, the proposed model represents concurrency with the concept of process; it can be seen as a third point of view on interactive systems, more adapted to the need of user interfaces and making interaction its core concept. In contrast with them, its design integrates software engineering concerns and particularly the need of strong conceptual unification so as to support flexible development processes. Moreover, our work extends the approach followed by SCADE Display concerning the verification capabilities of interactive applications: when SCADE adresses low-level related properties (related to the concrete user interface: graphics, code design) our approach also encompasses upstream user interface design phases.

THE DJNN FRAMEWORK

djnn (available at http://djnn.net) is a programming framework that relies on a model of interactive software in which any program can be described as a tree of interactive components [START_REF] Chatty | Supporting multidisciplinary software composition for interactive applications[END_REF]. Basic components such as variables, control structures, and graphical objects are assembled to produce bigger components, themselves assembled until producing the desired application.

The execution of a program is described by the interactions between its components, and between them and the external environment: components react to events detected in their environment, and may themselves trigger events. For instance, a simple "fire alarm" program can be described with three components. The first is activated when the temperature is higher than a threshold, the second produces a sound when activated and the third binds the two others by propagating the activation of the first one to the second one. Such a component model applies to input and output devices. This allows djnn to provide support for a wide range of devices, thus fostering the exploration of wide design spaces. But djnn has also the expressive potential of a general programming language. This contrasts with most user interface programming frameworks, which provide reusable components and architecture patterns that programmers combine with code written in a traditional programming language. Not only does djnn aim at covering 100% of the user interface code, it also has the potential of describing the functional core as well, thus covering whole interactive applications.

Theoretical foundation: interactive processes

Like functional programming languages, the conceptual model of djnn relies on a very reduced set of basic concepts from which all other language concepts and programmerdefined concepts are derived. In functional languages the basic concepts are functions, arguments and function calls, all rooted in the theoretical concept of lambda term from lambda calculus. In djnn the basic concepts are components, names and activation, all rooted in the theoretical concept of process from process algebras [START_REF] Baeten | A brief history of process algebra[END_REF].

While computations can be described as the evaluation of lambda expressions, interactions can be described as the activation of interconnected processes: activation signals, called events, propagate from one process to another according to how they are coupled, thus producing the reactive behavior of the system. This concept of interaction differs from that of communication used in most process algebras, but it is nevertheless possible to express formal models of component activation in existing process calculi.

Process-based theories are general enough to model both interaction-oriented software and computation-oriented software [START_REF] Goldin | Interactive computation -the new paradigm[END_REF]. But they can also model hardware devices, and more generally the environment in which software applications run. This allows to model both the software and its direct environment using processes, so that no special provision has to be made for those part of the software that interact with the environment and the user. Whole interactive applications can therefore be described in the same language.

Core interactive components

Components are man-made embodiment of processes: engineers build systems by assembling components, and the theoretical model of the resulting systems can be deduced from those of the individual components and how they are assembled. Programmers create interactive programs by instantiating and assembling software components, and connecting them to hardware components. The djnn environment provides them with basic software components to this effect:

• input components represent input devices, sensors, or elements of the execution context. Their activation is coupled to external events. For instance, a mouse is an input component made of smaller input components such as a buttons and a position tracker. The position tracker itself has two smaller input components named X and Y.

• output components represent output devices or abstractions used to manipulate output devices. Their activation is coupled to actions performed by the output devices. For example, a graphical object is an output component and any activation of it or of its sub-components triggers changes in the display.

• data components represent the computer memory. The smaller data components are named properties, and correspond to the basic types. Properties have sub-components named READ and WRITE, but like in traditional languages the usual practice is to reserve their use to specific components such as operations as assignments. The activation of the WRITE sub-component is the basis of dataflow: modifying a value can be used to trigger actions such as copying the value to another.

• operation components represent the operations provided by the execution platform, usually the CPU.

• control structure components represent the various ways in which the activation of components can be controlled.

A control structure is a component that creates couplings between other components when it is activated. Control structures are the key to supporting the diversity of control patterns used in interactive software. Standard control structures range from the binding, which creates a simple coupling when it is activated, or the connector, which creates a coupling between a source and a copy instruction, to finite state machines and Statecharts. Other control structures can be created at will by combining existing components.

Assembling components

Complete applications and reusable components can be created from the basic components described above. Basic components are assembled to create large components that implement small interactors. These interactors can be assembled to create larger interactors, and so on.

A simple button, for example, can be built from few graphical shapes (rectangles, gradient, color, text, etc.) associated with a switch and a finite state machine that control the appearance of the button on mouse or touch events. The button can then be inserted in a more complex component to trigger a specific process through a simple binding. component alarm { button b1 (50, 50, "alarm") beep fire_alarm binding (b1, "click", fire_alarm, "start") }

Verifying properties

The djnn framework gives a central role to the tree structure of programs. In particular, mimicking graphical scene graphs introduced a few decades ago, the tree structure is used to express execution control. As a consequence it becomes possible to evaluate some properties by a static analysis of the tree through pattern matching techniques such as XPath requests. For example, the position of a graphical object in the tree tells its relative position to other graphical objects in the same component. Thus, a component situated on the right of another one in the tree will be displayed on top of it if their coordinates overlap. In the same way, djnn implements a flavor of graphical scene graphs in which graphical style components such as color, opacity and stroke width can be placed in the tree and act as context modifiers that affect all the shapes that follow see Figure 1). Pattern matching over the tree structure also enables the verification of component signature. This is a strong requirement in the context of the parallel development of complex graphical user interfaces where it is needed to ensure that a component respect a contract. Suppose for example that one creates a new widget for a WIMP toolkit. It must then be checked that this widget has a width and a height children to ensure that it will be possible to connect them to the layout system. Such a verification can be made by checking that the XPath expressions expr=(/widget/width) and expr=(/widget/height) over the component do not return a null result.

Finally, the combination of Xpath queries to select elements and simple algorithms over their results allows to address more complex case such as the verification of the control flow connecting a sensor to an alarm through various computation units [START_REF] Chatty | Verification of properties of interactive components from their executable code[END_REF].

The djnn platform

djnn is currently available as a collection of libraries and as an interpreter. The core djnn library manages the execution model and the component system. The other libraries each bring a collection of components dedicated to an interaction modality: graphics, input, gesture, sound, etc. Programmers can use these libraries like they would use any programming framework, by writing programs that use the djnn API to create components. The main difference with programming frameworks is that they can create entire applications with component-creation instructions only.

The core djnn library also implements parsers for external component formats, currently XML and Json. Therefore, it can be turned into a component interpretor that reads components from files and executes them. Components can be stored in multiple files in order to support various software engineering processes. In particular, user interface design teams like to store their graphical components in separate files, so that they can be managed independently by graphical designers and merged with the rest of the application at run time only.

APPLICATION SCENARIOS

As an example development process based on djnn, consider an aircraft manufacturer who wants to add new interaction functionalities on a particular cockpit subsystem. This translates into various engineering phases at growing technology readiness levels, from initial exploration to final system development and validation. At lower TRLs, the design processes will ideally reflect the state of the art of user interface design. At higher TRLs, they must reflect the state of the art of requirements engineering and code validation.

In this section, we illustrate a proof of concept experiment where, after observing current practices and gathering requirements from various actors of the aeronautical industry, we tested the role that djnn could play in supporting work at both lower and higher TRLs. The proposed scenarios are very simplified and exaggerated compared to the original industrial situations. Nevertheless, they serve well to illustrate the benefits that could be expected from a unified architecture and execution model such as djnn's. We focus here on the design process of a primary flight display (PFD) i.e. the instrument that displays the basic parameters of the plane. The PFD consists of six parts, as shown in Figure 2:

• Attitude indicator: also known as artificial horizon, it gives information about the pitch (fore and aft tilt) and roll (side to side tilt) of the aircraft (center of the PFD)

• Altitude indicator (right side).

• Airspeed indicator (left side).

• Heading display: displays the magnetic heading of the aircraft (bottom).

• Source selector buttons: control the display of radio magnetic indicators on the heading display (bottom).

• Alerts: alert messages show at the top of the display.

In this prototype, the attitude component has an additional interactive part. Besides displaying altitude of the plane, this component gives an indication on the target altitude for an autopilot. However, while in traditional cockpits, the pilot sets the target altitude with a physical button in a distant part of the cockpit, here the team wants to explore the direct manipulation on the PFD.

In the following scenarios, a group of designers work with test pilots to build a prototype of the graphical appearance and the behavior of a new PFD, then the prototype is sent to the equipment provider. There, a team of developer codes the component and runs automated checks to verify that it has the same behavior as the prototype, while another team runs checks to verify properties that the component needs for inclusion in the existing code-base. Later, the component is returned to the manufacturer, who can run automated checks to verify its conformance with the original prototype. Through the examination of the design process of two components, we show here how the djnn framework supports concurrent development and enables the verification and validation of components.

Increasing fidelity

In the cockpit, the PFD is part of a more complex system of sensors and physical interactors. The team needs to simulate these subsystems in order to test and refine the behavior of the attitude component. At low TRL, the sensors do not have to be realistic. Therefore, the developer chooses to connect the attitude indicator to the best compatible sensor at hand: the motion sensor of his laptop computer. This allows him to perform very fast development iterations. When he is satisfied with his work, the developer needs to send the component to the lead developer who is in charge of integrating several components. He dumps the component to XML format and sends the resulting file to her. The lead developer just has to drag and drop the XML file to her project directory, where it will sit with the other components she has received. Running the master PFD component will load all the components from the directory and execute them. She can use her own motion sensor for testing the result. When the component is mature enough, it can undergo a review process to migrate to a higher TRL. The team in charge of this must test the component against a more realistic environment: a simulation engine controlled by a joystick. They save the component to a directory on the test machine with the proper equipment. The component needs to be adapted to the joystick used for pitch and roll. If necessary, this can be done with a simple rewiring; no modification is required in the component itself. But here, the original developer has added an adaptive behavior to the component: when a joystick is detected, the rewiring is performed automatically, and the component can be used as is.

Concurrent development

A programmer and a graphical designer are producing a component that displays the heading of the plane. Using the initial specification of the component structure as a contract, they can work in parallel. While the designer is creating the graphical skin and layout of the component, the programmer implements the behavior. Here, she uses temporary graphics that the graphical designer has sent earlier (Figure 3a).

When the graphical designer produces graphics, he saves them in SVG format, an XML-based markup language supported by all major vector graphics authoring tools. In this form, the graphics are considered as djnn components and can be manipulated like any other component. The developer can add them to the component he is working on, address them by their name, and connect them to other subcomponents. The names of graphical components in the SVG file are the implementation of the contract between the graphical designer and the developer.

When the final graphics are ready (Figure 3b) the graphical designer can send them to the developer. Replacing the temporary graphics with the new ones is as simple as replacing the SVG file in the appropriate directory and restarting the component. In our case, the graphical designer is late and the component has already been sent to the project manager who gives a demo to visitors in a few minutes. This poses no problem: the project manager saves the file, restarts the component, and the demo is ready.

Parallel design

The altitude component, besides displaying the altitude of the plane, also gives an indication on the target altitude for an autopilot. In traditional cockpits, the pilot sets the target altitude with a physical button in a distant part of the cockpit. For this new design, the team wants to explore the direct manipulation on the PFD. During design sessions, the team has identified several interaction variants. One prototype is developed in order to explore them further with final users. The first option relies on sliding the element that represents the target altitude (the blue element in Figure 4a). The second option is an indirect interaction on a smartphone-like number picker (Figure 4b). Switching from one option to the other is just a matter of loading one component or the other. Here, usability tests highlight manipulation problems with the first option and pilots validate the second one.

Component verification and validation

The airspeed component is subcontracted to an external provider, who delivers it through a web site. The project manager can either download the component and copy it in the component directory as described above or have it loaded dynamically by referencing the URL in the program. He needs to verify that the component will work well with the rest of the application. To do so he runs an automatic verification against the specification of the component, made of a collection of properties. This verification is made on the XML form of the djnn component, using pattern-matching techniques. In the first version of the component, the "ground speed" property is missing and the verification process automatically notifies it. After notifying the subcontractor, the verification is successful for the revised version received, and the component is loaded.

After the integration of all sub-components to the PFD component, the lead developer verifies that all the control flows are well wired. For example, she needs to be sure that alarms will be displayed when required. She uses a program that checks the control flow. The program traces back the control chain from "alert terrain" up to the "altitude" property and signals that it is not connected to any value. In the mean time, the verification raises a warning on the attitude component: two dataflow chains are connected to the same value. Thanks to these warnings, she can deduce than the simulated value of the altitude is connected by mistake to the attitude property, correct it and be certain that the alert terrain alarm will be displayed when needed.

CONCLUSION AND PERSPECTIVES

In this article, we proposed a general framework that provides a semantical unification of control mechanisms in interactive software. This framework relies on a framework whose basic elements are processes, names and events, from which more complex control structures can be defined (transfer of control, activation, interruption, transfer of data, deterministic choice, state machines, etc). On the top of these, a large collection of components have been designed for implementing the pragmatic aspects interaction: management of display (graphics, text, color, ...), input management (mouse, multi)touch), sound, interface with various external devices, etc. djnn is the name of the proposed implementation of this framework. It provides interaction designers and software developers with a platform for developing new components (through a dedicated language), assembling them and running the resulting application.

One long term objective for djnn is to provide the industry with a tool for development of interactive applications adapted to their domains. For this purpose, two major axes must be studied: for the moment, djnn is not supported by an IDE (Integrated Development Environment) similar to Codeblock, Eclipse or TopCased. Such tools useful for djnn users must be developed, especially a graphical editor for djnn models. The question of certification also has to be tackled. In the context of aeronautic, if djnn is used to develop and verify aircraft on-board applications, it must comply with some normative requirements related to software tool qualification (as specified in [START_REF]Software Tool Qualification Considerations[END_REF]).

The framework encompasses mechanisms dedicated to the expression and the verification of properties specific to interactive applications. Based on abstract interpretation, this allows to directly check on the code various properties at design-or system-level. Abstractions based on the component graph as well as the control flow graph retrieved from the code allow to address properties related not only to low level abstraction (code) but also to higher level (user interaction). As all necessary information describing the interaction is available at code level, our approach does not suffer from classical impossibilities related to absence of high level information for verification. Even if promising results for verification have already been obtained, a lot of research remain to be done to explore all the possibilities enabled by this approach.

Figure 1 .

 1 Figure 1. The order in the tree determines the graphical result

Figure 2 .

 2 Figure 2. A primary flight display

Figure 3 .

 3 Figure 3. Heading display: (a) sketch (b) final graphics

Figure 4 .

 4 Figure 4. Altitude indicators: (a) direct manipulation and (b) indirect interaction for setting the target altitude

Concrete semantics are mathematically well defined objects that explicit the meaning and the possible behaviors of the program. Concrete semantics are generally not computable, which makes all non-trivial properties undecidable. To avoid this, abstract semantics are introduced as computable approximations of concrete semantics in which more properties are decidable.

ACKNOWLEDGEMENTS

This work was supported by DGAC projects Fenics and Fumseck, and the EU ARTEMIS JU through project HoliDes (http://www.holides.eu/) SP-8, GA No.: 332933. Any contents herein reflect only the authors' views. No supporting agency is liable for any use that may be made of the information contained herein.


Jean-Aimé Maxa

Mohamed Slim

Ben Mahmoud

Nicolas Larrieu

JOINT MODEL-DRIVEN DESIGN AND REAL EXPERIMENT-BASED VALIDATION FOR A SECURE UAV AD HOC NETWORK ROUTING PROTOCOL

UAV Ad hoc Network (UAANET) is a wireless ad hoc network composed of Unmanned Aerial Vehicles (UAVs) and Ground Control Station (GCS). Compared to the standard Mobile Ad hoc NETworks (MANETs), the UAANET architecture has some specific features that brings exciting challenges to communication architecture design. One of them is the design challenge of a UAANET routing protocols. It must find an accurate and reliable route between nodes in a timely manner to exchange data traffics. It must also be secured to preserve efficiency in the presence of malicious attackers and provides data integrity and authentication.

Furthermore, UAANETs must be certified in the near future to act as autonomous systems without a dedicated safety pilot and to be authorized to fly in the national airspace. In such a context, in this paper, we contribute to the certification of the secure UAANET communication system software using a Model-Driven Development (MDD) approach and real experiments based validation. The validation process followed uses sequentially formal verification methods and real-world experimental results. The objective is to evaluate the routing protocol efficiency to a set of unexpected hazardous issues that come with the real environment.

Introduction

UAVs investigations began after the first world war with preliminary prototypes. Since then, technological and research advances in embedded systems help to produce small UAVs with highly effective capacities. A small UAV is a pilot-less aerial vehicle that has a set of micro electromechanical systems. It can be controlled either autonomously by on-board computers or remotely controlled by a distant op-erator. When several UAVs are communicating with each other via wireless links, they dynamically form a temporary multi-hop radio network called UAV Ad hoc NETwork (UAANET). Compared to the standard Mobile Ad hoc Network (MANETs), UAANETs have some specific features (3D mobility model, low node density, intermittent network connectivity) that brings interesting challenges to the communication architecture design. Indeed, in order to achieve UAANET missions (for instance surveillance and reconnaissance [START_REF] Mancini | The great reconnaissance: a uav project in niger[END_REF]), UAVs must relay network and payload packets between them to the Ground Control Station(GCS). Since the existing routing protocols designed for MANETs fail in tracking network topology changes [START_REF] Rosati | Dynamic routing for flying ad hoc networks[END_REF], adapted routing protocols are required to establish an accurate and reliable route between nodes.

Furthermore, the routing protocol also needs to be secured as it relay critical data traffics ( command/control (c2) traffics, payload 1 traffic and the routing protocol traffic). This is because, in a wireless ad-hoc environment in which there is no fixed infrastructure, the wireless links are prone to link attacks, which consist of passive eavesdropping and active interfering. As a result, routing control packet needs to be authenticated to verify both the identity of the message originator and the message integrity to avoid data tampering and modification.

Likewise, UAANETs applications offers a large possible civil and public domain applications in which one or several UAVs may be deployed [START_REF] Valavanis | Uav applications: introduction[END_REF]. One of the obstacle that stands for its deployments lies on certification restrictions. Indeed, UAANETs must be certified to act as autonomous systems without a dedicated safety pilot or to be simply authorized to fly in the general airspace. On a regional French scale, such a system needs to be fully compliant with the DGAC 2 regulations.

In such a context, the UAANET communication system must satisfy both UAANET network (routing and security) and validation requirements. Accordingly, in this paper, we provide a case study of designing a secure UAV Ad hoc routing protocol applying Model Driven Development (MDD). Our objective is twofold: on the one hand, to minimize certification and evaluation efforts by providing a formal verification capability which ensures quality and conformance of the routing protocol, and on the other hand, to validate the efficiency of the routing protocol through real UAANET test experiments. This validation process is complementary of the formal validation step in order to assess how our software solution behave in real outdoor experiments. It should be noted that this paper is part of the Secure UAV Ad hoc Network ( SUANET ) project presented in [START_REF] Maxa | Secure routing protocol design for uav ad hoc networks[END_REF].

The paper is organized as follows. In section 2, we describe the UAANET communication architecture, routing and security requirements. Section 3 highlights the current UAS certification state of the art. The model driven design of our secure UAANET routing protocol will be detailed in section 4. Then, we will describe in section 5 and section 6, the real-word experiments validation and performance evaluations of our routing protocol. Finally, in Section 7, we provide our conclusions and an overview of our future research perspectives.

UAANET communication architecture

In [START_REF] Li | Communication architectures and protocols for networking unmanned aerial vehicles[END_REF], survey of communication networks of small UAVs are presented. The authors characterize different network architectures: direct communication, cellular and ad hoc networking. Direct communication scheme and cellular networks have several flaws. They require a certain amount of bandwidth for each UAV to support a high node density in the network. Specifically in the direct-link architecture, UAV-to-UAV communications are not possible as data traffic must be routed to the GCS. In regards to the cellular architecture, the existing mobile phone infrastructure is not intended for air-to-ground communication. Since a single UAS transmitter can sweep a wide area with its signal, a UAS deployments may need a dedicated cellular infrastructure. But, the expensive implementation of these base stations is a financial handicap.

In order to address the weaknesses of the communication architectures discussed above, a UAANET can be used for UAV swarm (depicted in Figure 1) in which UAVs and GCS are communicating between each other without the need for a fixed infrastructure. Compared to other communication networks cited above, UAANETs have several advantages. The scalability is ensured thanks to the fast mobility of UAVs to cover a vast area rapidly. Also, the reliability is improved because the failure of one UAV does not affect the whole network. As regards the bandwidth, it can be reused more often and thus more efficiently due to the multi-hop communication. From a security viewpoint, the absence of a central node within the network decreases the risk of attack on a single point of failure. Each end system (UAVS and the GCS) is responsible for the network integrity and authentication.

These features make UAANET the most appropriate solution for UAVs communication. However, it raises a challenging networking problem.

Routing Protocol Challenges in UAANET

Several dynamic routing mechanisms are available for UAANETs [START_REF] Gupta | Survey of important issues in uav communication networks[END_REF]. Topology-based mechanisms, such as proactive, reactive and hybrid routing are the basis of numerous protocols. Nonetheless geographical routing could also be efficient in specific contexts.

In [START_REF] Maxa | Emulation-based performance evaluation of routing protocols for uaanets[END_REF], we introduced an emulation-based performance evaluation of MANETs routing protocols for UAANETs. This realistic study considers the Linux kernel networking stack requirements, the protocol implementations, background traffics, real time execution features and a realistic mobility model. The experimental results showed that AODV [START_REF] Perkins | Ad hoc on demand distance vector (aodv) routing (rfc 3561)[END_REF] routing protocol suits better in UAANET compared to OLSR [START_REF] Clausen | Optimized link state routing protocol (olsr)[END_REF] and DSR [START_REF] Johnson | The dynamic source routing protocol (dsr) for mobile ad hoc networks for ipv4[END_REF]. As AODV being the protocol the most reactive to topology changes and having a limited overhead, we concluded that AODV was the most suitable routing protocol for our scenario. As several studies proved that AODV can be outperformed by proactive protocols with a large num-Figure 1. UAANET Architecture ber of nodes, its on-demand mechanism allows a faster response during UAANETs disconnection. Our mobility pattern and our emulation system certainly affected the measures, but we found similar results to those exposed in [START_REF] Hyland | Simulation-based performance evaluation of mobile ad hoc routing protocols in a swarm of unmanned aerial vehicles[END_REF]. Accordingly, in [START_REF] Maxa | Model-driven approach to design a secure routing protocol for uav adhoc networks[END_REF], we introduce the model design of SUAP (Secure Uav Ad hoc routing Protocol) which is a secure UAANET routing protocol based on AODV.

Security Challenges in UAANET

The ultimate objective of a routing protocol is to find an accurate and reliable route while assuming that nodes in the network are friendly and cooperative. However, such assumption might not always be true as UAANET use an unprotected wireless medium and lack of fixed infrastructure to separate inside nodes from the outside (the attackers). Also, because of the critical level of c2 traffic exchanged, its security must be insured at all cost. Note that there can be different motivations for attackers to breach UAANET. For instance, an attacker may attempt to take control of UAVs by capturing the control and command traffics. This can be achieved through eavesdropping and packet forwarding attacks [START_REF] Butcher | Securing the mavlink communication protocol for unmanned aircraft systems[END_REF].

Generally, securing UAANET is a challenging task due to its cooperativeness characteristic and its uncontrollable environment. Unlike wired networks where attackers need to gain access to the physical medium to execute any types of attacks, in UAANET, an intruder can easily eavesdrop the exchanged traffic through the unprotected wireless links. From our best knowledge, only few secure UAANET routing protocol [START_REF] Maxa | Secure routing protocol design for uav ad hoc networks[END_REF] has been proposed. It can be either a new routing protocol that is designed from scratch with the security as one of its goals or a secure extension of an existing routing protocol. The latter approach is the most used one as it uses a routing protocol like AODV, DSR and OLSR, considered by the IETF MANET group for standardization. Thus, securing those routing protocols requires assessing attacks specific to that protocol and securing them accordingly. This latter approach is used in this paper to create the SUAP routing protocol.

UAS Certification Challenges

To apply for a certificate, UAS is divided into several parts ranging from electronic components, hardware components to software components that need to possess an airworthiness approval [START_REF] Larrieu | How can model driven development approaches improve the certification process for uas?[END_REF]. The advantage of evaluating these components separately is two fold: first, it allows the manufacturer of the different UAS components (engines, propellers) to design components that can be used in several UAS designs. Second, it allows the UAS assembler (in our case Delair Tech company [START_REF] Tech | www . delair -tech . com[END_REF]) to be involved only with the certification of the system, not with each component itself. This reduces the effort needed by the UAS designer to apply for a certificate. Note that a UAS can only be certified by the aviation authorities of the country where the principal place of business of the designer is located. Accordingly, on a regional French scale, our UAS communication system needs to be validated by the DGAC. Although the French UAV professional civil federation 3 is yet to propose a specific validation and certification standards for UAANETs, the process and safety standards depicted within the DO 178C [START_REF] Moy | Testing or formal verification: do-178c alternatives and industrial experience[END_REF] can be applicable for UAANETs [START_REF] Larrieu | Prototypage rapide de logiciel pour les systèmes avioniques: contribution des approches orientées modèle pour la certification de systèmes complexes[END_REF]. DO-178 is a commercial aviation standard used to certify aeronautical systems whose focus lies on Model Based Development and verification supplement with formal verification methods.

Note that, Delair Tech company has previously certified its DT-18 UAV to fly out of sight of the GCS (i.e, the operator). However, the UAANET architecture induces a modification of the existing communication system. As a result, a new validation and certification process is required. Consequently, the secure routing protocol that we are currently building must be the subject of strict validation process. We considered such requirements by using a qualified software development processes using model driven development.

Model driven development of secure UAANET routing protocol

The most used current Linux implementation of AODV (AODV-UU) is a source code that has not been carefully validated and certified. Also, there is no guarantee that all the functional requirements specified by the IETF standards have been implemented. Thus, there is no conformance testing between specification requirements and source code. Consequently, its direct deployment into UAANET is not advisable as it might fail during flight operations and cause meaningful damage. Different compliance testing methods have been developed for distributed communication systems [START_REF] Castanet | Generate certified test cases by combining theorem proving and reachability analysis[END_REF]. However, most of them are goal-oriented testing techniques which consist of choosing a specific property of the target system that is likely to be faulty. One way to overcome this issue is to use MDD approaches that can automatically generate, deploy and verify code by taking as inputs a high-level model.

MDD claims the use of models as primary artifacts in the development process. A system model composed of block diagrams and state charts is the focus of the development process, from requirement specifications to simulation testing and integration. When used with a qualified code generator, it generates a high level codes which facilitate the early verification of the design through formal verification tools. It also execute model-and-code consistency checking for system verification purposes.

Design methodology

Our design is based on Matlab Simulink and Stateflow frameworks. Simulink is composed of a block-diagram environment which allows us to accurately design the routing protocol while the stateflow frameworks allow us to define a finite number of states in the algorithm which are changed based on a defined condition.

Figure 2 represents the model driven development workflow and schematizes the integration process. It is composed of the seven different steps. In the first step, the specification is validated and partitioned into several subsets of the requirements. Each subset has its own unit test objectives. Then, in the second steps, each partition is designed into a high-level model using graphical descriptive language provided by Simulink and stateflow tools. To meet the SUAP security requirements and routing features, we used both security block architectures depicted in Figure 5 and generic routing protocol architecture as shown in Figure 6. The network layer is divided into several blocks exchanging messages between them and adjacent layers. Each block is designed as a state machine which analyzes incoming requests, then sends them in each iteration. The description of these design architectures is detailed in the next section .

Then, during the third step, each block model is converted into C library source code by Mathworks Embedded coder. Note that these source codes are independent of any operating system or hardware architecture. The next step (called glueing) consists of linking the generated code to the kernel space of our target operating system (Embedded Linux generated from OpenEmbedded). In the fifth step, the library code and glueing code are combined into binary files. The next step consists of aggregating the previous binary files with our target operating system to provide a final binary image. The last step is the execution of binary image into the target hardware for verification and validation.

Secure routing protocol design architecture

There have been several proposals to ensure the security of AODV [START_REF] Kannhavong | A survey of routing attacks in mobile ad hoc networks[END_REF]. They provide message authentication and integrity by means of cryptographic techniques for route discovery and route maintenance packets. However, most of them are vulnerable against wormhole attacks [START_REF] Khabbazian | Severity analysis and countermeasure for the wormhole attack in wireless ad hoc networks[END_REF]. The wormhole attack involves two attackers who perform a colluding attack. One attacker record packets at a particular location and replay them at another attacker by using a high-speed private network. This tunnel between two colluding attackers is referred to as a wormhole. Because of the broadcast nature of the radio channel, attackers are able to receive data packets not addressed to them. Figure 3 demonstrates an example scenario of this attack within UAANETs, where A1 and A2 are the colluding attackers while the GCS is the victim node. Even though, each node encapsulates each packet with cryptographic keys, wormhole attackers can breach UAANET security as there is no key required to process wormhole attacks. It should also be noted that wormhole attack is easy to execute as a commercial high-gain antennas configured in specific frequencies can eavesdrop the frequency and receive the signals send by the GCS and the UAVs.

Furthermore, the following assumption is considered in our network and attacker model:

• UAVs and GCS are coming from the same manufacturer which allows us to put aside the security issue from selfish nodes. Apart from being captured or controlled by an attacker, a node will not change its behavior and will always cooperate with its neighbors; • Nodes have sufficient energy power and network resources (i.e bandwidth) to perform cryptographic computation; • All UAVs utilizes omnidirectional antennas.

Communication range is r and cannot exceed Dmax ( r < Dmax ). Dmax is a maximum onehop range; • Nodes rely on efficient symmetric and asymmetric cryptography algorithm for encryption/decryption, authentication and hashing. We envision to use RSA algorithm for message authentication and SHA-256 as a hash algorithm. • All nodes are clocks synchronized. This is possible with the presence of GPS on-board of UAVs and GCS; • We assume that there is an efficient and reliable key management within the network to share, to manage and to revoke node cryptographic keys; • Routing control packet confidentiality is not insured. Indeed, routing packets are processed in real time by the flying UAVs. As such, even if an attacker is able to eavesdrop the message, its action is limited in passive mode because in the future, the past information is no longer valuable. By taking into account, those requirements, we propose the SUAP routing protocol which is a security extension of the AODV protocol, based on public key cryptography, hash chains and geographical leashes [START_REF] Hu | Packet leashes: a defense against wormhole attacks in wireless networks[END_REF]. It uses digital signatures for nonmutable fields 4 and hash chains for mutable fields (i.e the hop count). A node that generates a routing message signs it with its private key, and the nodes that receive the message verify the signature using the sender's public key. The hop count cannot be signed by the sender, because it must be increased at every hop. Therefore, a mechanism based on hash chains is used. As such, SUAP is vulnerable against wormhole attacks. Accordingly, a version of geographical leashes is used to estimate the correlation between the travelled distance and the hop count value. In order to do so, SUAP requires each node in the network to be tightly synchronized and maintain a local connectivity with its direct neighbor.

Moreover, two distinct mechanisms are used to protect against wormhole attacks. The first one is used for hello and route error messages. In our network model, we make the assumptions that, at the bootstrapping, nodes directly send hello messages in broadcast to reckon their directors (one hop) neighbors and detect link breaks. To protect these packets from wormhole attacks, we use a mechanism that analyzes the correlation between hop count and distance traveled by the packet. When sending messages, each node includes its actual location information. To protect from malicious modification, message fields are signed (including the geographical position). Figure 4 illustrates the format of modified beacon messages.

To illustrate our proposition, we considered the Figure 3 and the notation in table I. The connectivity between two legitime nodes can be expressed by [START_REF] Mancini | The great reconnaissance: a uav project in niger[END_REF], with R i, j is the current communication range.

c(i, j) = 1 si R i, j ≤ Dmax 0 si R i, j > Dmax (1)
The presence of wormhole link modify this condition to [START_REF] Rosati | Dynamic routing for flying ad hoc networks[END_REF]. It results that.

c(i, j) = 1 si R i, j ≥ Dmax 1 si R i, j > Dmax (2)
d(No, A1) 2 + d(A1, A2) 2 > Dmax 2 thus, d(A1, A2) > Dmax -d(No, A1)
We have (3) :

Dw = d(A1, A2) + d(No, A1) + d(A2, N3) Dw > Dmax (3)
Knowing that

T = n ∑ i=0, j=0 R i, j
• When the node N0 send the packet, To = Ro1 that corresponds to hc = x + 1 with x ∈ N; • When the node N1 send the packet, T 1 = To + R12 that corresponds to hc = x + 2; • When the node N2 send the packet, T 2 = T 1 + R23 that corresponds to hc = x + 3; thus,

T Dmax -1 ≤ hc < T Dmax + 1 (4)
By taking into account the inequality (3), we can compare the hop count value present in the packet and the hop count value computed on the traveled distance by following the corresponding value depicted in the

0 < To ≤ Dmax 0 Dmax < T 1 ≤ 2Dmax 1 ..... ..... (n -1)Dmax < T n-1 ≤ (n + 1)Dmax n-1
Table II and the formula (4). If there is a difference, the wormhole link is detected, and the packet is rejected. Otherwise, the link is considered as free of wormhole and the signature verification process begins. Note that because of the position information included in the packet, it is possible to compute the relative distance between 2 neighbor nodes using 3D Euclidean distance. The second mechanism is used during the route discovery process in which request and response messages are exchanged. In this mechanism, nodes do not need to send its geographical position. Instead, each node assumes that its local connectivity is secure thanks to the neighbor information provided by the previous mechanism. Each node then send in unicast all route discovery packets to its direct neighbors. Each node also includes the address of the next hop to which the message is forwarded and apply a hash chain to the packet mutable fields. The non-mutable fields are signed as stated previously. An illustration of the request message is shown in Table III. The source node appends its own address and the next node address to the hash chain called Hashnew. It also includes the Hashold (which is the previous Hashnew) within the packet. When an intermediate node says Ni receives a request, it checks its signature and verify the Hash chain. It re-computes the Hash chain with H [previousnode, MyIPAddress, Hashold] and verify if it has the same result as the one included in the packet.

Considering the Figure 3, we compute the hash chain as the following:

The GCS node executes the following operation:

• Select a H hash function;

• Compute Oldhash = H(seed), seed is a value selected randomly by the sender; The operation is repeated until the packet reaches the destination. The same mechanism is also used for the response packet. As regards the exact value of the hop count values, it can be inferred from the number of times that the hash was used for verification. It can also include in the hash chain computation. Note that this mechanism can also be efficient against wormhole attacks involving only one attacker [START_REF] Jain | A survey on complex wormhole attack in wireless ad hoc networks[END_REF].

Security block design architecture

In order to specify our specification into highlevel models, we use a dedicated security design architecture for the security part (depicted in Figure 5) and a dedicated generic routing architecture for the routing part (shown in 6). The specification follows the IETF draft [START_REF] Perkins | Ad hoc on demand distance vector (aodv) routing (rfc 3561)[END_REF] in which each requirement (messages, tables, parameters, extension specification) has been meticulously respected. Our system includes several blocks transmitting signals between them denoting the security and network requirements specifications. They also contain several instances of stateflow graphic representation. These blocks describe the possible protocol behavior as will detail in the following. To give a general idea of the complexity of the SUAP model specification, we present in the Table IV some significant metrics of the global system.

In the security architecture design, each packet received from the link layer must be verified by a module called "Packet identifier" to check whether or not the packet has a security extension. In case, it does not contain a sufficient security extension, the packet is rejected by the Packet rejector module.

The packet rejector module role is to delete suspicious packets. If the packet has its security extension activated, its content is extracted from the Content extractor module. This module explicitly identified which part contains the signature, the hash chains and the location information for the wormhole detector.

Then, the packet is verified by the wormhole tester module which mainly compute either the association between the hop count and the distance traveled by the packet (if beacon and route error messages are exchanged), or compute the actual hash chains for the message. In this step, if the packet fails to prove its required security level against wormhole attacks, it is redirected to the packet rejector module. Otherwise, it is sent to Authentication and Integrity tester module. In this block, the authentication of non-mutable fields and integrity of mutable fields is verified. If all the information within the security extension is valid, the packet is directed to the routing module to check whether or not the packet has reached its final destination.

Regarding routing blocks, The basic routing process is modeled as follows:

• Demux block accepts packet from transport layer (when the actual node needs to search a route towards a given destination) or the link layer. Then, the Demux block verifies the type field of the packets to determine if the packet is for route discovery block or route maintenance block. • Route discovery and Route maintenance block:

Upon the reception of a packet from the "Demux" block, "Route Discovery" and "Route Maintenance" process the same operation. They analyze the encapsulated routing information within the packet to determine its type: RREQ, RREP, HELLO, or RERR packet. • RREQ Mgmt, Hello Mgmt, RREP Mgmt, RERR Mgmt: These blocks determine if the packet carries sufficient routing information and reached its final destination. Based on this result, the packet is transmitted, to the "Packet send handler." • Packet send handler: The "Packet send handler" block is used to retrieve the packet and to update its fields according to its destination, whether to the transport or access layer depending on whether or not the current node is the final destination node. In case the packet has reached its final destination, it is transmitted to the application layer through a user-space daemon.

Otherwise, it is forwarded to the next node in the routing table.

It is important to underline that some functionalities described in the AODV specification has been omitted (e.g. multicast support, gratuitous RREP messages or packet extension) as they are not necessarily needed in our network model.

Formal verification process

A key benefit of MDD is early verification. Verification begins when block models are created and simulated using unit tests based on high-level requirements. In our case, this verification is processed by additional tools as shown in Figure 2:

• Simulink

UAANET real-world experiments

Routing Implementation details

To execute the source code obtained through MDD approach, it is necessary to cross-compile and cross link the embedded Linux C code into the target hardware, which is an ARM board 5 . This cross-compilation is executed with OpenEmbedded framework [START_REF] Team | Openembedded user manual[END_REF] which also generates6 a lightweight and efficient Linux distribution for the ad hoc network communication. It should be noted that our implementation is mainly based on the Linux Netfilter package through a kernel module. We attach each entry and output of our model to the set of hooks points within the Linux protocol stack. Compared to kernel modification methodologies [START_REF] Chakeres | Aodv implementation design and performance evaluation[END_REF], our implementation does not necessitate unnecessary communication (for instance the exchange of ARP packet) and can be installed and initialized through the user-space daemon as in AODV-UU.

Experimentation details

The UAANET architecture that has been set up is shown in Figure 8. The network is composed of 3 nodes, including 2 fixed wing UAVs (DT 18 [START_REF] Larrieu | How can model driven development approaches improve the certification process for uas?[END_REF] developed by the Delair Tech company) and one GCS (also from Delair Tech). The DT-18 is a V. The first UAV called Dr1 is flying at a distance of 250-500 meters from the GCS whereas the second UAV Dr2 flies at a distance 1500-2000 meters from the GCS. Hence, the distance between the two flying UAVs is approximately 1500m. The average altitude of UAVs is estimated at 1127 feet (345 m).

Furthermore, regarding the different types of traffics exchanged between nodes, there are 5 types of data traffics (depicted in the table VI) including:

• Heartbeat traffic: It is a 100 Bytes data packet sent both by the GCS and by each UAVs at 1 Hz frequency. Each node keeps sending heartbeat packet to find out whether or not it is connected to its associated neighbor. If a number of heartbeats messages are missing, the UAV failsafe (can be) is triggered to land the UAVs at the launch point. a customized Linux distribution compiled and built with OpenEmbedded framework. We also attached a HD camera and a Wi-Fi radio interface module. The Wi-Fi radio interface being used is the Mikrotik7 using 802.11n. During the experiments, we enabled space-time block coding to exploit channel diversity in order to avoid interference.The transmission bandwidth was set to 5 MHz and provides half duplex communication.

Each UAV is remotely controlled through a dedicated GCS (Desktop and Infrastructure) as depicted in Figure 8. However, they do not take part in the routing process. Their role is to provide safety links to each UAVs for failsafe management. This is part of DGAC regulation to have at least each UAV connected to a station control via a dedicated links. Each UAV has therefore two links. The first link is either 868 MHz or 900 MHz obtained through XBEE devices 8 . The second link called safety link is a mandatory specification that must be set up to provide recovery assistance when the communication link through the Xbee is not efficient. Figure 7 illustrates the different types of data link deployed.

Test scenario and nodes mobility

During the experiment, Dr2 is firstly launched to a 800 meters distance from the GCS. When it reaches its predilection position, we launched the Dr1 to extend the mission coverage. Dr1 is used as a node forwarder (its payload is not activated) by forwarding Furthermore, their mobility consists of rectilinear and circular movement remotely executed on-demand by the operator through the GCS desktop. The fluctuation between these mobility creates disconnection from time to time and decrease the performance accordingly.

Experimental results

Overhead

The overhead represents the amount of control packet sizes added to data packets. Within UAANETs, despite the constant mobility of nodes, the signaling (size of network control packets) cost of reactive protocols is significantly lower than payload sizes (see table VI). The overhead performance evaluation is shown in table VII The protocol does not generate a significant amount of overhead. Thus, it does not perturb the transfer of payload (video) packets. This good overhead results can be explained by the non-requirements to acknowledge each packet sent compared to DSR protocol and the no need to update an already established route. Indeed, once a route between GCS and Dr2 (through DR1) is computed and established, the protocol no longer seeks the complete topology of the network. Each node only checks its direct neighbor through periodic exchanged of beacon messages.

Route stability

This metric evaluates the delay during which the connectivity is uninterrupted. The result is depicted in Figure 9 and table VIII These results show that on average over 30 minutes test, there is a route loss every 14.5 seconds. This is explained by the node mobility that creates disconnections. One important aspect that must be noted is the stability fluctuation which is caused by the difference in the radiation plane and the polarization plane of the transmitting and receiving antenna which generates a signal attenuation. Indeed, because of the 3D mobility, each UAV has its relative position slightly tilted compared to its direct neighbors position. By comparing the Wireshark trace to the mobility log of each UAV, we noticed a group maintenance packet being transmitted when UAVs mobility mode transition (For instance, from rectilinear waypoint to circular). Consequently, there is a strong likelihood that the combination of the propagation loss and the signal attenuation cause those momentary link breakages.

Moreover, apart the difference at the antenna level, it is important to mention that the introduction of real parameters in real situations impacts the performance. For example, it is noticed in the movement log that when the UAV is cornering, the inner wing mask the modem radio as it is located under the drone. Generally, nodes mobility and antenna polarization issues make it difficult to maintain communication for a long time.

Nonetheless, despite the presence of these intermittent connectivity, the recovery delay is relatively lower (order of 1 milliseconds), thus, the communi- cation performance is not decreased and the payload data are correctly transmitted. As we will see in the next metric, the difference lies in the payload size being transmitted.

In the following, we will analyze the power of the Dr2 received signal to have a clear idea on route loss. hand, the constant oscillation is due to the unstable movement of each UAV during its execution of c2 traffics. On the other hand, the important oscillation peak is caused both by the part of the region that presents a high attenuation and by the signal attenuation (caused by antenna polarization) as explained previously.

Overview of the variation of reception signal strength of Dr2 during the mission

Additionally, based on Figure 11, which shows the correlation between signal strength and route lifetime, we can see that the route lifetime tends to increase (higher quality of service) when the signal quality increases. Since the bandwidth allocated for the data is unchanged over the whole test period, we can conclude that the noticeable fluctuation comes from other physical and topological factors.

Average delay for route establish in case of route loss may be determined through the reception of broadcast hello messages. If any hello message is received from a neighbor for a given time, it indicates that neighbors are no longer within transmission range, thus, the connectivity has been lost.

Figure 12 and Table IX shows the results. We can notice that the delay is quite low given the dynamic features of UAANET. This is because of the small sizes of control packets and the speed of lights which is approximately 3 * 10 8 ms -1 . Our protocol behaves correctly to its requirements specification. The topology change caused by UAVs mobility and speed does not affect significantly the delay to retrieve routes. This is also explained by the fact that the protocol does not wait for the loss of several beacon messages to start looking for an alternative route.

Average end to end delay of control packets

It refers to the time taken for a packet to be transmitted across the network. It is composed of transmission delay, propagation delay, processing delay and queuing delay. Figure 13 and Table X for the communication Dr1 to the GCS. These two graphs indicate a good ability to forward control traffics within the network as we are noticing small delays. The routing protocol does not add significant further delays. Besides, the small sizes of control packets justify the result. We also notice that the communication delay of Dr1 and Dr2 is slightly more important than Dr1 and GCS. This is because the GCS does not move during the duration of the mission whereas Dr1 and Dr2 execute their respective flight plan. It is important to note that the delay may vary depending on the type of control packet (request, response, hello or route error). Nonetheless, due to the small size difference between these packets, we can ignore these differences.

Loss analysis of control and payload packets

This metric measure how many routing control packets are lost during the mission. We also analyzed its impact on the payload traffics by measuring the size of payload packets being lost by the time the route is repaired. As shown in Table XII, we notice a quite important amount of control packet loss (mostly the loss of hello packets). When a certain amount of hello packet is lost, there is a delay to establish a new route. This delay is relatively small (as depicted in Table IX) but not negligible at this level. As a result, payload packets are fragmented and decreased in size as shown in Figure 15. This indicates the degradation of the video quality viewed on the GCS desktop application during the mission.

Conclusion and Future Research

In this paper, we have presented a case study of designing a secure UANET routing protocol applying model driven development approach. We were able to model and generate code through Mathworks (e.g., Simulink and Stateflow) tools. It allowed us an easy, rapid modeling and testing of the algorithms, and avoid many implementation problems by the use of integrated formal verification tools which gives a complete flexibility to the process. We obtained a verified and validated model that contributes to the certification of the final architecture.

We also introduced real test experiments to confront our final embedded software to the real words experiment environments. Our performance results show that our routing protocol fits well to the dynamic topology of UAANET. Despite the route loss for every 14.5 seconds which degrades the video traffic quality, we noticed that the delay to find alternative routes is relatively small, which does not perturb the payload traffic exchanges. However, we add this in our to-do list to have more stable routes and improve our communication architecture performance.

In regards to our short-term perspectives, we are currently working on formal verification of our secure routing protocol with AVISPA tool. It is a useful validation technique for authentication, nonrepudiation and confidentiality. This approach is not fully applied in ad hoc networks. Some researchers had used formal analysis with a mathematical approach but it appears to be hard to automate and time consuming. Our objective is to validate the SUAP security specification. Furthermore, we also plan to perform additional real-world tests to validate our secure routing protocol with a higher node density (3 or 4 UAVs) and by considering different additional scenarios.

Figure 2 .

 2 Figure 2. Set of MDD Tools Used to Design This Secure Routing Protocol

•

  Hash function H is only known by legitimate nodes and pre-loaded with keys at the bootstrapping;• In regards to attackers capabilities, we consider the work of Cordasco et al. in[START_REF] Cordasco | An attacker model for manet routing security[END_REF] based on Dolev-Yao model in which they present a topology and protocol agnostic model that takes into account a real-world scenario. Accordingly, we considered that the following attacks are possible: data traffic disclosure, routing information disclosure, performance degradation and topol-

Figure 3 .

 3 Figure 3. Illustration of Wormhole Attack in UAANETs

Figure 4 .

 4 Figure 4. Format of SUAP Modified Hello Message

Figure 5 .

 5 Figure 5. Secure UAANET Routing Protocol Design Architecture

Figure 6 .

 6 Figure 6. UAANET Routing Protocol Design Architecture

•

  Geographical reference: It is a 80 bytes packet for determining UAVs positions. It is sent from the UAVs to the GCS. 3 packets are sent per second • Command and control traffics sent to each UAV from the GCS. 80 Bytes sent per second. It consists of a flight configuration and waypoint sent by the operator through GCS desktop software. • Network traffic: It consists of routing control packets exchanged between nodes for route discovery and route maintenance. • Payload traffic (video traffic) exchanged from Dr2 to the GCS through Dr1. We sent 25 UDP packets (each packet has 1400 Bytes) per second. On each UAV, we mount an ARM-based computer-on-module produced by Phytec Inc. It runs

Figure 7 .

 7 Figure 7. Communication Links Between Nodes

Figure 8 .

 8 Figure 8. UAANET Real World Experiment Scenario

Figure 9 .

 9 Figure 9. Route Stability Between GCS and DR2

Figure 10 . 3 Figure 11 .

 10311 Figure 10. Variation of Reception Signal of DR2 Strength During the Mission

Figure 10 Figure 12 .

 1012 Figure10shows a combination of constant and peak oscillations during the mission. It shows that the signal power fluctuates during the mission and causes link breakages when it is under -60 dbm. On the one

Figure 13 .Figure 14 .

 1314 Figure 13. End to end Delay Between DR1 and GCS

Figure 15 .

 15 Figure 15. Average Payload Packet Loss

Table I .

 I Notation Table

	Paremeter Description
	hc	Hop count
	Dmax	One hop distance maximum
	Rij	Distance between nodes i and j
	d(No, A1)	Distance between the first target and the first attacker
	d(A1,A2)	Distance between the two attackers
	d(No, A2)	Distance between the first target and the second attacker
	d(A2,D)	Distance between the second target and the second attacker
	Pi	The amount of distance traveled by a packet at the time t
	T	The total distance of the legitimate route
	Dw	The total length of the path through the wormhole link

Table II .

 II Mapping Table Between the Distance Traveled and Hop Count

	T	Hop count (hc)

Table III

 III

		. SUAP Request Packet Signature
		Extension Fields
	Field	Value
	Type	64
	Hash
	function	hash function selected by the sender node. It is used to compute the hash chain field
	Signature	The signature of all the non-mutable fields
		Hashnew = H [CurrentNode, NextNode, Hashold]
		CurrentNode is the address of node
		sending the request packet. It can be
	Hashnew	its public key or its IP Address.
		The Nextnode is the next node public key or IP
		Address.
		Hashold is the previous chain element received
		from the previous node
		It is the previous chain element received from the
	Hashold	previous node. When receiving packets, nodes
		change the value of Hashnew into Hashold
	Hop Count	The actual hop count of the packet.

It is the number of times the hash is performed

Table IV .

 IV Metrics of the SUAP Protocol Specification

	Code lines	6236
	Blocks	30
	Procedures	188
	States	30
	Signals	36
	Macro definitions 14

Table V .

 V Main Characteristics of DT-18 UAVs

	Characteristic	Value
	Model	DT-18
	Payload	250 g
	Range	100 km
	Cruise speed	50 km/h
	Wind	up to 45 km/h
	real-time payload	up to 15 km. Extension to
	transmission	100 km
	Autopilot	Delair-Tech technology
	Onboard computer	payload and communication control, 1 GHz
	Experiment duration 30 minutes
	lightweight UAV capable of long-range flight whose
	characteristics are detailed in Table

Table VI .

 VI The Different Flows Exchanged During the Flight Test

	Type of traffic	Source --Destination	Size	Flow rate
	Heartbeat or Tick	GCS --Dr1 GCS --Dr2	64 Bytes	1 packet/s
	Geographical Reference (Georef)	Dr1 --GCS Dr2 --GCS	80 Bytes	3 packets/s
	C2	GCS--Dr1 GCS --Dr2	80 Bytes	1 packet/s
	Video	Dr2 --Dr1--GCS	1400 Bytes	25 UDP packets/second width=720,height=576
			Request: 66 bytes	1 packet/s for the hello
	Network	Exchanged between Dr1, Dr2 and the GCS	Response: 62 bytes Hello : 62 bytes	Request and Response and Error packets are exchanged
			Error: 54 bytes	during disconnection (route loss)

Table Protocol

 Protocol

	Overhead over 30 minutes
	test
	Overhead	Protocole
	Control packets	352 ko
	Traffic % (bytes) 2.15 %

Table VIII .

 VIII Route Stability over 30 minutes Test

	Metric	Value
	Average route lifetime	14.328955 s
	Maximum route lifetime 34.853527 s
	Minimum route lifetime 4.600461 s

Table IX .

 IX Average Delay to Re-establish Route in case of Route Loss

	Re-establish delay Value
	Average delay	0.001098 s
	Maximum delay	0.004646 s
	Minimum delay	0.000519 s
	This metric computes the recovery time to re-
	store from route loss. It is equal to the time interval
	between the sender of route request (identified with
	a given sequence number) and the arrival of route
	response to restore a route. Network connectivity

Table X .

 X End to end delay summary

	Delay	Value
	Average delay	0.000153 s
	Maximum delay 0.00297 s
	Minimum delay 0.000100s

Table XI .

 XI Average Delay Between Dr1 and Dr2

	Delay	value
	Average delay	0.000549 s
	Maximum delay 0.003 s
	Minimum delay 0.000224s

Table XII .

 XII Control and Payload Packet Loss Summary

	Parameters	Value
	Number of control packet loss	284 packets
	Average size of payload packet loss	12 Bytes
	Maximum size of payload packet loss	52 Bytes

In order to avoid misunderstanding, note that the payload from an UAS point of view is quite different from the network payload traffic, which is the amount of additional data required by traffic control.

DGAC: "Direction Générale de l'Aviation Civile" which is equivalent to the American FAA (Federal Aviation Administration)

The French organization responsible for UAS certification within DGAC: http://www.federation-drone.org/ certification

Routing message fields that does not change throughout the network. For instance, Destination IP Address, Source IP address, destination sequence number, etc.

This is because, the unit test of the routing protocol has been processed with a X86 architecture. As a result, the cross compilation is necessary to add the missing headers required by the cross compiler and the cross linker

configure and build

can be seen in http://www.mikrotik.com/

We have set 868 MHz for the Dr2 (the UAV that goes furthest) and

MHz for Dr1 (the nearest UAV) to avoid interference

Acknowledgments

We would like to express our gratitude to Delair Tech research and development team for their support and help during the real world experiments.