Archive ouverte de l'ENAC
Not a member yet
3458 research outputs found
Sort by
Code-Level Formal Verification of Ellipsoidal Invariant Sets for Linear Parameter-Varying Systems
No full textInternational audienceThis paper focuses on the formal verification of invariant properties of a C code that describes the dynamics of a discrete-time linear parameter-varying system with affine parameter dependence. The C code is annotated using ACSL, and the Frama-C's WP plugin is used to transform the annotations and code into proof objectives. The invariant properties are then formally verified in both the real and float models using the polynomial inequalities plugin of the theorem prover Alt-Ergo. The challenges of verifying the invariant properties in the float model are addressed by utilizing bounds on numerical errors and incorporating them into the real model
Simplifying Forwarding Data Plane Operations with XOR-Based Source Routing
No full textInternational audienceWe propose a theoretical analysis of a novel source routing scheme called XSR. XSR uses linear encoding operation to both 1) build the path labels of unicast and multicast data transfers; 2) perform fast computational efficient routing decisions compared to standard table lookup procedure without any packet modification all along the path. XSR specifically focuses on decreasing the computational complexity of forwarding operations. This allows packet switches (e.g, link-layer switch or router) to perform only simple linear operations over a binary vector label that embeds the path. We provide analytical proofs demonstrating that XSRs efficiently compute a valid unicast or multicast path label over any finite fields F2w. Furthermore, we show that this path label can be used for both the forward and return unicast paths, unlike other source routing algorithms that require recomputing a label for the return path. Compared to recent approaches based on modular arithmetic, XSR computes the smallest label possible and presents strong scalable properties, allowing it to be deployed over any kind of core vendor or datacenter networks
Geodesic regression on SE(3): Application to estimation of positions of a mobile
No full textInternational audienceWe address the problem of estimating the position of a mobile such as a drone from noisy position measurements. To model the motion of a rigid body, rather than considering trajectories in the state space as is usually done in functional data analysis, the framework of differential geometry is used. More precisely, the trajectory of the mobile is modelled as a Lie group-valued curve. The relevant Lie group for poses of a rigid object happens to be the Special Euclidean group SE(n), with n = 2 or 3. This work takes place in a parametric framework which extends linear regression in an Euclidean space to geodesic regression in a Riemannian manifold. This method was later on extended to higher order polynomials on Riemannian manifolds, and explicitly written in SO(3). Based on this approach, our goal is to implement this technique to the Lie group SE(3) context. Given a set of noisy points in SE(3) representing measurements on the trajectory of a mobile, one wants to find the geodesic that best fits those points in a Riemannian least squares sense. A more general mathematical formulation is established by using differential forms. Finally, applications to simulated data are proposed to illustrate this work. The limitations of such a method and future perspectives are discussed
Learning Uncertainty Parameters for Assistance in Conflict Resolution
No full textInternational audienceHelping Air Traffic Controllers (ATCOs) to solve conflicts is challenging because ATCOs only have a partial control on pilots reaction time and trajectory change, and cannot estimate very precisely the aircraft speed. A previous research [1] proposed a method to estimate ATCOs' uncertainty margins during their deconfliction task. It was shown that, given a predefined uncertainty model, it is possible to learn uncertainty parameters on two-aircraft exercises resolved by an automatic solver. In this article, we collect new data on a more realistic simulator showing a Singaporean En-Route sector and estimate individual and collective uncertainties. These uncertainties are then used in the automatic solver and the resolutions are compared to the actual maneuvers given by the ATCOs. Results on 6 ATCOs who performed several hours of control show that common uncertainties could be estimated with an error of the same range as individual uncertainties. When these uncertainties are used in the automatic solver the solutions are conform to the ATCOs decisions 77 per cent of the time which is 15 percent higher than without considering uncertainties. ACKNOWLEDGEMENT We thank the ATCOs from ENAC who volunteered to participate in our experiments, giving several hours of their time. Their involvement is essential for collecting relevant data
Attentional switch to memory: An early and critical phase of the cognitive cascade allowing autobiographical memory retrieval
No full textInternational audienceRemembering and mentally reliving yesterday's lunch is a typical example of episodic autobiographical memory retrieval. In the present review, we reappraised the complex cascade of cognitive processes involved in memory retrieval, by highlighting one particular phase that has received little interest so far: attentional switch to memory (ASM). As attention cannot be simultaneously directed toward external stimuli and internal memories, there has to be an attentional switch from the external to the internal world in order to initiate memory retrieval. We formulated hypotheses and developed hypothetical models of both the cognitive and brain processes that accompany ASM. We suggest that gaze aversion could serve as an objective temporal marker of the point at which people switch their attention to memory, and highlight several fields (neuropsychology, neuroscience, social cognition, comparative psychology) in which ASM markers could be essential. Our review thus provides a new framework for understanding the early stages of autobiographical memory retrieval
Approche PLNE pour replanifier les vols lors de perturbations survenant sur un mode d'accès d'un aéroport
No full textInternational audienceAirport access mode disruptions, such as a subway shutdown, threaten the whole passenger door-to-door journey. When such a disruptive event occurs, knowledge on passengers' delays would help the airport operation centre to decide if a departure flight should be delayed. This paper proposes a tactical flight rescheduling at an airport to minimise the number of stranded passengers while considering operational constraints. An integer linear programming formulation of the problem is presented. Constraints such as terminal capacities, maximal runway throughput, minimum turnaround time, or minimum transfer time for connecting passengers are considered. An exact and a heuristic resolution are proposed and compared on a study case around Paris-Charles de Gaulle airport. The new schedule satisfies the operational constraints and reduces up to 60% the number of stranded passengers with moderate deviation from the initial planning.Une perturbation survenant sur un mode d'accès à un aéroport, telle qu'une panne de métro, peut compromettre le trajet porte-à-porte des passagers. Lorsqu'une telle perturbation se produit, la connaissance des retards passagers aiderait les opérateurs aéroportuaires à décider si un vol au départ doit être retardé. Cet article propose une replanification tactique des vols dans un aéroport afin de minimiser le nombre de passagers manquant leur vol tout en tenant compte des contraintes opérationnelles. Une formulation du problème en programmation linéaire en nombres entiers est présentée. Les contraintes de capacité des terminaux, de débit maximal des pistes, de temps de rotation minimal ou encore de temps de transfert minimal pour les passagers en correspondance sont prises en compte. Une résolution exacte et une heuristique sont proposées et comparées sur un cas d'étude de l'aéroport Paris-Charles de Gaulle. Le nouveau planning satisfait les contraintes opérationnelles et réduit jusqu'à 60% le nombre de passagers bloqués, tout en assignant un retard modéré aux différents vols
Modélisation, simulation et émulation d'applications distribuées dans des essaims de systèmes cyber-physiques déployés dans des réseaux dynamiques
No full textThe research field in distributed systems has witnessed a recent growing interest in wireless mobile distributed computing, i.e. distributed algorithms deployed in dynamic networks. Such systems introduce new challenges due to their time-varying topologies, which hinder the performance and safety guarantees of algorithms that are fundamental building blocks of more complex distributed algorithms. The main focus of this work is to establish different ways to study such systems via emulation and simulation and to propose some techniques to deploy applications in dynamic networks. We evaluated different data flow paradigms, such as many-to-many distributed storage, one-many computational offloading, and many-to-many decentralized swarm control and data load-balancing.We adopted the quantitative approach as a cornerstone methodology, using simulation and emulation to collect data for analysis. Even though there are many discrete simulators in the state-of-the-art, there was a gap for emulation tools applied to mobile ad hoc computing. Some important features were missing, such as a full-scale emulated deployment environment where prototypes coexist with off-the-shelf applications and more options for mobility control. This work proposes MACE, a framework that enables the emulation of mobile distributed applications in a virtual environment so that the scenarios and topologies composed by mobile wireless nodes can be easily modified. Since emulation requires that the tests run in wall time, the need for a fast simulator arose. Therefore, we designed, implemented and validated a fluid model that simulates traffic flow in mobile ad hoc networks. With this model, we finally implemented a simulation tool that enables fast algorithm and parameter analysis and can potentially be embedded in constrained nodes for in-flight mission re-evaluation. The fluid model can scale to large topologies with hundreds of nodes and could complete experiments running stress workloads with simulation time shorter than the simulation time horizon. It can also be configured with bounded and unbounded network queues, use mixed mobility models and control laws, and model different applications running in the application layer mixed with synthetic traffic injection. By studying different control laws, we can reduce the probability of enduring network partitions and enhance the traffic balance to reduce the formation of bottlenecks that hinder the application's performance.Our work also encompassed the proposal of some applications related to the domain of UTM, such as optimized edge-assisted offloading algorithms for swarms of UAVs that can be potentially used for UTM Distributed Detect and Avoid systems. Moreover, we also propose a distributed position tracking data layer for very low-level airspace using State Machine Replication and could achieve low end-to-end latencies even with a high number of replicas.La recherche sur les systèmes distribués a connu récemment un intérêt croissant pour les applications pour un environnent mobile, c'est-à-dire les algorithmes distribués déployés dans des réseaux dynamiques et sans fil. Cependant, la conception de ses systèmes présentent de nouveaux défis en raison de leurs topologies variables dans le temps, qui peuvent compromettre la performance et la sûreté des algorithmes distribués. L'objectif principal de ce travail est d'établir différentes manières d'étudier de tels systèmes via l'émulation et la simulation, et de proposer quelques stratégies pour déployer des applications en environnent mobile. Nous avons évalué différents paradigmes de flux de données, tels que le stockage distribué multi-nœuds, l’ordonnancement de tâches de calcul sur plusieurs nœuds, le contrôle décentralisé des essaims de drones et l'équilibrage de la charge de données.Nous avons adopté une approche quantitative comme méthodologie de base, en utilisant la simulation et l'émulation pour collecter les données à analyser. Bien qu'il existe de nombreux simulateurs discrets dans l'état de l'art, aucun n’était adapté à l’émulation des systèmes répartis sur des réseaux mobile ad hoc. Certaines caractéristiques importantes manquaient, telles qu'un environnement de déploiement émulé à grande échelle où les prototypes coexistent avec les applications réelles et davantage d'options de contrôle de la mobilité. Ce travail propose MACE, un environnent qui permet l'émulation d'applications mobiles distribuées dans un environnement virtuel de sorte que les scénarios et les topologies composés par les nœuds mobiles sans fil peuvent être facilement modifiés. Comme l'émulation exige que les tests s'exécutent comme les vrais systèmes, le besoin d'un simulateur rapide s'est fait sentir. Nous avons donc conçu, mis en œuvre et validé un modèle fluide qui simule le flux de trafic dans les réseaux mobiles ad hoc. Avec ce modèle, nous avons finalement mis en œuvre un outil de simulation qui permet une analyse rapide des algorithmes et des paramètres et qui peut potentiellement être intégré dans des nœuds contraints pour une réévaluation de la mission en temps d’exécution. Le modèle fluide peut s'adapter à de grandes topologies avec des centaines de nœuds et peut réaliser des expériences en exécutant des charges de travail sous contrainte avec un temps de simulation plus court que l'horizon temporel de l’émulation. Il peut également être configuré avec des files d'attente de réseau limitées et non limitées, utiliser des modèles de mobilité et des lois de contrôle mixtes, et modéliser différentes applications fonctionnant dans la couche d'application avec injection de trafic synthétique. En étudiant différentes lois de contrôle, nous pouvons réduire la probabilité de partitions durables du réseau et améliorer l'équilibre du trafic pour réduire la formation de goulots d'étranglement qui entravent les performances de l'application.Notre travail englobe également la proposition de certaines applications liées au domaine de la gestion du trafic des systèmes d'aéronefs sans pilote (de l’anglais Unmanned Aircraft System Traffic Management, UTM), telles que des algorithmes optimisés pour la bordure du réseau des essaims de drones qui peuvent être potentiellement utilisés pour les systèmes distribués de détection et d'anti-collision UTM. En outre, nous proposons également une architecture de suivi de position distribuée pour l'espace aérien à très basse altitude en utilisant la réplication, où nous avons pu mesurer de faibles latences de bout en bout même avec un nombre élevé de répliques
Cleared for Safe Take-off? Improving the Usability of Mission Preparation to Mitigate the Safety Risks of Drone Operations
No full textInternational audienceDrone operations such as power line inspection, automated deliveries, or crowd control are becoming more widespread. For flights that present serious risks to human safety, operators must conduct safety assessments and get authorizations from the regulators. These preparation tasks are complex and time-consuming but few previous works addressed them. We interviewed 14 professional drone operators, safety study consultants, and 2 regulators to better understand the needs for these tasks. The result is a workable model of the tasks which includes defining the concept of operation, assessing operational risks, and negotiating for authorization. We devised 9 recommendations to inform the design of future mission preparation tools, and consolidated them with a follow-up questionnaire. The recommendations include systematically describing a mission with operational parameters, showing their estimated impact on mission safety, or enabling awareness of the application's status among all stakeholders. We conclude with design concerns and opportunities to inform future research
An EM Approach for GNSS Parameters of Interest Estimation Under Constant Modulus Interference
No full textInternational audienceInterferences are an important threat for applications relying on Global Navigation Satellite Systems (GNSS). Interferences degrade GNSS performance, and can lead to denial of service. The most notable intentional interference family is characterized by its constant envelope, e.g. chirp and tone interferences. Due to its simple structure, the space to search the interference contribution yields to complex circles, allowing the introduction of some latent variables related to those circles. In order to mitigate the interference effect, we compute the maximum likelihood estimator of the parameters of interest (time delay and Doppler shift) in presence of those latent variables. Thus, we resort to the Expectation Maximization algorithm which has already been proved to be efficient in such cases. Experiments conducted on synthetic signals highlight the efficiency of the proposed algorithm