Archive ouverte de l'ENAC
Not a member yet
3458 research outputs found
Sort by
Implémentation des Bigraphes dans Coq
No full textInternational audienceLes bigraphes sont un modèle mathématique introduit par Robin Milner. Ils peuvent être utilisés pour représenter des systèmes concurrents et distribués. Nous avons implémenté une sémantique formelle des bigraphes dans l’assitant de preuve Coq. Cet article présente l’implémentation choisie et comment instancier un bigraphe dans notre bibliothèque
The impact of Augmented Reality and 3D Visualisation in ATS Airspaces' Learning Process
No full textInternational audienceAir Traffic Services airspaces classified as Class A to G refer to volumes, within which specifictypes of flights may operate and for which specific air traffic services and rules of operation arespecified. Within these airspaces, predetermined trajectories such as SID (Standard InstrumentDepartures) and STAR (Standard Arrival Routes) are used by instrument flight rules (IFR)flights from the take-off phase to the approach phase. Learning how airspaces and trajectoriesare designed is essential before starting the practical training. To reach this objective, air trafficcontrol students currently learn through 2D tools as paper documents and Computer-BasedTraining data exercises. It aims at understanding these volumes’ layout to build 3Drepresentations so that air traffic controllers will better apply the corresponding rules andstrategic separations between aircraft in vertical evolution (mostly departures and arrivals)inside these volumes. The objective of this study is to characterise the effects of augmentedreality and 3D visualisation on airspaces learning. An educational tool was designed forvisualising and manipulating airspaces in 3D using a user-centered design approach with airtraffic control students and instructors. To identify their needs in terms of constructing 3Drepresentations during training, we conducted contextual interviews, observations and aquantitative questionnaire. We then iterated by involving users in the prototyping process.Evaluations of the final mock-ups and the functional application were carried out with end-users through questionnaires and interviews in order to assess intrinsic motivation andwillingness to use
Division réseau équitable dans les essaims de nanosatellites
No full textInternational audienceNous proposons de partitionner l’architecture d’un réseau ad-hoc mobile en plusieurs groupes, afin de re-distribuer équitablement la charge entre les membres du réseau. Notre étude porte sur un essaim de nanosatellites fonctionnant comme un télescope spatial distribué, placé en orbite lunaire. Chaque nanosatellite de l’essaim collecte des données d’observation de l’espace, puis les échange avec les autres membres de l’essaim. Les données recueillies sont ensuite combinées localement afin de produire l’image globale observée par l’essaim. Cependant, un système fondé sur ce mode opératoire est particulièrement sensible aux pertes de paquets et aux pannes d’énergie. En effet, la transmission simultanée d’un important volume de données peut entraîner des problèmes de communication, notamment en surchargeant le canal radio ou en augmentant le risque de collisions, menant dans les deux cas `a des pertes de paquets. La consommation énergétique totale de l’essaim est également proportionnelle au nombre de paquets transmis : il faut alors trouver une solution pour limiter le nombre de transmissions afin d’économiser l’énergie des nanosatellites. La principale contribution de ce papier est de proposer une approche basée sur la division équitable du réseau en plusieursgroupes de nanosatellites. Nous comparons les performances de trois algorithmes de division de graphe : Random Node Division (RND), Multiple Independent Random Walks (MIRW), et Forest Fire Division (FFD). Nos résultats montrent que MIRW obtient les meilleurs scores en termes d’équité, peu importe le nombre de groupes produit
Memory Recall for Data Visualizations in Mixed Reality, Virtual Reality, 3D and 2D
No full textInternational audienceThis article explores how the ability to recall information in data visualizations depends on the presentation technology. Participants viewed 10 Isotype visualizations on a 2D screen, in 3D, in Virtual Reality (VR) and in Mixed Reality (MR). To provide a fair comparison between the three 3D conditions, we used LIDAR to capture the details of the physical rooms, and used this information to create our textured 3D models. For all environments, we measured the number of visualizations recalled and their order (2D) or spatial location (3D, VR, MR). We also measured the number of syntactic and semantic features recalled. Results of our study show increased recall and greater richness of data understanding in the MR condition. Not only did participants recall more visualizations and ordinal/spatial positions in MR, but they also remembered more details about graph axes and data mappings, and more information about the shape of the data. We discuss how differences in the spatial and kinesthetic cues provided in these different environments could contribute to these results, and reasons why we did not observe comparable performance in the 3D and VR conditions
Assessing GNSS Carrier-to-Noise-Density Ratio Estimation in The Presence of Meaconer Interference
No full textInternational audienceIn the context of Global Navigation Satellite Systems (GNSS), the measure of the Carrier-to-Noise Density Ratio (C/N0) plays a critical role in evaluating received signal quality, particularly in the presence of Radio-Frequency Interferences such as from a meaconer. This paper presents a dual-step strategy to characterize C/N0 under meaconer influence. First, the theoretical expression of the real C/N0 is computed. Second, a model to predict meaconer-induced distortion on the Moment Method (MM) and the Narrowband-Wideband Power Ratio (NWPR) estimators is derived. The comparison between real and estimated C/N0 reveals a deviation between NWPR, MM and real C/N0. In essence, this work enhances comprehension of meaconing-induced C/N0 distortion
Kalman Filter for Dynamic Estimation of Stochastic Radio Source Power and DoA
No full textInternational audienceInterferometric measurements corresponds to sample covariance matrices of signals received by several sensors. In scenarios like dynamic radio astronomy imaging, the properties of these signals can vary over time, presenting a challenging case for study. In this context, this work tackles the problem of estimating stochastic radio source power from sample covariance measurements. A novel approach is developed, introducing a nonstandard Kalman filter tailored for Gaussian noise and signals, expanding the Kalman filter's applicability range to situations where the underlying measurement model is unknown. The effectiveness of this approach for source power and direction of arrival estimation are illustrated through simulations using synthetic data
Modeling and Optimization of the Design of a Robotic Hydroponic System
No full textInternational audienceThe progress of space exploration towards establishing human colonies on extraterrestrial bodies, coupled with the pressing need to address the climate crisis on Earth, underscores the significance of developing sustainable and self-sufficient cultivation techniques. A review of the existing literature reveals that most research in this area has concentrated on the operation and control of robotic hydroponic systems, often applied to off-the-shelf designs. However, by focusing solely on operational aspects, past research may have overlooked opportunities for significant resource savings that could be achieved through structural optimization. We propose in this paper a framework to optimize the structure of an automated Nutrient Film Technique (NFT) hydroponic system to minimize resource consumption (e.g. energy and plant nutrients), mass and volume. The modelling and optimization process employs Multidisciplinary Design Analysis and Optimization (MDAO) techniques to accommodate the diverse range of disciplines involved and the multiple optimization objectives of the system. The proposed framework considers the composition of the crew and computes the optimal structure tailored to meet their dietary requirements, based on the selected optimization objectives. To evaluate the system’s performance, our framework incorporates criteria inspired by the innovative Advanced Life Support System Evaluator (ALiSSE), developed by the European Space Agency (ESA), which offers a comprehensive system approach for assessing life support systems. Through rigorous analysis, consistency of the model and optimization is demonstrated, yielding expected results, and affirming the effectiveness of the approach.<br /
Optimisation dynamique de la mobilité du passager multimodal
No full textMultimodal transportation represents an innovative approach to contemporary mobility challenges in logistics and transportation. By skillfully integrating different modes of transportation, multimodal transportation provides a comprehensive and efficient solution to the need to move goods and people. The synergistic combination of different modes of transportation creates complex, interdependent multimodal networks, where the failure of a single element can have a significant impact on the entire network. This thesis focuses on the analysis of the vulnerability of transportation systems to disruptions, and proposes a topological approach aimed at guaranteeing the minimum optimal operation of these networks, which is crucial for the mobility of the affected passengers. As a first step, a vulnerability model has been developed to quantify the vulnerability of passenger routes to disruptions. This model combines the number of alternative paths and the flow of passengers on the routes. The integration of this model into the route selection process was tested on the Sioux Falls city road network. By incorporating this model into the route selection process, we were able to mitigate the impact of network disruptions on passenger travel. We then focused our research on improving the overall robustness of transportation networks. The approach adopted is to make small structural adjustments to the network in order to maximize the number of alternative routes. These alternative routes provide solutions in the event of network disruptions. This method was applied to the low-cost flight network in mainland France. Finally, the last component of the transportation network to be optimized concerns vehicles. This final section focuses on enhancing the robustness of aircraft flight paths in the face of unforeseen meteorological obstacles. The method used combines a trajectory generation algorithm, a clustering algorithm, and a filtering process to generate a set of dissimilar alternative trajectories. The results indicate that topological improvements in robustness at all levels of the transportation network effectively mitigate delays caused by unforeseen disruptions to the overall travel time of network passengers.Le transport multimodal incarne, dans le domaine de la logistique et du transport, une approche prometteuse pour adresser les défis contemporains de la mobilité. En intégrant habilement différents modes de transport, le transport multimodal offre une solution complète et efficace pour répondre aux besoins de déplacement des marchandises et des personnes dans une démarche durable et respectueuse de l'environnement. La combinaison synergique de différents modes de transport engendre des réseaux multimodaux complexes et interdépendants, où la défaillance d'un seul élément peut entrainer des répercussions significatives sur l'ensemble du réseau, difficiles à appréhender à une échelle globale. Cette thèse se propose d'étudier l'apport de divers outils mathématiques en réponse à ces enjeux via l'analyse de la vulnérabilité des systèmes de transport face aux perturbations, et propose une approche topologique visant à garantir un fonctionnement minimal optimal de ces réseaux, crucial pour la mobilité des passagers affectés. Dans un premier temps, un modèle de vulnérabilité a été élaboré pour quantifier la vulnérabilité des routes empruntées par les passagers en cas de pannes. Ce modèle combine le nombre de chemins alternatifs et le flux de passagers sur les routes. L'intégration de ce modèle dans le processus de sélection des itinéraires a ensuite été testé sur le réseau routier de la ville de Sioux Falls. La prise en compte de ce modèle dans le processus de décision des routes à emprunter permet d'atténuer l'impact des perturbations du réseau sur le déplacement des passagers. Par la suite, nous avons axé notre recherche sur l'amélioration de la robustesse globale des réseaux de transport. L'approche adoptée consiste à apporter des ajustements structurels mineurs sur le réseau afin d'accroître au maximum le nombre de chemins alternatifs. Ces itinéraires de substitution offrent des solutions en cas de dysfonctionnement du réseau. Cette méthode a été appliquée au réseau aérien des vols à bas coûts en France métropolitaine. Enfin, le dernier levier d'optimisation du réseau de transport concerne les véhicules et est adressé en dernière partie de cette thèse. Elle se concentre sur le renforcement de la robustesse de la trajectoire de vol des avions face à des obstacles météorologiques imprévus. La méthode utilisée combine un algorithme de génération de trajectoires, un algorithme de classification et un processus de filtrage pour générer un ensemble de trajectoires alternatives dissimilaires. Les résultats montrent que l'amélioration topologique de la robustesse à tous les niveaux du réseau de transport permet de réduire effectivement les retards occasionnés par des perturbations imprévues sur le temps de trajet global des passagers du réseau
Vérification formelle de réseau de neurones quantizé
No full textInternational audienceNeural networks have become a crucial element in modern artificial intelligence. However, despite their advancements, they often act as black boxes and can produce unexpected and incorrect results. This is why it is important to formally verify the properties of neural networks. Our work focuses on using quantization as an optimization method to accelerate the verification process. We propose a verification method for a quantized neural network (QNN) based on rational approximation of the neural network and set-based theory. We evaluate our method using the iris and HIGHWAY-ENV benchmarks, with z3 as a Satisfiability modulo theories (SMT) solver.</div