Tri :
Date
Editeur
Auteur
Titre
|
|
Institut Supérieur de l'Aéronautique et de l'Espace
/ 12-09-2022
Thomas Ludovic
Voir le résumé
Voir le résumé
Les réseaux temps-réels, comme ceux spécifiés par IEEE Time-Sensitive Networking (TSN) et IETF Deterministic Networking (DetNet), fournissent aux applications critiques un service déterministe avec des bornes de latence garanties.Plusieurs mécanismes comme les ordonnanceurs et les régulateurs de trafic (TSN ATS, asynchronous traffic shaping) ont été développés et leurs effets sur les bornes de latences pire-cas ont été abondamment étudiés dans la littérature en utilisant la théorie du calcul réseau.Toutefois, les réseaux temps-réels doivent désormais aussi offrir une reconfiguration simplifiée avec des chemins alternatifs, un haut niveau de fiabilité et parfois un service de synchronisation du temps.Pour répondre à ces besoins, l'utilisation de topologies à plusieurs chemins a été encouragée pour faciliter la reconfiguration et des mécanismes de redondance et de synchronisation ont été développés pour fournir un haut niveau de fiabilité et une synchronisation du temps.Tandis que chacun de ces mécanismes dispose d'une théorie pour valider son efficacité dans son objectif respectif, la littérature n'a que peu étudié leurs effets secondaires sur les bornes de latences et leurs interactions avec les ordonnanceurs et les régulateurs de trafic.Dans cette thèse, nous utilisons la théorie du calcul réseau pour analyser les combinaisons de mécanismes et leurs effets sur les bornes de latences dans les réseaux temps-réel avec des topologies à plusieurs chemins.Nos principales contributions sur le plan théorique sont :1/ Nous développons un algorithme (FP-TFA) qui calcule des bornes de latence dans les réseaux dans lesquels la variété des chemins crée des dépendances cycliques.Nous proposons et analysons l'approche de déploiement partielle des régulateurs de trafic (soit par flux, soit avec TSN ATS) ainsi qu'un autre algorithme (LCAN) qui casse toutes les dépendances cycliques à coût minimal.2/ Nous analysons les effets des mécanismes de redondance sur les bornes de latence en modélisant leur comportement dans la théorie du calcul réseau.Nous analysons aussi leurs interactions avec les régulateurs de trafic.En particulier, nous observons que TSN ATS peut mener à des latences non bornées lorsqu'il est utilisé avec les mécanismes de redondances.3/ Nous proposons un modèle d'horloge qui décrit, au sein de la théorie du calcul réseau, les imperfections des horloges des réseaux synchronisés ou non.Nous montrons que l'usage de régulateurs de trafic avec des horloges imparfaites occasionne une pénalité dans les bornes de latence.Avec TSN ATS, cette pénalité n'est pas bornée, y compris dans les réseaux synchronisés avec une grande précision.Nous proposons deux méthodes (cascade et ADAM) pour adapter les paramètres des régulateurs et ainsi résoudre ce problème.Nous fournissons également des contributions d'intérêt pratique :a) l'outil modulaire xTFA, qui calcule des bornes de latences en utilisant les résultats de la thèse,b) un module pour simuler l'effet des horloges locales dans le simulateur à évènements discrets ns-3, etc) une application de nos résultats sur une étude de cas industrielle.
|
Texte intégral
|
|
Institut Supérieur de l'Aéronautique et de l'Espace
/ 26-08-2022
Scotto di perrotolo Alexandre
Voir le résumé
Voir le résumé
Les méthodes aléatoires pour le calcul approché de décomposition aux valeur singulières/valeurs propres ont suscité beaucoup d’intérêt au cours des dernières décennies. Ces méthodes se sont avérées performantes, efficaces en termes de coût de calcul et particulièrement bien adaptées aux problèmes de grande taille. À cet égard, des recherches récentes ont proposé des applications de cesméthodes en assimilation de données, où la taille des problèmes est prohibitive pour un grand nombre d'approches classiques. Dans cette thèse, nous proposons trois contributions interconnectées aux méthodes aléatoires pour l'approximation de rang faible, l'extraction d’information spectrale et le préconditionnement en assimilation de données variationnelle.Premièrement, nous proposons une analyse générale de l'erreur d'approximation de rang faible aléatoire en norme de Frobenius et en norme spectrale. Cette généralisation étend les possibilités d'analyse à un plus grand nombre de méthodes aléatoires en autorisant des matrices de covariance générales et un vecteur de moyenne non nulle pour la matrice gaussienne d'échantillonnage. La particularisation de nos bornes à la méthode dite de Randomized Singular Value Decomposition (RSVD) montre que nous améliorons les bornes d'erreur de référence proposées par Halko, Martinsson et Tropp (2011).Ensuite, nous présentons des algorithmes aléatoires pour la résolution de problèmes aux valeurs propres spécifiques qui apparaissent notamment en assimilation de données. Les méthodes proposées sont polyvalentes et généralisent les contributions de Saibaba, Lee et Kitanidis (2016) et Daužickaité et al. (2021). Nous fournissons ensuite une analyse théorique de nos méthodes qui éclaire sur la sensibilité de l’erreur au nombre d'itérations de sous-espace, au nombre d'échantillons aléatoires et à la matrice de covariance pour la matrice gaussienne d'échantillonnage. Des illustrations numériques sur un problème d'assimilation de données confirment le potentiel de nos algorithmes.Enfin, nous proposons une classe de préconditionnement à mémoire limitée aléatoire dédiée à l'assimilation de données variationnelle. Nous proposons de tels préconditionnements pour deux méthodes de Krylov en particulier: une approche dite inverse-free dans l'espace primal introduite par Guröl (2013) et une méthode d'espace dual proposée par Gratton et Tshimanga (2009). La dimension réduite de l'espace dual rend cette dernière approche plus intéressante à la fois en termes de coût de calcul et de stockage. Les préconditionnements aléatoires proposés sont basés sur des expressions adaptées identifiées par Gürol (2013) pour lesquelles les calculs coûteux d’information spectrale exacte est remplacée par des approximations obtenues avec une procédure aléatoire. Des illustrations sur un problème d'assimilation de données variationnel quadridimensionnel de référence démontrent le potentiel de nos préconditionnements aléatoires, ouvrant ainsi des perspectives intéressantes.
|
Texte intégral
|
|
Institut Supérieur de l'Aéronautique et de l'Espace
/ 21-06-2022
Chaine Pierre-Julien
Voir le résumé
Voir le résumé
L’industrie aérospatiale fait face à un nouveau défi : proposer de nouvelles fonctionnalités et de nouvelles missions autour de la Terre, dans le système Solaire et au-delà. Ces nouveautés ne se feront pas sans une amélioration de la performance à bord des satellites, notamment au niveau de l'architecture de communication. C’est la raison pour laquelle l’industrie aérospatiale envisage un changement radical de ses réseaux embarqués, passant du bus MIL-STD-1553 pour le trafic temps réel et Spacewire pour le trafic haut débit, à un réseau «unifié » reposant sur une technologie unique capable de transporter ces deux types de trafic. Au début de la thèse, IEEE Time Sensitive Networking (TSN), la technologie état de l’art d’Ethernet, a commencé à attirer l’attention de différents acteurs du spatial. De fait, le but de cette thèse a été de mettre en évidence l’adéquation de TSN avec les exigences de l’industrie aérospatiale.Afin de résoudre ce problème, nous avons commencé par identifier un ensemble de technologies – Ethernet, ARINC 664, TTEthernet, Time Sensitive Networking et Spacefibre – a priori capables de répondre aux besoins des futures missions. Nous avons ensuite proposé une comparaison qualitative de ces technologies en se basant sur leur compatibilité avec les futures exigences des satellites. Cette comparaison s’est organisée autour de deux thèmes : qualité de service (i.e. performance réseau et tolérance aux fautes) et gestion du temps. Elle nous amènera à sélectionner trois candidats : TTEthernet, Spacefibre et TSN. Tandis que TTEthernet et Spacefibre étaient déjà connus et commençaient même à être intégrés dans des architectures réseaux embarqués satellite au moment d’écrire ce document, Time Sensitive Networking était lui totalement nouveau pour l’industrie aérospatiale.Ainsi, après cette étape préliminaire, nous avons étudié en profondeur les très nombreux standards de TSN. Nous avons identifié IEEE 802.1Qbv dit Time Aware Shaper comme le standard TSN indispensable pour répondre aux exigences en performance réseau des futurs satellites. Nous avons par ailleurs discuté de l’intérêt d’autres standards TSN (i.e. IEEE 802.1Qci, 802.1CB, 802.1AS, 802.1Qbu) qui sont, avec Qbv, en voie d’être inclus dans un profil TSN dédié à l’industrie aérospatiale.Afin de valider la compatibilité de TSN, nous nous sommes intéressés à la génération de configurations TSN. Cette tâche n’est pas aisée car chaque configuration nécessite d’instancier un très grand nombre de paramètres. De fait, ces configurations sont presque toujours générées de manière automatique. Cette automatisation est un véritable levier dans l’industrialisation du TSN, à la fois dans les satellites, et d’autres domaines d’application. Ainsi, nous nous sommes concentrés sur la configuration automatique du standard Qbv afin d’adresser les besoins en performance, considérant que les fonctions de tolérances aux fautes pouvaient être reléguées au niveau applicatif. Alors que les stratégies automatiques reposant sur des émissions planifiées à date fixe dans tous les équipements du réseau étaient très répandues dans l’état de l’art, nous avons proposé une nouvelle stratégie de configuration intitulée Egress TT. En pratique, les configurations Egress TT reposent sur des émissions planifiées à date fixe seulement dans le dernier équipement du trajet de n’importe quel flot. Le délai d’un message entre sa source et le dernier équipement dans son trajet peut être variable. En effet, il dépend de l’instant auquel le message a été émis à sa source et aux potentiels ralentissements qu’il rencontrerait dans le réseau. Néanmoins, ce délai variable est absorbé par une planification des émissions bien choisie au dernier saut. Cette nouvelle stratégie propose un meilleur passage à l’échelle que les stratégies existantes. Elle permet aussi de réduire l’effort de développement nécessaire pour la mise à jour des logiciels applicatifs vers l’architecture réseau nouvelle génération.
|
Texte intégral
|
|
Institut Supérieur de l'Aéronautique et de l'Espace
/ 14-06-2022
Mounsif Leila
Voir le résumé
Voir le résumé
La transmission Faster-than-Nyquist (FTN) monoporteuse consiste à transmettre avec un rythme symbole supérieur à la bande occupée par le signal émis. Cette stratégie s’est révélée pertinente pour accroître l’efficacité spectrale atteignable sur des canaux contraints en puissance et pour rendre le signal de communication difficile à identifier pour un éventuel noeud espion. Alors que de très nombreuses contributions se sont focalisées sur la détection symbole (ou séquence) en présence d’interférence entre impulsions de mise en forme, nous nous intéressons à la synchronisation, peu étudiée pour ce mode de transmission mais essentielle pour pouvoir envisager des récepteurs pratiques. L’objet principal de ces travaux de thèse est la conception de séquences pilotes adaptées à la synchronisation du délai et de la phase en FTN, au sens de la minimisation de la borne de Cramér–Rao (CRB) des paramètres, en fonction de la densité de transmission. À travers une étude analytique de la CRB du délai, nous révélons qu’une séquence optimale pour l’estimation de ce paramètre pour un système de Nyquist est non-informative pour les systèmes FTN, dans le cas d’un filtre de mise en forme réel de type root-raised cosine. Les courbes de CRB des paramètres obtenues sont comparées à des estimateurs basés sur le maximum de vraisemblance, asymptotiquement efficaces. Des études complémentaires à ces travaux pourraient inclure une évaluation de la robustesse des estimateurs basés sur le maximum de vraisemblance à une contamination des symboles pilotes par des symboles de données. Aussi, il serait pertinent de prévoir une étape préliminaire de synchronisation du décalage en fréquence.
|
Texte intégral
|
|
Institut Supérieur de l'Aéronautique et de l'Espace
/ 19-05-2022
Taleb Khaled
Voir le résumé
Voir le résumé
Dans cette thèse, nous examinons le canal wiretap de Wyner dans la pratique, pour atteindre la sécurité en terme de théorie de l'information. Ce type d'approche de la sécurité a longtemps été écarté des applications pratiques. Ceci est principalement dû à une définition légèrement différente de la sécurité (Sécurité forte vs sécurité sémantique), en plus du fait que ces méthodes sont étudiées de manière asymptotique, donc pas en pratique. Les spécialistes ont donc préféré des solutions cryptographiques sur les couches supérieures du réseau afin d'assurer la sécurité. Cependant, il a été montré que ces définitions de la sécurité sont en fait équivalentes les unes aux autres. De plus, nous montrons que le comportement asymptotique des codes polaires, utilisés sur un canal wiretap, appelés codes polaires wiretap, est compatible avec son comportement asymptotique, ce qui rend les codes polaires wiretap utiles pour des applications pratiques. Un autre avantage principal de l'utilisation de la sécurité de la couche physique est que les types de réseaux émergents tels que les réseaux de capteurs, les réseaux ad hoc qui passent par plusieurs intermédiaires de la source à la destination, ou les réseaux d'identification par radiofréquence (RFID), sont de faible complexité, sur lesquels la gestion des clés cryptographiques, ainsi que la complexité de calcul rendent l'utilisation des techniques cryptographiques typiques difficile. Nous nous appuyons principalement sur les schémas présentés par Vardy et al. pour obtenir un secret faible et fort. Étant donné que nous utilisons ces schémas dans des longueurs de bloc finies, des fuites d'informations peuvent se produire. Il existe des méthodes dans la littérature pour calculer et estimer cette fuite d'information, mais nous montrons comment ces méthodes sont soit infaisables en pratique, soit simplement inexactes. De plus, nous introduisons une nouvelle méthode, pour estimer cette fuite, qui s'avère être très précise et plus légère en calcul que les méthodes connues. D'autre part, nous étudions également la construction pratique de codes polaires wiretap à longueur de bloc finie et examinons l'impact des principaux paramètres de construction sur le taux de code réalisable et la fuite d'information. Enfin, nous présentons notre banc d'essai, utilisé pour mettre en œuvre les codes polaires wiretap en pratique, en utilisant un émetteur et deux récepteurs, simulant le récepteur légitime et l'espion. Nous montrons que plus l'espion est éloigné de l'émetteur, plus il y a de bruit, et donc une moins bonne capacité de décodage, et qu'au-delà d'une certaine distance, il est incapable de décoder quoi que ce soit, et reçoit une image très bruyante, de laquelle aucune information utile ne peut être extraite.
|
Texte intégral
|
|
Institut Supérieur de l'Aéronautique et de l'Espace
/ 01-04-2022
Xu Zhujun
Voir le résumé
Voir le résumé
L'objectif de ce travail de thèse est de développer des méthodes de détection et de suivi d'objets 2D et 3D fondés sur l'apprentissage profond sur vidéo monoculaire et de les appliquer au contexte du véhicule autonome. En effet, lorsque l’on utilise directement des détecteurs d'images fixes pour traiter un flux vidéo, la précision souffre d'un problème de qualité d'image du fait de l’échantillonnage. De plus, les annotations 3d des vidéos prennent du temps et sont coûteuses en raison du grand nombre d'images. Nous profitons donc des informations temporelles dans les vidéos, telle que la cohérence des objets, pour améliorer les performances. Les méthodes ne doivent pas introduire trop de charge de calcul supplémentaire, car le véhicule autonome exige une performance en temps réel.Plusieurs méthodes peuvent être utilisées dans différentes étapes, par exemple, la préparation des données, l'architecture du réseau et le post-traitement. Tout d'abord, nous proposons une méthode de post-traitement appelée heatmap propagation (propagation de carte de chaleur) fondée sur un one-stage détecteur CenterNet pour la détection d'objets dans les vidéos. Notre méthode propage la détection fiable effectuée sur les images précédentes sous la forme d’une heatmap pour la prochaine image. Ensuite, pour distinguer différents objets d'une même classe, nous proposons une architecture de réseau image par image pour la segmentation d'instances vidéo en utilisant les instance sequence queries (requête de séquence d’instances) . Le suivi des instances est réalisé sans post-traitement supplémentaire pour l'association de données. Enfin, nous proposons une méthode d'apprentissage semi-supervisée pour générer des annotations 3D pour une base de données de suivi d'objets dans les vidéos 2D. Cela permet d'enrichir le processus d'apprentissage pour la détection d'objets 3D. Chacune des trois méthodes peut être appliquée individuellement pour étendre les détecteurs d'images dans le cadre d’applications sur vidéo. Nous proposons également deux structures de réseau complètes pour résoudre la détection et le suivi d'objets 2D et 3D sur vidéo monoculaire.
|
Texte intégral
|
|
Institut Supérieur de l'Aéronautique et de l'Espace, Macquarie University (Sydney, Australie)
/ 17-03-2022
Dehez Clementi Marina
Voir le résumé
Voir le résumé
En 2016, le nombre de décès dus aux accidents de la route atteignait 1,35 million, et ces accidents sont souvent imputable à l’erreur humaine. L'expansion technologique d'Internet et des réseaux interconnectés facilitent l'échange d'informations, parfois vitales. C'est pourquoi beaucoup de travaux ont été produit sur l'automatisation des véhicules. L’amélioration de la sécurité routière est l'un des facteurs qui motive la recherche dans ce domaine et pousse vers l’adoption de systèmes de transport intelligents (ITS) et de réseaux véhiculaires ad hoc (VANET).Un VANET est défini comme un réseau ad-hoc particulier, formé de véhicules capables de communiquer et de traiter l’information reçue, et évoluent en milieu urbain (rues ou autoroutes). Les véhicules peuvent communiquer directement, de pair à pair, ou via un nœud intermédiaire.L'objectif principal de la sécurité des VANETs et des communications véhiculaires est de fournir l'intégrité des messages échangés et la disponibilité des services qui supportent ces échanges. La protection de la confidentialité de ce qu'ils contiennent est un objectif secondaire car non vital. Assurer la responsabilité, c'est-à-dire proposer un moyen d'identifier les entités communicantes et de les tenir responsables pour les messages qu’ils diffusent, est essentiel voire légalement obligatoire. Ce mécanisme doit garantir que tout nœud qui subit une faute, panne ou agit de façon malveillante, soit identifié, révoqué, finalement puni pour ses actions et leurs conséquences. Cependant, un tel mécanisme d'identification pose un problème et risque de compromettre la vie privée des utilisateurs, même lorsqu'ils sont honnêtes.Cette thèse porte sur le délicat compromis entre anonymat et traçabilité dans systèmes distribués tels que les ITSs. Nous étudions l'utilisation des blockchains (chaînes de blocs) dans la construction de primitives cryptographiques à seuil. Ces primitives sont utilisées afin de préserver la vie privée mais aussi la responsabilité des acteurs et étudiées dans leur application au cas des VANETs.Notre première contribution, appelée DOGS, est un schéma de signature de groupe basé sur la blockchain qui propose la fonctionnalité d'ouverture distribuée. Nous montrons, dans cette thèse, que le système améliore un schéma de signature de groupe existant et exploite un protocole de génération de clé distribuée pour répartir le rôle de l'ouvreur (Opener) sur un ensemble de nœuds appelés les sous-ouvreurs (sub-openers).Notre deuxième contribution est une génération de clé distribuée anonyme mais traçable, appelé BAT-Key, qui utilise une blockchain pour assurer la confiance entre les différentes entités qui composent le système. Dans la suite de la thèse, nous expliquons comment nous avons amélioré les protocoles traditionnels avec la propriété d'anonymat qui protège l'identité des participants.Notre troisième contribution, appelée TOAD, est un schéma de chiffrement à seuil basé sur la blockchain avec un service de déchiffrement anonyme mais traçable. Nous montrons que le schéma s'appuie sur un schéma de chiffrement à seuil connu et l’améliore par un processus de déchiffrement collaboratif qui protège l'identité des serveurs de déchiffrement.Tout au long des chapitres, nous expliquons comment l'utilisation de la blockchain garantit la traçabilité des actions effectuées au sein du système par des nœuds anonymes et assure ainsi leur responsabilité tout en préservant la vie privée.Ces schémas sont de la plus haute importance dans l'ère du numérique, même en dehors du domaine des ITSs. Pourtant, nous avons choisi d'illustrer leur importance dans le contexte des VANETs à travers notre dernière contribution : la description de notre construction d'un système de rapport de trafic routier basé sur la blockchain qui préserve l’anonymat des nœuds qui rapportent les informations, mais les tient pour responsables de leurs messages en cas de litige.
|
Texte intégral
|
|
Institut Supérieur de l'Aéronautique et de l'Espace
/ 16-03-2022
El Masri Maxime
Voir le résumé
Voir le résumé
De nombreuses disciplines scientifiques s’intéressent à l’estimation d’espérances d’une fonction d’intérêt selon une certaine loi de probabilité. Cette fonction peut être considérée comme une boite noire, potentiellement couteuse à évaluer. Une méthode couramment utilisée pour estimer des espérances, tout en limitant le nombre d’appels à la boite noire, est la méthode stochastique d’échantillonnage préférentiel (Importance Sampling, IS) qui consiste à échantillonner selon une loi de probabilité auxiliaire au lieu de la loi initiale. L’estimateur d’IS est défini à partir de l’estimateur de Monte-Carlo, avec des poids d’importance, et converge presque sûrement vers l’espérance voulue, par la loi des grands nombres. Cependant, sa variance, et donc la précision de l’estimation, dépend fortement du choix de la densité auxiliaire. Une densité optimale d’échantillonnage préférentiel minimisant la variance peut être définie sur le plan théorique mais n’est pas connue en pratique. Une possibilité est alors de choisir la densité auxiliaire dans une famille paramétrique, avec la-quelle il est facile de générer des échantillons, afin d’approcher la distribution optimale théorique. Des algorithmes adaptatifs (Adaptive Importance Sampling, AIS), qui estiment les paramètres de manière itérative, ont été développés pour trouver les paramètres optimaux permettant d’approcher la densité théorique visée. Mais lorsque la dimension de l’espace des paramètres augmente, l’estimation des paramètres se dégrade et les algorithmes d’AIS, et l’IS en général, deviennent inefficaces. L’estimation finale de l’espérance devient alors très imprécise, notamment du fait de l’accumulation des erreurs commises dans l’estimation de chaque paramètre. L’objectif principal de cette thèse est ainsi d’améliorer la précision de l’IS en grande dimension, en réduisant le nombre de paramètres estimés à l’aide de projections dans un sous-espace de petite dimension. Nous nous concentrons particulièrement sur la recherche de directions de projection influentes pour l’estimation de la matrice de covariance dans un cadre gaussien unimodal (où l’on met à jour le vecteur moyenne et la covariance). La première piste explorée est la projection sur le sous-espace de dimension un engendré par la moyenne optimale. Cette direction est particulièrement pertinente dans le cas d’estimation d’une probabilité d’événement rare, car la variance semble diminuer selon cette direction. La seconde proposition correspond à la projection optimale obtenue en minimisant la divergence de Kullback-Leibler avec la densité visée. Cette seconde proposition permet de projeter dans un espace de plusieurs dimensions contrairement à la première, et permet d’identifier les directions les plus influentes. Dans un premier temps, l’efficacité de ces projections est testée sur différents exemples d’estimation d’espérances en grande dimension, dans un cadre théorique n’impliquant pas d’algorithmes adaptatifs. Les simulations numériques réalisées montrent une nette amélioration de la précision de l’estimation par IS avec les deux techniques de projection sur tous les exemples considérés. Ensuite, nous proposons un couplage de ces projections avec l’algorithme d’Entropie Croisée (Cross Entropy, CE), un algorithme d’AIS destiné à l’estimation de probabilités d’événements rares. L’efficacité de ces algorithmes est vérifiée sur plusieurs cas-tests avec un faible budget de simulation. La technique basée sur la projection dans les directions optimales permet d’obtenir des estimations très précises pour des dimensions modérément grandes (plusieurs dizaines). Le couplage avec la projection sur la moyenne reste en revanche performante dans des dimensions de quelques centaines dans la plupart des exemples. Dans tous les cas, les simulations montrent que les méthodes proposées sont plus précises que la CE classique en grande dimension avec un même budget.
|
Texte intégral
|
|
Institut Supérieur de l'Aéronautique et de l'Espace
/ 15-02-2022
Rakotomalala Lucien
Voir le résumé
Voir le résumé
De nos jours les avions ne peuvent se passer d'un important réseau embarqué pour faire communiquer les nombreux capteurs et actionneurs qui y sont disséminés. Ces réseaux ayant une fonction critique, en particulier pour les commandes de vol, il est important d'en garantir certaines propriétés telles des délais de traversée ou l'absence de débordement de buffers. Le calcul réseau est une méthode mathématique permettant de réaliser de telles preuves [2]. Elle a joué un rôle clef dans la certification du réseau AFDX, dérivé de l'ethernet, utilisé à bord des avions les plus récents (A380, A350).Le Calcul Réseau se base sur des résultats mathématiques utilisant l'algèbre tropicale. Ces résultats sont relativement simple mais déjà bien assez subtiles pour qu'il soit très facile de commettre des erreurs ou des omissions lors de preuves papier ou de calcul de valeur concrètes. Par ailleurs, les assistants de preuve sont un bon outil pour réaliser une vérification mécanique de ce genre de preuves et obtenir un très haut niveau de confiance dans leurs résultats. Nous formalisons donc avec un tel outil les notions et propriétés fondamentales de la théorie du Calcul Réseau. Ces résultats font intervenir des propriétés sur les nombres réels, tel que des bornes supérieures et des limites de fonctions linéaires donc nous souhaitons utiliser un outil de formalisation capable d'implémenter untel niveau mathématique. Nous utilisons l'assistant de preuve Coq. Il s'agit d'un outil disposant déjà d'un long développement dont la librairie Mathematical Components qui permet de formaliser de l'analyse sur les nombres réels et la construction de structures algébriques comme celles utilisées dans le Calcul Réseau. Le calcul de valeurs effective repose sur des opérations de l'algèbre min-plus sur des fonctions réelles. Des algorithmes sur des sous-ensembles spécifiques peuvent être trouvés dans la littérature [3]. De tels algorithmes et leurs implémentations sont toutefois compliqués. Plutôt que de développer une preuve de la bonne implémentation de ces algorithmes, nous prenons une implémentation existante comme Oracle et nous donnons des critères de vérifications en Coq.[1] Anne Bouillard, Marc Boyer et Euriell Le Corronc. DeterministicNetwork Calculus : From Theory to Practical Implementation. John Wiley& Sons, Ltd, oct. 2018[2] Assia Mahboubi et Enrico Tassi. Mathematical Components. Zenodo,jan. 2021[3] Anne Bouillard et Eric Thierry. « An Algorithmic Toolbox forNetwork Calculus ». In : Discret. Event Dyn. Syst. 18.1 (2008),p. 3-49.
|
Texte intégral
|
|
Institut Supérieur de l'Aéronautique et de l'Espace
/ 03-02-2022
Fabozzi Fabio
Voir le résumé
Voir le résumé
Dans cette thèse de doctorat, nous nous intéressons à l'estimation robuste de la phase de la porteuse en utilisant le filtrage bayésien variationnel. La mesure de la phase porteuse est devenue une tâche fondamentale dans de nombreuses applications d'ingénierie telles que le positionnement précis dans le domaine du GNSS. Malheureusement, les mesures de phase obtenues par les techniques traditionnelles de poursuite de phase peuvent être fortement mises à mal par la présence de sauts de phase ambigus, appelés sauts de cycle. Ces derniers peuvent durement impacter les performances des algorithmes de poursuite conduisant, dans le pire des cas, à une perte permanente de verrouillage du signal. Un processus de ré-acquisition est alors nécessaire qui affecte les performances de suivi. Par conséquent, pour résoudre ce problème, nous proposons un filtre non linéaire robuste de poursuite de phase basé sur l'inférence de Bayes variationnelle. Tout d'abord, l'algorithme est développé en supposant une dynamique lente de phase (c'est-à-dire la boucle au premier ordre), puis, son ordre est augmenté en estimant un vecteur d'état formé par la phase et ses dérivées. Les performances de ce nouvel algorithme sont comparées avec celles de techniques conventionnelles (tels que la DPLL (Digital Phase Lock Loop) et la KF (Kalman Filter)-DPLL) en terms de précision d'estimation et d'occurence de sauts de cycle. La comparaison est d'abord effectuée à l'aide de données synthétiques, puis de données GNSS réelles dans un récepteur radio logicielle GNSS. Les résultats montrent que la méthode proposée a de meilleures performances par rapport aux filtres linéaires conventionnels, lorsque le rapport signal sur bruit est faible.
|
Texte intégral
|
|