Patrice Micouin

Micouin Consulting

Louis Fabre
email: louis.fabre@airbus.com

Roland Becquet
email: roland.becquet@airbus.com

Thomas Razafimahefa
email: thomas.razafimahefa@airbus.com

François Guérin
email: francois.guerin@mathworks.fr

Property Model Methodology: A Landing Gear Operational Use Case

Relevant for engineering a wide range of technological systems, Property Model Methodology (PMM) is applied in this paper to the development process of a helicopter function in the frame of the ARP4754A/ED79A. After a short presentation of the method, the case study is presented: "to retract and to extend airborne the landing gear system". Then, each stage of the PMM development process is illustrated by examples from the case study: (1) Modeling the top level requirements specification, (2) Validating the requirements specification by proof and simulation, (3) Modeling the architectural design, Refining the top level requirements into requirements specified to the different subsystems contributing to the function and Modeling the terminal subsystems detailed designs (4) Validating the requirements specified to the contributing subsystems by proof or simulation, (5) Verifying the design models by simulation and finally (6-8) Verifying physical implementations by test on the basis of all validation and verification scenarios accumulated throughout the development. At end, lessons learnt and industrial perspectives are summarized highlighting how PMM is a methodology adapted to the challenges facing to systems engineering by the globalization of development processes and showing how PMM can provide a powerful conceptual framework to support digital continuity within globalized Design Organizations. Modeling, simulation, proof and test generation activities are supported by the MATLAB and Simulink products.

Introduction

The aeronautic industry has to deliver more and more complicated systems in term of functions while maintaining high level of quality and safety/reliability. In the same time, competition is driving aircraft manufacturers to strongly improve their costs (including non-recurring costs) and development lead time. At the age of globalization, these systems are designed and produced by large, multicultural, geographically distributed teams belonging to different industrial organizations. This evolution introduces additional complexities (the complexity of a goal-oriented process refers to its propensity to fail [START_REF] Suh | Complexity, Theory and Applications[END_REF]). To face these challenges, classical systems engineering approaches do not provide a sufficient level of efficiency when a huge amount of disparate documents are to be produced, exchanged and used by stakeholders, before being able to reach the expected level of maturity to develop a product. Providing and sharing quickly unambiguous and validated specifications, verified designs and interface descriptions, validation and verification scenarios becomes a key issue to ensure an efficient and safe workflow and a digital continuity between all the stakeholders.

In this paper, the authors synthesize the results of a helicopter function development carried out during the first six months of 2017 at the Airbus Helicopters Design Office. After a brief presentation of the PMM methodology, we provide the reader with descriptions of the applicative context and the H/C (H/C stands for helicopter) function selected as use case. Then, we describe the development sequence by distinguishing at each step the two following levels: (1) PMM methodological guides and (2) Implementation in the MATLAB and Simulink products modeling and simulation environment. Lastly, we summarize the main lessons learnt in this experiment and we identify the way ahead from an industrial point of views. Note that some technical points such as the integration of concurrent modeling activities, physical interfaces derivation from functional interfaces and safety topics are not reported in the frame of this size-limited paper.

PMM process and core concept overview

PMM is a Model-Based & Simulation-Based Systems Engineering method [START_REF] Micouin | Model Based Systems Engineering: Fundamentals and Methods[END_REF] focusing on operational goals. It is a top-down approach that authorises the re-use of pre-existing blocks at any hierarchical level of a system model architecture. PMM complies with current industrial development standards. More specifically, it follows step by step the recommendation ARP4754A/ED79A [START_REF] Sae | ARP4754A, Guidelines for Development of Civil Aircraft and Systems[END_REF]. PMM is a method, derived from the scientific method [START_REF] Bunge | Philosophy of science, volume 1: from problem to theory[END_REF] and applied for engineering technological systems, i.e. a sequence of operative rules, defined to build specification models and design models of engineered systems and expressed in a simulation language. Finally, PMM third pillar is simulation, which is the primary means for validating specification models and verifying design models. It is language-and tool-agnostic and the languages that can support directly PMM are simulation languages such as VHDL [Micouin & alii, 2016], Modelica [Pinquié & alii, 2017] and in the current paper, the MATLAB and Simulink languages as shown through several proofs of concept (POC). The PMM concepts are directly mapped onto simulation language features to produce simulation models. Step 1: Specification Modeling is carried out at the system level, is the development of a goal-oriented system specification model. The PMM concept of a specification model, collecting a set of PBRs, matches with the ARP4754A/ED79A definition of a specification (i.e. a collection of requirements). Figure 1.Step 2: Specification Formal and Factual Validation, a formal validation of the system specification model is performed in order to complete it and to remove contradictions. On this basis, simulation scenarios are defined in order to factually validate the system specification model. So, PMM supports an early and rigorous validation process, before starting a solution definition process.

Figure 1.

Step 3: Architectural Design and Requirement Refinement, we continue with an iterative process that consists in breaking down the system into subsystems. It is, by several aspects, a very classical process. It is acquainted with different design methods such as the Suh 's Axiomatic Design method [START_REF] Suh | Axiomatic Design Advances and Applications[END_REF]. Each subsystem is made up of a specification model and one or more design model alternatives. Thus, a collection of competing system's architectures is considered, and then one is preferred. The subsystems and their connections constitute the system's architecture.

Figure 1.

Step 4: Refinement Validation, at each hierarchical level, the subsystem specification models are validated individually and together against higher level subsystem specification model, from the system specification model to the lowest level. A subsystem is qualified as elementary when it is acquired or when it is not decomposed any further and its behavior is completely defined as a detailed design model. The design process ends when all the elementary subsystems have been identified, and modelled or acquired. Figure 1.Step 5: Design Formal Verification, after this top-down design process, is a bottom-up process that consists in iteratively verifying the elementary design models and then the intermediate design models so as to finally end up with the complete system model. For each integration level, design models are integrated and verified against their own specification models. So, PMM supports a design verification process based on simulation before starting the physical implementation. Figure 1.Step 6 to 8: Implementation Factual Verification, the final steps that deal with the production/verification of the physical products (Hardware and Software), their integration/verification, and the final installation/verification of the system in its environment remains to be experienced practically. It is out of scope of this paper. Note that each step of the PMM process includes recovery points, not represented here, to reengineer the system when a goal is not met at any step.

Furthermore, the process of modeling and simulating a function or system is not monolithically established once only. It is advised to establish it incrementally taking advantage of the additive and parallel nature of PMM constructs.

PBR concept:

The core concept of PMM is the Property Based Requirement (PBRs) Theory defined in [START_REF] Micouin | Toward a property-based requirement theory: system requirements structured as a semilattice[END_REF]. PBRs are predicates that link system or function goals (outputs), observables (outputs) with inputs in order to specify the actualization conditions of system's (resp. function's) properties. The PBRs structure prevents introducing design biases at specification level. The same process applies for secondary (undesired) outputs such as system failures and inputs (expected or undesired). The PBR theory is based on the theory of properties established by the epistemologist Mario A. Bunge [START_REF] Bunge | Ontology I: The furniture of the World[END_REF]. Their basic form is as follows:

PBR #n : when C → val(O.P) ∈ D⊆Im(P)
This statement means: "when the condition C is true, the property P of the object O is actual and its value shall belong to the domain D, where D is a subset of P image" where C is a relevant condition for the system, the function or its environment: a functioning mode, a system state, an (undesirable) event, a time delay or a combination of such features, where the domain D is a finite set, such as {on, off} or an infinite set, such as [0, 1]x [0, +∞[, (possibly linked to a frame and a physical unit) and where D is a subset of the set of actually possible values of the property P, quoted Im(P).

Based on Bunge's property algebra, several PBRs can be combined thanks to the conjunction operator "∧" in order to build composite PBRs. In a dual way, the partial order relationships "≤" and "≥" enable analysts to compare two PBRs. Thus, the expression "PBR 1 ∧ PBR 2 " is the conjunction of PBR 1 and PBR 2 and is itself a PBR. Moreover, the statement "PBR 1 ≤ PBR 2 " means PBR 1 is less constraining than PBR 2 . Thanks to these connectors, the specification model is endowed with an algebraic structure. Each PBR is an element of this structure whose maximum element is the specification model itself.

Context and use case description

A H/C provides its operators and passengers with many capabilities (or functions) depending on its operation phases that enable it to carry out its missions. If we focus our attention on the physical interface between the H/C and the ground, we can identify different capabilities the aircraft has to provide such as (1) "to absorb and to dissipate energy at landing" (2) "to maintain sufficient ground clearance", (3) "to maneuver and to stop on the ground", (4) "to retract and to extend airborne landing gear" or (5) "to ensure landing gears and aircraft integrity", (6) and so on, as this list is not complete.

In this paper, we have chosen to focus our attention on the "to retract and to extend airborne the landing gear" function. The purpose of this function is to provide the crew with the ability to reduce the aircraft drag (Landing Gears -LGs-in retracted position) and to provide it a means for landing (LGs downlocked in extended position). This function is a H/C function because it requires, on the one hand, the interaction of the crew for its control and its monitoring and, on the other hand, the cooperation of several H/C systems for its implementation, namely the Landing Gear System (LGS) as an effector system, a power system such as an Electric Generation and Distribution System (EGDS) or a Hydraulic System, and a control and supervision system such as an Avionics system. It is the proper operation and cooperation of these various systems that makes it possible to obtain the expected effects (functions) at H/C level.

Let us recall here informally some of the intended effects of this function. Some of these intended effects will be rigorously formalized in the next paragraph. We will justify the reasons of this necessary formalization in the next paragraph.

-REQ1: On ground as well as during take-off or landing phases, the landing gears (LGs) shall be fully extended and down-locked in order to prevent any retraction risk. -REQ2: when a LG is fully extended and down-locked, then a green arrow shall signal ("on") in the cockpit and ("off ") otherwise, in less than 50 msec. The presence in the cockpit of these indicators is a specification assumption. -REQ3: when the H/C is airborne and one LG, at least, is in retraction or in extension, then an indication "LG in progress" shall be displayed ("on") in the cockpit [, otherwise the indication "LG in progress" shall be displayed ("off")]. The presence in the cockpit of the indication "LG in progress" is a specification assumption -REQ4: when the H/C is airborne, the LGS is in extension or down-locked [and the normal LG control is not inhibited], if the crew sets in the normal LG control "up" position, then LGS shall reach the "up-locked" position in less than 15 seconds, except in case of retraction failure . The presence in the cockpit of this normal LG control with two positions "Up" and "Down" is a specification assumption. -REQ5: when the H/C is airborne and when the LGS is in retraction or up-locked [and the normal LG control is not inhibited], if the crew sets in this normal LG control "Down" position, then LGS shall reach the "down-locked" position in less than 15 seconds.

-REQ6: when the H/C is airborne, if the crew sets in the "Down" position the emergency LG control, then [the normal LG control shall become inhibited in less than 50 milliseconds] and the LGS shall reach the "down-locked" position in less than 90 seconds excepted in case of Emergency Extension Failure. The presence in the cockpit of this emergency LG control with two positions "Off" and "Down" is a specification assumption. -[REQ7: when the H/C is airborne and the LGS is down-locked and the normal LG control is inhibited, if the crew sets in the emergency LG control's "off" position and sets in the normal LG control's "down" position, then the normal LG control shall become disinhibited]. -REQ8: A normal LG control failure shall not impair the emergency LG control. It is assumed here (ASSUMP1) that an emergency extension failure can have two causes: a fault of emergency control part or a fault of operative part while a normal extension failure can have two causes: a fault of normal control part or a fault of operative part of the LGS.

We also make the following additional assumptions and definitions, inherited from the H/C pre-development phase:

-The landing gear system LGS is tricycle system made up of a Nose Landing Gear (NLG) and two main landing gears (MLG: LLG for the left LG and RLG for the right one) -Contact with the ground is elaborated from three redundant sensors (N, L and R) Weight on Wheel signaling a LG loaded or not. -The H/C is on ground if and only if the three sensors signal a load (DEF1 in the sequel).

-The H/C is airborne if and only if the three sensors signal no load.

At the time of the experiment, this function was under development in the frame of a new H/C developed by Airbus Helicopters and the experiment was considered as an aid for the actual development.

To specify the right function or the right system Suh highlights in [Lee & [START_REF] Suh | Axiomatic Design and Fabrication of Composites Structures[END_REF]] that: "many designers deliberately leave their design goals implicit and then start working on design solutions even before they have clearly defined their design goals. They measure their success by comparing their design with the implicit design goals that they had in mind, which may or may not what the customer wanted. They spend a great deal of time improving and iterating the design solution and "what they had in mind" converge". This blurred and hasty approach reported by Suh, is actually costly and inefficient and is opposed to the scientific approach, which prescribes defining a well-formed problem before attempting to solve it.

The PMM methodological guide for top-level specifications PMM sets as paramount objective for the development team to specify the right system or function, i.e. system or function that meets the needs of its acquirer and other relevant stakeholders such as the crew, certification authorities or the safety service. If this goal is not achieved, the developed system may not meet the actual need.

Step 1 Specification Modeling:

To achieve this objective, PMM asks the development team to establish a specification model of the system or function to be developed. Conceptually, a specification model is a formal model including (1) system (respectively function) requirements, (2) system (resp. function) interface requirements and (3) system (resp. function) assumptions and (4) formal definitions. These features are expressed according to the Property Based Requirement (PBRs) Theory.

Thus, the development team expresses each definition, assumption and requirement that it thinks to be relevant for specifying the function in the form of a PBR. (1) Goals that are system outputs are modelled as inputs of the specification model. (2) Then the actualisation conditions of these goals are identified. These conditions are modelled either as observables or as expected inputs. where WOnW stands for Weight on Wheel, N, L and R stand for Nose, Left and Right. REQ6: when AC State = airborne and if Emergency LG control position ="Down" → Normal_control_status = "inhibited" after 50 msec and LGS position = "down-locked" after 90 sec REQ8: when LG.Normal_Control_fault ="true" → LG.Normal_control_fault = "false" ASSUMP1: when LG.Emergency_Control_Fault ="True" or LG.Operative_Fault= "true"→ Emergency_Failure = "true"

Step 2 Specification Formal and Factual Validation:

Obviously, once determined, requirements are not miraculously correct, and once established, a specification is not miraculously complete either. They may include specification errors. This is why the ARP4754A/ED79A introduced a validation process of requirements and assumptions for engineering aircraft systems. The goal of the validation process is to remove specification errors. The PMM concepts of formal and factual validation deepen the concept of validation of requirements and assumptions defined by the ARP4754A/ED79A standard.

Certainly, representing requirements into formal models is more demanding than writing requirements in an informal and lax language, concealing all the pitfalls and ambiguities of natural languages, but it offers several advantages:

-it forces the specifier to formulate without ambiguity his/her expectations and prevents any form of procrastination, frequent when specifications are textual, -formal modelling of a specification allows a formal validation of the top level system (resp.

function) specification model. The compilation process of the models guarantees the syntactic coherence of the interfaces. More, PMM formal validation is a process to guarantee the formal completeness (no logical holes) and formal correctness (no logical contradictions) of specification model regarding its inputs and outputs possible values. When logical holes or logical contradictions are detected, the specification model has to be updated until the successful completion of the formal validation. In this case, the specification model is considered as formally validated. -the simulation of a specification model formally validated linked with the corresponding specification mirror model allows a factual validation of the top level system or function specification model regarding a given set of validation scenarios. The goal of this process is to guarantee the factual completeness of specification model (stakeholders confirm there is no behavioural holes) and factual correctness (stakeholders confirm that the observed behaviours of the function or system are the right ones and none is missing). PMM factual validation is a process involving the relevant stakeholders such as program representatives, test pilots, flight engineers, safety representatives and authority or customers. It provides the stakeholders with a simulation of the expected behaviours of the function or the subsystem on the basis of the selected validation scenarios. When behavioural holes or incorrect behaviours are detected by the stakeholders, the specification model has to be updated until the successful completion of the factual validation. In this case the specification model is considered as factually validated.

At end, when the specification model is formally and factually validated, it is presumed as error-free and it designates the right function or the right system. However, its physical feasibility remains an open issue, possibly covered by physical prototyping when risks are identified.

Implementation based on MATLAB and Simulink Products.

Specification modeling and specification validation:

The PMM concept of a PBR can be easily implemented as a conditional assertion (Boolean function) with various simulation languages such as those mentioned above. Simulink provides a very convenient way to model them thanks to two blocks coming from Simulink libraries: Assertion and Implies blocks.

As examples, the following block diagrams model PBRs: definitions, requirements and assumptions: A PMM specification model can be easily implemented as Simulink subsystem embedding a set of conditional assertions operating concurrently on the specification model inputs.

As an example, the following block diagram models a specification model of the extension/retraction function.

Figure 6. Specification Model for the extension/retraction function at Helicopter level.

Note that a specification model has only inputs and no outputs. The specification model inputs are connected to system model and design model inputs, outputs and probes (observables). At this stage of the development, we use Simulink Design Verifier to detect logical holes or logical conflicts in the specification model in order to complete and to correct it, when necessary.

Specification logical hole:

A logical hole may occur when the conditions for which O.P shall be in Im(P)-D remain unspecified, while O.P shall be in the domain D when C is true or when a condition value remains unspecified.

As an example of logical hole, in the use case description above section (REQ3), the removal of the phrase dealing with the conditions under which the "LG in progress" indicator shall be "off" (marked with square brackets [] and italic text) introduces an (intentional) logical hole in the specification.

Specification logical contradiction:

A logical contradiction occurs in the following context: O.P shall be in the domain D and simultaneously in the domain D' when C with D∩D'=Ø (empty set).

As an example of logical contradiction, in the use case description above (REQ7), the removal of the phrases dealing with the inhibition/disinhibition of the normal control (marked with square brackets [] and italic text) makes room for a logical contradiction in the specification in the following conditions: the H/C is airborne, if the normal LG control is set in "Up" position (retraction order) and the emergency LG control is set in "Down" position (emergency extension order).

Simulink Design Verifier provides computational means to detect such logical holes or such logical contradictions when the specification model is instrumented with the relevant proof (or test) objectives and submitted to the analysis of the Simulink Design Verifier proof engine or test generator. In our case, it is capable of falsifying proof objectives or test objectives and of exhibiting counter examples putting the specification model at fault . Simulink Design Verifier confirms that the hole has been removed as soon as the conditions for which the indicator shall be "off" or as soon as the inhibition/disinhibition mechanism have been modeled in the specification. -at the bottom right side, a graphical visualization of LGs position evolutions between 0 (fully retracted position) and -100 (fully extended position).

Basically, a validation bench represents the system to be validated in its operation environment.

As shown on the figure 8, the LGS is, at the snapshot time, normally extending, and just the RLG is already down locked while the other LG are not yet completely extended and locked. This is the reason why the Right Green Arrow shall be "on", the others shall be "off" (compliance with REQ2), while the "LG in progress" indication shall be "on" (compliance with REQ3).

The goal of the validation bench is to show the stakeholders how the system is expected to behave in different situations of its operational life. Stakeholders are expected to comment on these behaviors: they may agree with them, reject them, ask for additions or changes. The specification model has to be reworked and the factual validation ends when the behavior shown is agreed and committed by the relevant stakeholders.

The validation process is based on validation scenarios built relying on the system CONOPS and additional scenarios including failure scenarios, emergency procedures, handling errors, and so on. Note that the following points are not documented here: (a) Validation scenarios are performed manually and can be recorded for later replay. Systematic scenarios based on Simulink Design Verifier capabilities are also possible to reach a defined validation level of rigor according to the ARP4754A/ED79A recommendation (b) the specification mirror model is a design doing exactly what the specification model is expecting.

On the LGS project, the use of the validation bench allowed to confirm with the test crew the simulated behaviors, to clarify the expected behaviors during an emergency extension sequence of landing gears, to request the specification of additional requirements for new warnings in some circumstances, etc.

In the following table is shown how the PMM formal and factual validations cover the validation aspects of the ARP 4754A recommendation: To design and to implement the function or the system right As shown in figure 9, and in accordance with Suh's Axiomatic Design [START_REF] Suh | Axiomatic Design Advances and Applications[END_REF], system models "must be decomposed until we get a complete detailed design or until the design is complete.

However, contrary to conventional wisdom on decomposition, they cannot be decomposed by remaining in design domain only. One must zigzag between the specification and design domains to be able to refine requirements and design parameters".

PMM methodological guide for architectural design and requirements refinement

Step 3 Architectural Design and Requirement Refinement: Based on a formally and factually validated specification model, the design phase can be initiated. One candidate architecture description of the system or the function is introduced in the form of a design model comprising subsystem models and links between these subsystem models (internal interfaces) and the links with the system model external interfaces. Subsystems modeled can be discrete (causal) with signals links (unidirectional) or continuous (acausal) with links power flows (bidirectional) or else hybrid (including discrete and continuous parts) with signals and power flow links. As an example, LGS extension/retraction function is distributed on several aircraft systems including avionics, electrical, hydraulic and mechanical landing gear systems. Alternate design models can be considered to seek for the best (Time, Cost, Quality, Performance) TCQP design trade-off.

According to the Suh's zigzagging masterful view, system level PBRs have to be refined into subsystem PBRs allocated to the various subsystem models composing the considered architecture in order to assign to each subsystem its role and responsibilities to achieve the system goals. These subsystems PBRs derive from the system PBRs and from the architectural design choices.

Figure 10. Subsystem specification models validation wrt System specification model Design activity and PBRs refinement involve knowledge of the various engineering disciplines concerned as well as those of the safety specialists. It also calls for collaborative working between the different engineering discipline designers to share a common goal, to agree roles and responsibilities for each system and to make the necessary tradeoffs. The material basis on which this collaborative work is carried out is the design model. It constitutes a common objective reference on which mutual commitments (subsystem PBRs and interfaces) are based, as well as a contractual design practice.

Step 4 Refinement Validation: According to PMM, before separating and further developing the various subsystems concurrently, the team has to validate the refinement of the system PBRs into subsystems PBRs to ensure that this refinement is correct and complete and does not lead to incoherencies or to gaps. To be valid, for a given system design model A, the conjunction of the refined PBR 1 , …, PBR n assigned to subsystems must be more constraining than the system PBRs.

When A → PBR ≤ PBR 1 ⋀ ... ⋀ PBR n
In this case, according to the PMM Prime Contractor Theorem, if each physical subsystem meets its commitments (specification) then the system integrated in accordance with its design model will respond to its own specification.

PMM system design phase ends when no further design decomposition is needed and when detailed design models are established by the designers (internal or external in case if the lower level is delegated to a supplier) on the basis of the knowledge of their respective engineering disciplines.

Step 5 Design Formal Verification: As any implementation product made by humans, design models may include design errors. So, they have to be verified in order to remove design errors, to ensure that fault tolerance and reconfiguration mechanisms are really efficient and then to produce a physical system free of design error.

While specification, design modeling and specification validation are interleaved and top-down ("zig-zagging" in the words of N.P. Suh) processes, design model verification is performed in a bottom-up process: 1-First, the lowest level design models are verified regarding their own specification model. 2-Second, the lowest level design models can be (1) integrated and ( 2) the resulting integrated design model can be verified regarding the corresponding specification model 3-Lastly, the integrated design models can be (1) integrated to produce the top level design model and installed in its simulated environment (2) the top level design model can then be verified regarding the top level specification model on the basis of operational scenarios.

This design verification process has to be performed with a level of rigor corresponding to the required Design Assurance Level (DAL) of the subsystem and verification scenarios have to be built in order to test the design model compliance with the specification model. At any level, the design models have to be formally verified: i.e. discrepancies between the design model outcomes and the expectations of the previously validated specification model have to be searched for and can be detected during simulation runs. In that case, design model should have to be corrected in order to comply with its specification model. This process ends when all the design models from the bottom to the top level comply with their respective specification models. Then, they are considered as formally verified.

Step 6 to 8 Implementation Factual Verification: As stated above, step 6, 7 and 8 (verification of physical implementations) is not documented in this paper.

Implementation based on MATLAB and Simulink Products

Simulink and Stateflow, possibly associated with Simscape, provides capabilities for building design models including discrete subsystems, continuous subsystems and hybrid subsystems linked as appropriate by signals and/or power flows in order to design systems including avionics, mechanical and electrical subsystems. These links can represent functional or physical bonds depending on the system development stage.

Figure 11. Landing Gear Function Design Model.

Figure 11 represents an architectural design model of the LGS extension/retraction function that introduces the contributing subsystems: the LGS itself connected to others contributors: a hydraulic system, an electrical system, avionics and LG panels for controls indications and alerts. Connections are unidirectional for signals and bi-directional for power flows.

Additionally, Simulink provides the "reference system" feature allowing to model concurrently and separately the design of each subsystem composing the elements of the system design model with its specified requirements.

Again, Simulink Design Verifier provides us with a validation means for the refinement of system (resp. function) PBRs into PBRs subsystems. For this purpose, the objective of the proof to establish is that each system PBR must be satisfied as soon as all the subsystem PBRs that refines it are also true. This is the exact translation of the PMM Prime Contractor Theorem. Otherwise, a PBR refinement error has been made and must be corrected.

With appropriate tools, design models including continuous subsystems and hybrid subsystems linked as appropriate by signals and/or power flows are built to model and simulate the behavior of mechanical, hydraulic, thermal and electrical subsystems according to their connections. These connections can represent functional or physical bonds depending on the system development stage. Simulink and Stateflow provide capabilities for building design models representing discrete subsystems that can be transformed into as software code or simple or complex electronic hardware in order to design avionics or others Airborne Electronics Hardware (AEH).

Then, in order to (1) develop several alternate design models of the same system, and (2) to freeze significant stages of system development, including factual validation, functional design and physical design stages, Simulink provides the "variant system" feature allowing to model several alternate design models with the same definite external interfaces and simulate any of them by simple configuration before a simulation run.

The last point, which could not be established in the context of the reported experiment, was to generate, for discrete systems, systematic verification sequences according to the level of rigor related to the Design Assurance Level (DAL) assigned to the function or the system considered.

For this purpose, the process is (a) To defined the verification (test) objectives ensuring the required level of DAL, (b) To instrument the specification models with the relevant verification objectives, (c) To generate, using Simulink Design Verifier, the right sequences of inputs, driven by the instrumented specification models; and recorded in a "signal builder". (d) To launch the builder signal that will stimulate the models the design models while the specification models monitor design models outputs.

Note that the design verification sequences are recorded in the signal builder and may be used for similar usages (e.g. to verify physical products themselves).

Lessons learnt and industrial perspectives

Confirming the preliminary results of the previous POCs, the experiment showed practically the feasibility and relevance of the PMM process on an actual full scale case. It has helped to remove ambiguities in first level specifications. It enabled the test pilots to validate the expected behavior specified by the top level specification model. It initiated a collaborative design working and it also helped in the establishment of subsystem specifications for suppliers. Although the demonstration is not complete for implementation verification aspects, it supports the claim that PMM reduces the time and risk of system development and consequently the system development non-recurring costs.

At the same time it increases the maturity of the system definition. In this experiment, the MATLAB and Simulink products proved to be well adapted to the PMM methodological expectations while we benefit from very mature means. This confirms our vision on PMM enabling capacity to drastically improve efficiency in H/C complicated system developments.

Currently, PMM provides means to model failures and faults and to specify the expected behavior in case of faults, to design systems avoiding or tolerating faults by redundancies and reconfiguration mechanisms and to demonstrate the compliance of these designs with the safety requirements. However, it remains for PMM to provide a systematic way to echo safety analyses and connect safety activities with development activities to support a Model Based Safety Assessment (MBSA) in accordance with the ARP 4761A [SAE, forthcoming] that should be released soon.

Complexity Reduction: PMM method, shared with partners and suppliers, should strongly ease the challenge of complicated aircraft development in such a globalized design organization context. The unambiguous and formal aspect of PMM, relying on an objective basis provided by simulation should provide means to improve cooperation among organizations, to prevent and overcome misunderstandings, introduced by cultural differences and that abound in current development organizations. In addition, technical basis of contractual work share among industrial alliances will be more efficient and leaner by providing a formal definition of roles and responsibilities and technical commitments.

Digital Continuity: While the digital continuity provided by digital engineering documents may be questionable, the PMM methodology, with its simulable digital products (specification and design models, interface dictionaries and V&V scenarios) provides a powerful conceptual framework to support digital continuity while transferring its openness to the interoperability of simulation environments.

Reuse: PMM provides means to transform a large amount of specification and design patterns as assets for reusing them in subsequent or derivative developments, paving the way of a very industrial and effective development process of technological systems. So, progressively after several program deployments the PMM will even more facilitate efficiency in product lines development through straightforward and efficient reuse. Louis Fabre I'm the Senior Expert for software and system of software at Airbus Helicopters R&D directorate, coordinating an expertise group in the "cockpit design, computers and software" department. I'm acting in the airborne software domain for around 30 years, starting at Aerospatiale commercial aircraft and then at Airbus Helicopters, covering a wide range of activities from development, verification up to certification aspect. I participated to the early trials of PMM identifying quickly the potential of the method to support an early formal definition and validation of systems requirements and design, allowing reducing the amounts of open problems at software level.

Patrice Micouin

Thomas Razafimahefa

I am working in landing gear design office from Airbus Helicopters, my department is responsible to develop wheels landing gears for medium and heavy helicopters. I work in this department since 9 years and I was involved on several domains of this system such as: supply chain technical support focal point, installation & integration responsible (installation & definition drawings, procedures…), system engineering responsible (specification, certification document redaction, supplier management) . Now I am in charge to modelize landing gears systems through simulation tools to validate systems expectations. I am working in the group which implements the Property Model Methodology.

Roland Becquet

With 17 years of experience in landing gear design, I have been involved in several landing gear developments either as structural analysis engineer or as design engineer, both in SAFRAN Landing Gears and in Airbus. I have been an Airbus Helicopters' Landing Gear expert and ATA32 (landing gear) compliance verification engineer (CVE) since 2016. In the expert role, I actively participated, either as writer or as validator, to Airbus Helicopters ATA 32 specification based on the "Property Model Methodology". In addition to expert activities, I am in charge in the design office of the continuing airworthiness activities of landing gears.

François Guérin

François Guérin is a principal technical consultant with over 10 years' experience assisting companies in the implementation and optimization of Model-Based Design. He specializes in providing guidance for the development of high-integrity systems in aerospace and rail. Prior to joining MathWorks, François was a member of the Control Distributed and Automation group of the University of Cambridge, and a software engineer at Alten France. He received a B.Eng. in European engineering and an M.S in control engineering from Coventry University.

Figure 1 .

 1 Figure 1. PMM processes and steps numbered from 1 to 8 Roughly described, PMM usually starts just after the validation of a Concept of Operations (CONOPS) [ISO/IEC/IEEE, 2011] and is made up of eight steps:

Figure 1 .

 1 Figure 1.Step 1: Specification Modeling is carried out at the system level, is the development of a goal-oriented system specification model. The PMM concept of a specification model, collecting a set of PBRs, matches with the ARP4754A/ED79A definition of a specification (i.e. a collection of requirements). Figure1.Step 2: Specification Formal and Factual Validation, a formal validation of the system specification model is performed in order to complete it and to remove contradictions. On this basis, simulation scenarios are defined in order to factually validate the system specification model. So, PMM supports an early and rigorous validation process, before starting a solution definition process.

  (3) Eventually, the result of the analysis is formalized as one or several PBRs packaged function by function, if necessary. Here are some definition, assumption and requirements model examples: DEF1: The AC is on ground ↔ WOnNW = True and WOnLW = True and WOnRW = True

Figure 2 .

 2 Figure 2. DEF1: The HC is onGround, if and only if Weight on Wheels are "on".

Figure 3 :

 3 Figure 3: REQ6 Simulink Implementation

Figure 7 .

 7 Figure 7. PMM System Model including a Specification Model and a Design Model interconnected During a simulation run, the specification model monitors the design model and checks its compliance status with respect to requirements at each simulation step. In case of requirement violation, the violation is logged and the simulation may be stopped. Specification Formal Validation: Formal validation of a specification model is supported by Simulink Design Verifier, a tool belonging to the MATLAB and Simulink product list. Basically, it provides several means to verify Simulink models including (1) formal methods to identify hidden design errors and (2) test inputs generation for model coverage and custom objectives.

Specification

  Factual Validation: While PMM formal validation of a specification model is a matter of models coherence, factual validation is a matter of model consistency with respect to an extra-modeling reality such a legal reality or a contractual reality (the distinction between formal coherence and factual consistency relies on the difference between formal truth and factual truth [Leibniz, 1714]): the expectations of relevant stakeholders such as those of acquirers, operators, regulation authorities and so on. The factual validation of specification model should rely on a model previously formally validated. Factual validation requires the definition of three additional artifacts: (1) a validation bench and (2) a particular model, called specification mirror model (3) Validation scenarios.

Figure 8 .

 8 Figure 8. Factual validation bench (Snapshot). The figure 8 shows a bench developed in order to factually validate the LGS extension/retraction function. It includes: -at the top left side, relevant actual LG controls and one virtual button to control the ground/flight condition, -at the bottom left side, environmental conditions (OAT, Airspeed and load factors) affecting the extension/retraction of the LGS and the manual or recorded to replay control scenarios, -at the middle the AC level function model, -at the top right side, the relevant actual LG indicators, LGS in progress indicator and Green Arrows and Nose Wheel Locked in Axis indication.

Figure 9 .

 9 Figure 9. Zigzagging between specification and design domains.

Figure 12 .

 12 Figure 12. Hydraulic Physical Design Model.

Figure 12

 12 Figure 12 represents the hydraulic design model introduced for controlling the LGS extension/retraction mechanism. It introduces the contributing components: tanks, pumps, pipes, valves, monitoring indicators and hydraulic ports. Note here how the PMM systems engineering is close to the concerned engineering discipline and to its own language.

Figure 13 .

 13 Figure 13. Multibody Physical Design Model of LG.

Figure 13

 13 Figure 13 represents a mechanical design model of the LGS extension/retraction mechanism. It introduces the contributing components: cylinders converting hydraulic power into displacements of the landing gear parts according their mechanical links in the relevant geometrical frames. Parts or assembly models are imported from a 3D Aircraft Digital Mock-Up ensuring the consistency of data with our PMM functional and behavioral mock-up.

  I'm the inventor of the Property Model Methodology (PMM). As a late outcome of my PhD in the Automotive Systems Engineering domain (2006), I published in the Systems Engineering Journal (2008) a disruptive theory of Property-Based Requirements (PBRs). The lack of an engineering methodology tightly related to engineering disciplines and providing a vehicle for my PBR theory, as well as my practice of simulation languages gradually led me to propose a systems engineering method: PMM. Targeting initially causal systems, I extended it to multiphysics systems. Currently, I work for the Airbus Helicopters Design Office. Pascal Paper In Airbus-Helicopters R&D Method, I lead engineering transformation project relying on Property Model Method to increase system designer efficiency. From 2005 to 2012, I leaded transnational Multi-System Physical Integration department in AIRBUS aircrafts. Between 1999 and 2005, I leaded Airbus Concurrent Engineering deployment for series programs and A400M. From 1992 to 1999, I leaded lofting & master geometry in Aerospatiale Aircraft. From 1989, I was responsible for 3D method within Aerospatiale space leading a project aiming to set up configured DMU for ARIANE 5. I started my career in Dassault-Aviation on a PHD on Radar Cross Section numerical 3D computation.

Table 1 :

 1 ARP 4754A validation goals and PMM coverage

	ARP 4754A validation		PMM
	aspects	Formal validation	Factual validation
	Correctness	No logical contradiction	Correctness commitment by stakeholders
		proof or test	based on an objective basis (specification
			model)

Completeness

No logical hole proof or test Completeness commitment by stakeholders based on an objective basis

Acknowledgements

Authors warmly thank A. Jenni (head of Vehicle Systems and Installations), C. Haefflinger (head of Vehicle Basic Systems) and V. Pacheco (head of Landing Gear Systems) for their kindness and their support during this experiment, M. Achache (Executive Manager Technical Audit Avionics) for his relevant comments on the paper, R. Pinquié, A. Barouni and V. Paredes for their contributions during the experiment and finally L Espié & J Wirtz for having sponsored PMM project through Airbus Helicopters R&D Method&Tool fundings.

Property Model Methodology (PMM) is a registered trademark of Patrice Micouin MATLAB and Simulink are registered trademarks of The MathWorks, Inc. See mathworks.com/trademarks for a list of additional trademarks. Other product or brand names may be trademarks or registered trademarks of their respective holders


Thibault Catry
email: thibault.catry@ird.fr

Zhichao Li
email: zhichao.li@teledetection.fr

Emmanuel Roux
email: emmanuel.roux@ird.fr

Vincent Herbreteau
email: vincent.herbreteau@ird.fr

Christophe Révillion
email: christophe.revillion@ird.fr

Nadine Dessay
email: nadine.dessay@ird.fr

FUSION OF SAR AND OPTICAL IMAGERY FOR STUDYING THE ECO-EPIDEMIOLOGY OF VECTOR-BORNE DISEASES IN TROPICAL COUNTRIES

Vector-borne diseases like malaria represent a major public health issue worldwide. Other mosquito-borne diseases affect more and more countries and people, with effects on health which are not all identified yet. Recent developments in the field of remote-sensing allow to consider overriding the existing limits of studying such diseases in tropical regions, where cloud and vegetation cover often prevent to identify and characterize environmental features. We highlight the potential of SAR-optical fusion for the mapping of land cover, the identification of wetlands, and the monitoring of environmental changes in different habitats related to vector-borne diseases in the French Guiana -Brazil cross-border area. This study is the foundation of a landscape-based model of malaria transmission risk. Environmental factors, together with epidemiological, socio-economic, behavioral, demographics, and entomological ones, contribute to assess risks related to such pathologies and support disease control and decision-making by local public health actors.

VECTOR-BORNE DISEASES

Malaria has declined by 37% between 2000 and 2015, nearly half of the world's population remains at risk (about 3.2 billion people, [START_REF]World Malaria Report 2015[END_REF], Fig. 1). Other emerging mosquito-borne diseases (e.g. dengue, chikungunya, Zika) affect more and more countries and people, with lasting effects on health which are not all identified yet. Various possible causes of rapid spreading of dengue and Zika epidemics have been identified: climate change, demographic growth, urban growth, urban fragmentation, ecological changes, increase in travels and international trade, disturbances in health systems and vector control efficiency, land cover/use changes... It is also known that natural and human-made ecosystem changes, such as climatic perturbation and land use and land cover (LULC) changes, can affect significantly the distribution of malaria by making disease vector (anopheles darlingi mosquito) habitats more or less suitable [START_REF] Stefani | Land cover, land use and malaria in the Amazon: a systematic literature review of studies using remotely sensed data[END_REF][START_REF] Li | Mapping a Knowledge-Based Malaria Hazard Index Related to Landscape Using Remote Sensing: Application to the Cross-Border Area between French Guiana and Brazil[END_REF]. Hence, the prevention and control of vector borne diseases requires to identify, characterize and monitor these environmental factors, their changes and their impacts on the emergence of diseases. In this context, using remote sensing appears to be a pertinent tool that can characterize almost completely and continuously the environment related to vector-borne diseases transmission.

VECTOR-BORNE DISEASES AND REMOTE-SENSING

There has been a growing use of remote sensing data in epidemiology in the last 30 years [START_REF] Herbreteau | Thirty years of use and improvement of remote sensing, applied to epidemiology: from early promises to lasting frustration[END_REF][START_REF] Stefani | Land cover, land use and malaria in the Amazon: a systematic literature review of studies using remotely sensed data[END_REF], but some limitations usually occur, like (1) the price of very highresolution data, (2) the general use of pre-processed data, (3) some technical limitations and (4) the fact that vector-borne diseases are strongly scale-dependent. In tropical regions persistent cloud cover and dense vegetation cover strongly affect the use of remotelysensed data for environmental purposes. The adaptability of remote-sensing data is then limited when addressing epidemiology. Stefani et al. [START_REF] Stefani | Land cover, land use and malaria in the Amazon: a systematic literature review of studies using remotely sensed data[END_REF] did a systematic review of literature studying the relationship between malaria and land cover/use types in the Amazon (Fig. 2). -How to describe social discrepancies and their influence?

-How to characterize the dynamics of multiscale processes?

-How to provide real-time information, for monitoring and surveillance systems?

-How to facilitate the transfer of data and products towards the research community, actors of health services and the public?

CASE STUDY

Context

The Franco-Brazilian cross-border region considered here is composed by the French municipalities of Camopi, Saint-Georges-de-l'Oyapock and Ouanary, which are located on the western bank of the Oyapock River, and the Brazilian municipality of Oiapoque on the eastern bank of the river (Fig. 3). The human habitats in this study area mainly locate in Saint-Georges (FR), Oiapoque (BR) and the villages of Camopi (FR) (see the red rectangles in Fig. 3). In the Americas, the Amazonian region is the most affected by malaria. Movement of malaria across international borders poses a major obstacle for malaria elimination due to various human activities, population movement, human vulnerability due to limited formal education and few financial resources, inadequate health systems, etc. [START_REF] Wangdi | Cross-border Malaria: A Major Obstacle for Malaria Elimination[END_REF].

Methodology

Overall methodology In this study, we follow a four step approach (fig. 4) which is part of a more general landscape-related malaria hazard model. This model is based on the exploitation of an optical image (like SPOT 5) in order to establish a simple forest/non forest land cover classification. This classification then integrates information regarding wetlands distribution extracted from a SAR image (L-band SAR like PALSAR) and a layer of urban classification derived from very high resolution sensors (optical alone or optical and SAR combined together). These land cover classes are then confronted to epidemiology and entomology data in order to calculate spatialized landscape indicators used to create malaria hazard/risks maps to be delivered to local authorities and public health actors.

Images characteristics and treatments

One SPOT 5 image was acquired at 1A level in which radiometric calibration and orthorectification have been successively performed by using the ENVI 5.1. For the PALSAR image acquired at level 1.5 in which radiometric calibration, geometrical correction and speckle filtering (Lee filter 3*3) have already been performed by Japanese Space Agency (JAXA).

Several spectral indices were calculated from the pretreated SPOT 5 MS image. A decision tree-based classification was then carried out for mapping the various LULC types using ENVI 5.1 (Fig. 5). The resulting classification was post-processed using the majority analysis (kernel size 3*3) for removing the isolated pixels. Finally, we evaluated the classification by randomly choosing 20 sites in each class and establishing the actual land cover of these sites by photo-interpretations of one Pleiades image dated September 30, 2012 with a 50-centimeter spatial resolution.

A textural analysis (GLCM under Sentinel tool box) was performed and a simple thresholding method on the variance of PALSAR signal and a colored composition (Red = VH, Green = VV, Blue = VH/VV) was then used for extracting bare soil, flooded forest, forest, free water and swamps (fig. 6).

A multi-sensor approach

Optical data

Figure 7 shows the resulting SPOT 5 classification. The overall accuracy was found to be 0.90 and the kappa coefficient was 0.84. Comparing with the SPOT 5 classification, this method allowed us to characterize free water, flooded forest and swamps (Fig. 8) using an archive 2010 image. Moreover, it is important to remind that we used free archive PALSAR imagery in order to test the contribution of L-band SAR data to the identification of malaria environmental features, before considering the acquisition of expensive new L-band data.

The validation of PALSAR classification is complicated but some insights could be obtained from 2010 archive optical imagery if the cloud cover is not too dense. Recent field surveys during the similar period (similar season) can also be used for the validation since the identified wetlands are not strongly changed with time.

L-band SAR (here 12.5 m resolution PALSAR data) is an efficient tool for the detection of large wetlands, which can define main resting, and breeding sites of malaria vectors.

A multi-resolution approach

High spatial resolution data (SPOT 5, S2, S1, PALSAR) are used to characterize areas covered by various types of forest, where adult mosquitoes rest and feed. This part of the study focuses on the relationship between the environment and the vectors of the disease, i.e. the "hazard" component of the malaria transmission risk. Very high spatial resolution data (SPOT 7, Pleiades, TerraSAR-X) will be used to characterize urban and peri-urban structures and domestic wetlands, where breeding sites for mosquitoes are frequent. This part will focus on the relationship between the environment and human populations, i.e. the "vulnerability" component of the malaria transmission risk.

A multi-temporal approach: S1 and S2

The repetitivity of Sentinel data (up to 5 days) will allow the production of land cover maps on a weekly basis, from free satellite imagery. Combining S1 and S2 products, the monitoring of urban and peri-urban changes, at the interface with forest areas and wetlands, main « mosquito reservoirs » and sources of epidemic risk, is to be made possible. These data should be used to update a preexisting map of urban and peri-urban areas, established from a sensor like SPOT 5 (similar resolutions in space). The combination of SAR S1 and optical S2 data should be efficient tool to overcome disturbances from persistent cloud cover over the studied area. Finally, Sentinel images are to be combined to meteorological data (from satellite or ground station) to better constrained the role of rainfall in the evolution of wetlands in the area.

FUSION OF OPTICAL AND SAR data

On the basis of remotely-sensed and field data, the fusion of layers containing spatialized information extracted from optical and SAR images from various sensors and at various resolutions will favour the production of indicators and maps to support decisionmaking processes by public health actors (fig. 9) Figure 9: Process of fusion of various remotely-sensed data at the decision-level (from [START_REF] Pohl | Review article multisensor image fusion in remote sensing: concepts, methods and applications[END_REF]).

DEFINITION OF LANDSCAPE INDICATORS

In this study, we use a model previously established by Stefani et al. ([2], Fig. 10). This paper proposed a generic model of the relationship between deforestation and malaria transmission risk emerges from the literature. It considers that: i) deforested areas can procure favourable conditions for An. darlingi breeding, ii) forest and secondary vegetation can define resting sites for adult An. darlingi mosquitoes that return to the forest after feeding, when houses are located close to the forest and iii) that malaria transmission risk depends on the spatial distribution of LC types and, in particular, the interaction level between human populations and LC/LU types associated with breeding and resting sites. This generic model is schematically represented in Figure 9. This shows the importance of distinguishing different situations by considering the LC/LU types over time in terms of both proportions and spatial distributions.

TOWARDS EPIDEMIC HAZARD MAPS

This study shows that fusion of land cover layers extracted from optical and SAR high-resolution imagery is an efficient tool for detecting large permanent (or long-lasting) wetlands (potential breeding sites) and various forest types (potential resting and feeding sites). Land cover classification of SPOT 5 image suffers two mains flaws: the impossibility to penetrate the forest canopy and disturbance from persistent cloud cover in tropical areas. In particular, L-band SAR has proven its ability to detect the water under forest, a key element for the identification of breeding sites of malaria vectors and malaria vector control. Until now, only free archive SAR data were used in order to test the methodology but the acquisition of PALSAR 2 data is planned. Its main advantage is the possibility to access very high spatial resolution. Combining very high resolution optical (SPOT 6-7 / Pleiades) together with the very high resolution SAR permit characterize the urban structures and minor sizes, non-permanent water bodies such as domestic wetlands within the urban areas, at the direct contact with vulnerable populations.

These results of land cover classification fusion from optical and SAR data are the basis of a landscapebased model of malaria transmission risk (Fig. 11) The layers of forest / vegetation and wetland types, are then combined to a layer of urban classification and 2 fieldbased layers: one regarding the entomology of mosquitoes and the malaria epidemiology in the area. These combined layers allow the calculation of landscape indicators and consequently the creation of malaria transmission risk map integration vector-related environmental information (hazard estimation) and human related environmental factors (vulnerability assessment).

CONCLUSION

This study provides a method of identification of environmental features associated with malaria vector resting and breeding sites. Optical and SAR remote sensing have been proved to be complementary for this purpose. This method provides the complete LULC information about malaria transmission, which may be automatically and easily reproduced at temporal scale using a time series of images. The fusion of layers containing spatialized information extracted from optical and SAR data from various sensors and at various resolutions aims at producing indicators and malaria transmission hazard/risk maps to support decision--making processes by local institutions /authorities and public health actors.

Data processing methodologies developed in this study will be automated and made available to the science community and the actors of public health. All products (land cover maps, hazard maps) will be made available on a preexisting platform. These results contribute to Theia CES "health and environment" and "land cover".

Figure 1 :

 1 Figure 1: Malaria incidence rates by countries from 2000 to 206, WHO, 2015.

Figure 2 :

 2 Figure 2: Relationship between malaria and land cover/use types in the amazon [2].. Black = positive correlation, grey = no correlation, white = unknown. Using remote-sensing for studying vector-borne diseases however implies some challenges -How to quantify the role of environmental factors on the transmission of such diseases compared to other factors like sociodemographic and behavioral factors?

Figure 3 :

 3 Figure 3: Map of cross-border region between FrenchGuiana and Brazil.

Figure 4 :

 4 Figure 4: 4 steps methodology developed in this study, in the frame of a landscape-related malaria hazard model.

Figure 5 :

 5 Figure 5: Classification decision tree applied to optical imagery. Decision tree nodes are in grey.

Figure 6 :

 6 Figure 6: Summarized method of optical-SAR classification fusion for mapping the malaria environmental features. Combining the information from SPOT 5 and PALSAR data using the knowledge-based decision rules: 1) If a pixel belongs to PALSAR free water or SPOT 5 free water, then the pixel is labelled as free water; 2) If a pixel belongs to PALSAR bare soil or SPOT 5 bare soil/built-up/road, then the pixel is labelled as bare soil/built-up/road; 3) If a pixel belongs to one of PALSAR wetlands classes and SPOT 5 vegetation class, then the pixel is labelled as wetland.

Figure 7 :

 7 Figure 7: Pixel-based land cover map of SPOT 5 image in the region of Saint-Georges and Oiapoque.

Figure 10 :

 10 Figure 10: Landscape indicators that may increase or decrease malaria transmission risk as a function of time and landscape fragmentation [2].

Figure 11 :

 11 Figure 11: Landscape-based model of malaria transmission risk involving the decision-level fusion of spatialized information layers.

Proc.'Living Planet Symposium 2016', Prague, Czech Republic, 9-13 May 2016 (ESA SP-740, August 2016)

ACKNOWLEDGEMENTS

This research was supported by the TéléPal project (CNES-TOSCA 2014 call), and the China Scholarship Council. We greatfully thank ESA for inviting us at the LPS 2016 in Prague.