La blockchain est un registre distribué et décentralisé, permettant de stocker et d’échanger des informations de façon sécurisée, sans tiers de confiance. Pour cela,les informations, appelées transactions, sont regroupées au sein de blocs, qui sont ensuite liés entre eux de façon immuable grâce à des procédés cryptographiques. Le registre sert d’historique de toutes les actions menées par les participants du réseau depuis sa création.C’est une technologie en plein essor, de plus en plus utilisée au quotidien. Cet engouement croissant entraîne une explosion du nombre de transactions, ayant pour conséquence directe une forte augmentation de la taille des principales blockchains.Celles-ci deviennent donc plus compliquées à stocker dans leur intégralité, ce qui peut décourager certains nœuds de stocker toute la blockchain et ainsi réduire le niveau de décentralisation.Dans cette thèse, nous proposons un nouveau type de nœud, appelé low storage(LS) node, qui ne stocke plus les blocs en entier, mais des fragments de ceux-ci codés avec un code à effacement. Pour retrouver le bloc initial, un nœud LS commence par télécharger suffisamment de fragments codés depuis d’autres nœuds LS du réseau,puis procède au décodage.L’intérêt de cette approche est qu’elle permet à certains nœuds de stocker une version codée moins volumineuse de la blockchain tout en contribuant à la décentralisation de la blockchain. Elle facilite ainsi le passage à l’échelle des blockchains qui pose actuellement problème.Ce manuscrit présente également BlockHouse, un système complet permettant la location d’espace de stockage libre entre particuliers. La principale innovation est l’utilisation de contrats intelligents (smart contracts) déployés sur la blockchain qui permettent des paiements automatiques et sécurisés basés sur des preuves de récupérabilité des données régulièrement fournies par les serveurs de stockage.

De nos jours, la conception avant-projet en aéronautique repose majoritairement sur des modèles numériques faisant interagir de nombreuses disciplines visant à évaluer les performances de l’avion. Ces disciplines, comme l’aérodynamique, la structure et la propulsion, sont connectées entre elles afin de prendre en compte leurs interactions. Cela produit un processus d’évaluation des performances de l’avion coûteux en temps de calcul. En effet, une évaluation peut prendre de trente secondes pour les modèles de basse fidélité jusqu’à plusieurs semaines pour les modèles de plus haute fidélité. De plus, à cause de la multi-disciplinarité du processus et de la diversité des outils de calcul, nous n’avons généralement pas accès aux propriétés ou au gradient de cette fonction de performance. En outre, chaque discipline utilise ses propres variables de conception et doit respecter des contraintes d’égalité ou d’inégalité qui sont souvent nombreuses et multimodales. On cherche finalement à trouver la meilleur configuration possible dans un espace de conception donné. Cette recherche peut se traduire mathématiquement par un problème d’optimisation boite noire sous contraintes d’inégalité et d’égalité, aussi connues comme contraintes mixtes, dépendant d’un grand nombre de variables de conception. De plus, les contraintes et la fonction objective sont coûteuses à évaluer et leur régularité n’est pas connue. C’est pourquoi, on s’intéresse aux méthodes d’optimisations sans dérivées et particulièrement celles reposant sur les modèles de substitution. Les méthodes d’optimisation Bayésienne, utilisant des processus gaussiens, sont notamment étudiées car elles ont montré des convergences rapides sur des problèmes multimodaux. En effet, l’utilisation d’algorithmes d’optimisation évolutionnaire ou reposant sur le gradient n’est pas envisageable du fait du coût de calcul que cela implique : trop d’appels pour générer des populations de points, ou pour approcher le gradient par différences finies. Cependant la méthode d’optimisation Bayésienne est classiquement utilisée pour des problèmes d’optimisation sans contrainte et de faible dimension. Des extensions ont été proposées pour prendre en compte ce verrou de manière partielle. D’une part, des méthodes d’optimisation ont été introduites pour résoudre des problèmes d’optimisation à contraintes mixtes. Toutefois, aucune d’entre elles n’est adaptable à la grande dimension, aux problèmes multi-modaux et aux contraintes mixtes. D’autre part, des méthodes d’optimisation ont été développées pour la grande dimension pouvant aller jusqu’aumillion de variables de conception. De même, ces méthodes ne s’étendent que difficilement aux problèmes contraints à cause du temps de calcul qu’ils nécessitent ou de leur caractère aléatoire. Une première partie de ce travail repose sur le développement d’un algorithme d’optimisation Bayésienne résolvant les problèmes d’optimisation sans contrainte en grande dimension. Il repose sur une stratégie d’apprentissage adaptatif d’un sous-espace linéaire réalisée conjointement à l’optimisation. Ce sous-espace linéaire est ensuite utilisé pour réaliser l’optimisation. Cette méthode a été testée sur des cas tests académiques. Une deuxième partie de ce travail traite du développement d’un algorithme d’optimisation Bayésienne pour résoudre les problèmes d’optimisation multi-modaux sous contraintes mixtes. Il a été comparé aux algorithmes de la littérature de manière intensive sur une grande batterie de tests académiques. Finalement, on a confronté le second algorithme à deux cas tests aéronautiques. Le premier cas test est une configuration classique d’avion moyen-courrier à propulsion hybride électrique développé par l’ONERA et l’ISAE-SUPAERO. Le second cas test est une configuration classique d’avion d’affaire développée par Bombardier Aviation. Ce cas test repose sur une optimisation à deux niveaux de fidélité. Un niveau de fidélité conceptuel et un niveau de fidélité préliminaire pour lesquels le problème est respectivement évalué en trente secondes et 25 minutes. Cette dernière étude a été réalisée lors d’une mobilité internationale chez Bombardier Aviation à Montréal (CA). Les résultats ont montré l’intérêt de la méthode mise en place

Cette thèse étudie le problème de planification de vol et de la maintenance des avions militaires. D’abord, nous étudions la complexité de ce problème d’optimisation. Puis, nous proposons un modèle de programmation linéaire en nombres entiers (PLNE) pour le résoudre. Nous construisons un générateur d’instances et une heuristique pour générer des solutions initiales. Ensuite, nous appliquons l’Apprentissage Automatique pour améliorer la performance des modèles PLNE en utilisant des coupes valides générées à partir des conditions initiales et des coupes apprises à partir de la prédiction des caractéristiques de solutions optimales. Ces coupes sont appliquées à un nouveau modèle PLNE. Le résultat est une réduction du temps de résolution avec peu de pertes d’optimalité et de faisabilité par rapport aux méthodes matheuristiques alternatives. Finalement, nous présentons une nouvelle matheuristique pour résoudre efficacement des grandes instances. La méthode utilise une descente à voisinage variable qui combine la programmation dynamique (DP) et l’horizon glissant. La DP exploite une représentation en graphe de l’espace des solutions de chaque avion. Le résultat est des solutions rapides et presque optimales, et un passage à l’échelle efficace pour des instances de très grande taille.

La thèse est une étude d'approches probabilistes pour la modélisation et l'analyse de systèmes temps réel. L'objectif est de comprendre et d'améliorer le pessimisme qui existe dans l'analyse du système. Les systèmes temps réel doivent produire des résultats avec des contraintes de temps réelles. L'exécution des tâches dans le système est basée sur leur pire temps d'exécution. En pratique, il peut y avoir de nombreux temps d'exécution possibles inférieurs au pire des cas. Nous utilisons le temps d’exécution probabiliste dans le pire cas, qui est une distribution de probabilité dans le pire des cas, qui limite tous les temps d’exécution possibles. Nous nous approchons avec le modèle de chaîne de Markov à temps continu pour obtenir des probabilités de manquer une contrainte de synchronisation dans le monde réel. Nous étudions également les systèmes de criticité mixte (MC) car ceux-ci ont également tendance à faire face au pessimisme dans un souci de sécurité. Les systèmes MC consistent en des tâches d’importance ou de criticité ged différentes. Le système fonctionne sous différents modes de criticité dans lesquels l'exécution des tâches de criticité identique ou supérieure est assurée. Nous abordons d’abord les systèmes MC en utilisant la chaîne de Markov en temps discret pour obtenir la probabilité que le système entre dans des niveaux de criticité plus élevés. Nous observons certaines limites de nos approches et nous procédons à la modélisation des systèmes probabilistes MC à l'aide de modèles Graph. Nous remettons en question les approches existantes dans la littérature et fournissons les nôtres. Nous obtenons des calendriers pour les systèmes MC optimisés pour l'utilisation des ressources. Nous faisons également le premier pas vers la dépendance entre les tâches en raison de leur scheduling.

La performance des réseaux sans fil où les utilisateurs partagent l'air comme moyen de communication est fortement limitée par le phénomène d'interférence électromagnétique. En effet, deux utilisateurs proches qui communiquent sur la même fréquence verront leurs ondes interférer, ce qui peut entraîner la perte de l'information transmise. Ainsi, il est indispensable de mettre en place des protocoles d'accès visant à limiter l'interférence en choisissant de manière efficace les utilisateurs autorisés à émettre à chaque instant. D'un point de vue scientifique, il s'agit d'un problème difficile qui a attiré l'attention de la communauté en informatique et probabilités appliquées depuis plus de 30 ans. Récemment, une nouvelle classe de protocoles d'accès - appelés protocoles CSMA adaptatifs - a émergé, et semble très prometteuse : par exemple, il a été montré que ces nouveaux protocoles possèdent une propriété très attrayante de stabilité maximale. Le but de ce projet est d'approfondir la connaissance que l'on a des protocoles CSMA adaptatifs dits QB (pour l'anglais "Queue-Based") qui à ce jour est encore extrêmement limitée. Concernant ces protocoles, le but de ce projet est de prouver des résultats théoriques permettant de comprendre le compromis réalisable entre débit et délai. Modèle probabiliste - d'un point de vue technique, il s'agit d'étudier le modèle suivant: chaque utilisateur du réseau est représenté par le nœud d'un graphe G, appelé graphe d'interférence, et tel que deux voisins du graphe ne peuvent être actifs simultanément. Des paquets à transmettre arrivent à chaque nœud au cours du temps, et le but est de choisir quels nœuds sont actifs à un moment donné. Le protocole CSMA-QB répond à cette question de la manière suivante : lorsqu'un nœud est actif, il se désactive à taux constant et lorsqu'il est inactif et qu'aucun de ses voisins ne le bloquent, alors il s'active à un taux qui dépend du nombre de paquets en attente de transmission via une fonction ψ appelée fonction d'activation. Le but général de la thèse est de comprendre l'influence de la topologie de G et du choix de ψ sur la performance du protocole. Pour cela, il s'agira d'étudier le temps de mélange de la dynamique de Glauber ainsi qu'un phénomène classique en théorie des probabilités, appelé phénomène de moyennisation stochastique, qui permettent une compréhension fine du comportement dynamique du réseau.

Cette étude concerne l’utilisation de la logique du premier ordre et la logique temporelle linéaire pour la spécification et la vérification des systèmes dynamiques ayant des structures riches. Elle concerne l’étude de la correction de fonctionnement du protocole de recherche distribuée Chord. L’objectif est d’une part d’améliorer la spécification et la vérification des systèmes dans le langage formel Electrum qui est une extension dynamique du langage formel Alloy basé sur la logique du premier ordre temporelle linéaire.Pour ce faire, nous avons développé une couche syntaxique au-dessus d’Electrum. L’objectif de cette couche est de faciliter la spécification du comportement dans Electrum, pour ce faire, nous avons défini une syntaxe permettant de générer automatiquement une partie de la spécification du comportement. Par ailleurs cette couche permet également de réduire les erreurs de spécification en déchargeant les utilisateurs de la spécification de certaines tâches comportementales ardues et sujettes aux erreurs.D’autre part, l’objectif est d’analyser formellement la correction de la propriété fondamentale de vivacité du protocole Chord. Pour ce faire nous avons spécifié et vérifié le protocole Chord avec l’extension d’Electrum que nous avons développée, puis nous avons prouvé sa correction et montré les avantages de notre méthode d’analyse.

Les travaux menés dans cette thèse de doctorat s’inscrivent dans le cadre d’un effort plus large d’automatisation des systèmes de simulation industriels. Dans l’industrie aéronautique, et plus particulièrement au sein d’Airbus, l’application historique de la simulation est la formation des pilotes. Il existe aussi des utilisations plus récentes dans la conception de systèmes, ainsi que dans l’intégration de ces systèmes. Ces dernières utilisations exigent un très haut degré de représentativité, là où historiquement le plus important était le ressenti du pilote. Les systèmes sont aujourd’hui divisés en plusieurs sous-systèmes qui sont conçus, implémentés et validés indépendamment, afin de maintenir leur contrôle malgré l’augmentation de leurs complexités et la réduction des temps de mise sur le marché. Airbus maîtrise déjà la simulation de ces sous-systèmes, ainsi que leurs intégrations en simulation. Cette maîtrise est empirique, les spécialistes de la simulation reprennent l’ordonnancement d’intégrations précédentes, et l’adaptent à une nouvelle intégration. C’est un processus qui peut parfois être chronophage, et qui peut introduire des erreurs. Les tendances actuelles de l’industrie sont à la flexibilité des moyens de production, à l’intégration d’outils logistiques permettant le suivi, à l’utilisation d’outils de simulation en production, et à l’optimisation des ressources. Les produits sont de plus en plus souvent des itérations d’anciens produits améliorés, et les tests et simulations intégrés à leurs cycles de vie. Travailler de manière empirique dans une industrie qui nécessite de la flexibilité est une contrainte, et il est aujourd’hui important de facilement modifier des simulations. La problématique est donc de mettre en place des méthodes et outils permettant a priori de générer des ordonnancements de simulations représentatifs. Afin de répondre à ce problème, nous avons mis en place une méthode permettant de décrire les composants d’une simulation, la manière dont cette simulation pourra être exécutée, ainsi que des fonctions permettant de générer des ordonnancements. Par la suite, nous avons implémenté un outil afin d’automatiser la recherche d’ordonnancement, en se basant sur des heuristiques. Enfin nous avons testé et vérifié notre méthode et outils sur des cas d’études académiques et industriels.

Actuellement, le développement d’un logiciel de taille industriel repose généralement surdes tests ou des preuves unitaires pour garantir rigoureusement ses exigences. En outre, il adéjà été montré que l’utilisation combinée du test et de la preuve unitaires est plus efficaceque l’utilisation d’une seule de ces deux techniques. Néanmoins, un ingénieur en vérificationhésite encore à utiliser ces deux techniques conjointement, faute d’une notion de couverturecommune au test et à la preuve. Définir une telle notion est l’objet de cette thèse.En effet, nous introduisons une nouvelle couverture, appelée « couverture label-mutant ».Elle permet de représenter les critères de couverture structurelle habituels du test, comme lacouverture des instructions, la couverture des branches ou la couverture MC/DC et de décidersi le critère choisi est satisfait en utilisant une technique de vérification formelle, qu’elle soitpar test, par preuve ou par une combinaison des deux. Elle permet également de représenterles critères de couverture fonctionnelle. Nous introduisons aussi dans cette thèse une méthodereposant sur des outils automatiques de test et de preuve pour réduire l’effort de vérificationtout en satisfaisant le critère de couverture choisi. Cette méthode est mise en oeuvre au seinde la plateforme d’analyse de code C (Frama-C), fournissant ainsi à un ingénieur un moyenopérationnel pour contrôler et réaliser la vérification qu’il souhaite.

Dans la dernière partie, des simulations numériques sur le claquage micro-ondes et la formation de structures filamentaires de plasma sont conduites. Les effets de différents types d’approximations sur le modèle physique du plasma sont analysés. Puis, ces expériences numériques démontre la précision et l’efficacité, en terme de temps de calcul, de la méthode multi-échelle proposée. Enfin, on étudie les effets de chauffage du gaz sur la formation et l’entretien de structures filamentaires dans l’air à pression atmosphérique. Pour cela, le modèle micro-onde-plasma développé est couplé avec les équations de Navier-Stokes instationnaires pour les écoulements compressibles. Les simulations montrent des caractéristiques intéressantes de la dynamique de ces structures plasma pendant le processus de chauffage du gaz, qui sont en accord étroit avec les données expérimentales.

Dans cette thèse, nous nous intéressons à l’amélioration des performances numériques de la méthode Galerkin Discontinu en Domaine Temporel (GDDT), afin de valoriser son emploi industriel pour des problèmes de propagation d’ondes électromagnétiques. Pour ce faire, nous cherchons à réduire le nombre d’éléments des maillages utilisés en appliquant une stratégie de h-déraffinement/p-enrichissement. Dans un premier temps, nous montrons que si ce type de stratégie permet d’améliorer significativement l’efficacité numérique des résolutions dans un cadre conforme, son extension aux maillages non-conformes peut s’accompagner de contre-performances rédhibitoires limitant fortement leur intérêt pratique. Après avoir identifié que ces dernières sont causées par le traitement des termes de flux non-conformes, nous proposons une méthode originale de condensation afin de retrouver des performances avantageuses. Celleci se base sur une redéfinition des flux non-conformes à partir d’un opérateur de reconstruction de traces, permettant de recréer une conformité d’espaces, et d’un produit scalaire condensé, assurant un calcul approché efficace. La stabilité et la consistance du schéma GDDT ainsi défini sont établies sous certaines conditions portant sur ces deux quantités. Dans un deuxième temps, nous détaillons la construction des opérateurs de trace et des produits scalaires associés. Nous proposons alors des flux condensés pour plusieurs configurations non-conformes, et validons numériquement la convergence du schéma GDDT résultant. Puis, nous cherchons à concevoir un algorithme de h-déraffinement/p-enrichissement automatisé, dans le but de générer des maillages hp minimisant les coûts de calcul du schéma. Ce processus est traduit sous la forme d’un problème d’optimisation combinatoire sous plusieurs contraintes de natures très diverses. Nous présentons alors un algorithme de post-maillage basé sur un parcours efficace de l’arbre de recherche des configurations admissibles, associé à un processus de déraffinement hiérarchique. Enfin, nous mettons en œuvre la chaîne de calcul développée sur plusieurs cas-tests d’intérêt industriel, et évaluons son apport en termes de performances numériques.