L'augmentation de la demande d'énergie à bord des véhicules et les besoins en machines de traction pour les véhicules hybrides incite à étudier d'autres structures de machines que l'alternateur à griffes. Ici, une structure à double excitation parallèle innovante à été étudiée pour le besoin alternateur. L'introduction des aimants apporte un surplus considérable de puissance, ceci a été mis en évidence en comparant cette structure à une machine à pôles saillants bobinés classique, la puissance a été carrément doublée. Le cahier des charges (3,2 kW) pour cette étude a été atteint sans difficultés. Le principe de double excitation choisi permet le contrôle du flux, et donc du débit avec un simple pont redresseur à diodes. L'étude théorique et expérimentale a montré l'efficacité de la désexcitation par le courant rotor et sans risque de démagnétisation des aimants. La comparaison expérimentale et à iso-encombrement avec une structure à griffes à aimants interpolaires montre la suprématie de cette dernière, en puissance grâce à sa bobine d'excitation globale permettant plus d'ampères tours, et en rendement en faibles puissances grâce à son défluxage total et local. Néanmoins, pour les fortes puissances, la machine à double excitation, de part sa structure bidimensionnelle, ayant moins de pertes fer, à plus de rendement. Une étude plus poussée pourra montrer le positionnement de cette structure pour les applications moteur dans les véhicules hybrides. Une petite comparaison de performances avec la machine à griffes a montré que cette dernière n'est pas automatiquement la meilleure.

L'objectif de ce travail est de fournir des modèles et outils pour simplifier la construction des systèmes distribués à base de composants sécurisés, ainsi que la gestion des propriétés de sécurité, en utilisant des outils de haut niveau d'abstraction pour la configuration et la reconfiguration dynamique. En plus des propriétés d'accessibilité et de communications sécurisées classiques, nous focalisons notre travail sur une propriété des systèmes répartis plus générale : la non-interférence. Cette propriété atteste qu'il ne doit pas y avoir de flux d'information entre des parties publiques et privées du système. Ce qui implique le suivi de l'acheminement de l'information entre les différentes composantes du système distribué. Notre objectif principal est donc de proposer un modèle, accompagné d'un ensemble d'outils, garantissant la propriété de la non-interférence à la construction du système, et ce à une plus grosse granularité : celle des composants. Ces outils permettent de (1) configurer les paramètres de sécurité des composants et des liaisons entre eux, (2) vérifier la propriété de non-interférence dans le code d'un composant et entre les différents composants du système et (3) générer automatiquement le code nécessaire pour appliquer ces propriétés de sécurité. D'autre part, nous proposons une architecture permettant de vérifier dynamiquement la propriété de non-interférence dans un système réparti.

Nous cherchons à améliorer l'état de l'art des implémentations de contrôle de flux d'information dans les systèmes Linux. Le contrôle de flux d'information vise à surveiller la façon dont l'information se dissémine dans le système une fois hors de son conteneur d'origine, contrairement au contrôle d'accès qui ne peut permettre d'appliquer des règles que sur la manière dont les conteneurs sont accédés. Plusieurs défis scientifiques et techniques se sont présentés. Premièrement, la base de code Linux est particulièrement grande, avec quinze millions de lignes de code réparties dans trente-mille fichiers. La première contribution de cette thèse a été un plugin pour le compilateur GCC permettant d'extraire et visualiser aisément les graphes de flot de contrôle des fonctions du noyau. Ensuite, le framework des Linux Security Modules qui est utilisé pour implémenter les moniteurs de flux d'information que nous avons étudiés (Laminar [1], KBlare [2] et Weir [3]) a été conçu en premier lieu pour le contrôle d'accès, et non de flux. La question se pose donc de savoir si le framework est implémenté de telle sorte à permettre la capture de tous les flux produits par les appels système. Nous avons créé et implémenté une analyse statique permettant de répondre à ce problème. Cette analyse statique est implémenté en tant que plugin GCC et nous a permis d'améliorer le framework LSM pour capturer tous les flux. Enfin, nous avons constaté que les moniteurs de flux actuels n'étaient pas résistants aux conditions de concurrence entre les flux et ne pouvaient pas traiter certains canaux ouverts tels que les projections de fichiers en mémoire et les segments de mémoire partagée entre processus. Nous avons implémenté Rfblare, un nouvel algorithme de suivi de flux, pour KBlare, dont nous avons prouvé la correction avec Coq. Nous avons ainsi montré que LSM pouvait être utilisé avec succès pour implémenter le contrôle de flux d'information, et que seules les méthodes formelles, permettant la mise en œuvre de méthodologie, d'analyses ou d'outils réutilisables, permettaient de s'attaquer à la complexité et aux rapides évolutions du noyau Linux. / We look forward to improving the implementations of information flow control mechanisms in Linux Operating Systems. Information Flow Control aims at monitoring how information disseminates in a system once it is out of its original container, unlike access control which can merely apply rule on how the containers are accessed. We met several scientific and technical challenges. First of all, the Linux codebase is big, over fifteen millions lines of code spread over thirty three thousand files. The first contribution of this thesis is a plugin for the GCC compiler able to extract and let a user easily visualize the control flow graphs of the Linux kernel functions. Secondly, the Linux Security Modules framework which is used to implement the information flow trackers we have reviewed (Laminar, KBlare, and Weir) was designed in the first place to implement access control, rather than information flow control. One issue is thus left open: is the framework implemented in such a way that all flows generated by system calls can be captured? We have created and implemented static analysis to address this problem and proved its correction with the Coq proof assistant system. This analysis is implemented as a GCC plugin and have allowed us to improve the LSM framework in order to capture all flows. Finally, we have noted that current information flow trackers are vulnerable to race conditions between flows and are unable to cover some overt channels of information such as files mapping to memory and shared memory segments between processes. We have implemented Rfblare, a new algorithm of flow tracking, for KBlare. The correction of this algorithm has been proved with Coq. We have showed that LSM can be used successfully to implement information flow control, and that only formal methods, leading to reusable methodology, analysis, tools, etc., are a match for the complexity and the fast-paced evolution of the Linux kernel.

Thèse numérisée par la Direction des bibliothèques de l'Université de Montréal.

L'objectif de ce travail est de fournir des modèles et outils pour simplifier la construction des systèmes distribués à base de composants sécurisés, ainsi que la gestion des propriétés de sécurité, en utilisant des outils de haut niveau d'abstraction pour la configuration et la reconfiguration dynamique. En plus des propriétés d'accessibilité et de communications sécurisées classiques, nous focalisons notre travail sur une propriété des systèmes répartis plus générale : la non-interférence. Cette propriété atteste qu'il ne doit pas y avoir de flux d'information entre des parties publiques et privées du système. Ce qui implique le suivi de l'acheminement de l'information entre les différentes composantes du système distribué. Notre objectif principal est donc de proposer un modèle, accompagné d'un ensemble d'outils, garantissant la propriété de la non-interférence à la construction du système, et ce à une plus grosse granularité : celle des composants. Ces outils permettent de (1) configurer les paramètres de sécurité des composants et des liaisons entre eux, (2) vérifier la propriété de non-interférence dans le code d'un composant et entre les différents composants du système et (3) générer automatiquement le code nécessaire pour appliquer ces propriétés de sécurité. D'autre part, nous proposons une architecture permettant de vérifier dynamiquement la propriété de non-interférence dans un système réparti. / The goal of this thesis is to provide models and tools to simplify secured component-based distributed systems' construction and the management of their security properties, by using high-level tools for dynamic configuration and reconfiguration. In addition to the classic properties of accessibility and secured communications, we focus on a more general security property of distributed systems : the non-interference. This property says that there mustn't be information flow between secret and public parts of the system ; which requires information flow control across the system. Our main objective is to propose a model and set of tools guarantying the non-interference property at compiletime, and at a bigger granularity : the components. These tools are (1) tools for configuring security parameters of components and binding between components, (2) a compiler checking the non-interference property, and (3) tools for automatic generation of code assuring these security properties. On the other hand, we present an architecture enabling a dynamic verification of the non-interference property in a distributed system.

L'augmentation envisagée de la pénétration des unités de production d'énergies décentralisées raccordées au réseau de distribution amène à revoir l'architecture physique et algorithmique de ce dernier. En effet, une insertion massive avec le schéma de réseau tel qu'il apparaît aujourd'hui, impliquera des problèmes au niveau du plan de tension, du schéma de protection, voire de la stabilité. L'électronique de puissance trouve là un champ fertile d'applications notamment pour tout ce qui est de la régulation de la circulation des flux énergétiques et du réglage du plan de tension. Les travaux menés dans cette thèse ont trait à une solution d'électronique de puissance de type série qui est à même de régler les transits de puissances active et réactive. Ce système permet également, sans modification de son architecture, de limiter les courants de court circuit. Le réseau envisagé pour l'étude est de type bouclé ou maillé ce qui préfigure la tendance des réseaux du futur. Les travaux théoriques relatifs aux différents niveaux de contrôle-commande ont été confrontés à l'expérimental avec succès. Le plan d'expérimentation consiste en une simulation temps réel hybride avec le compensateur réel et le réseau émulé et interfacé par de la puissance.

De nos jours, les ordinateurs sont omniprésents. Tous ces ordinateurs stockent et manipulent de l'information, parfois sensible, d'où l'intérêt de protéger et de confiner la dissémination de cette information. Les mécanismes de contrôle de flux d'information permettent justement d'analyser des programmes manipulant de l'information sensible, afin de prévenir les fuites d'information. Les contributions de cette thèse incluent des techniques d'analyse de programmes pour le contrôle de flux d'information tant qualitatif que quantitatif. Les techniques d'analyse qualitatives permettent la détection et la prévention des fuites d'information. Les techniques quantitatives permettent d'estimer ces fuites afin de décider si elles sont négligeables. / Computers have become widespread nowadays. All these computers store and process information. Often, some of this information is sensitive; hence the need to confine and control its dissemination. An important field in computer science, that is concerned about analysing programs in order to confine and control the release of sensitive information, is the information flow control field. The contributions of this thesis include program analysis techniques for qualitative and quantitative information flow control. Qualitative techniques aim at detecting and preventing information leaks. Quantitative techniques go beyong the detection of information leaks, by estimating the leakage in order to decide whether it is negligeable.

Ce travail vise à faire une pré-évaluation des paramètres de contrôle en vue de réduire la traînée sur véhicule réel. Deux mécanismes d’actionnement différents (Murata micro-blower et couteau d’air) ont été caractérisés et comparés en vue de déterminer leurs qualités ainsi que leurs limites. Les micro-blowers ont pour but d’exciter la couche limite en vue de perturber directement les structures tourbillonnaires formées dans la couche de cisaillement. Le couteau d’air étudié, à surface arrondie, pourrait être considéré comme un dispositif actif de réduction de la traînée à effet Coanda équivalent au dispositif passif de type boat-tail. Différentes stratégies de contrôle en boucles ouverte et fermée sont examinées, telles que le soufflage continu, le forçage périodique, le contrôle du mode glissant (SMC) et le contrôle par apprentissage (MLC). La SMC est un algorithme robuste en boucle fermée permettant de suivre, d’atteindre et de maintenir une consigne prédéfinie; cette approche présente l’intérêt d’avoir une capacité d’adaptation prenant en compte les perturbations extérieures inconnues. Le contrôle par apprentissage est un contrôle sans modèle qui permet de définir des lois de contrôle efficaces qualifiées et optimisées via une fonction coût/objectif spécifique au problème donné. Une solution hybride entre MLC et SMC peut également fournir un contrôle adaptatif exploitant les mécanismes d’actionnement non linéaires les plus adaptés au problème. L’ensemble de ces techniques de contrôle ont été testées sur diverses applications expérimentales allant d’une simple configuration académique de marche descendante jusqu’à des géométries présentant une structure d’écoulement représentatives de véhicules réels. Pour la configuration de marche descendante, l’objectif était de réduire expérimentalement la zone de recirculation via une rangée de micro-jets et de l’estimer par des capteurs de pression. Les contrôles d’écoulement ont été réalisés par forçage périodique ainsi que par MLC. On démontre dans ce cas que la MLC peut surpasser le contrôle par forçage périodique. Pour la configuration sur corps épais (corps d’Ahmed), l’objectif était de réduire et/ou de maintenir la traînée aérodynamique via un couteau d’air placé sur la partie supérieure du hayon arrière et évalué par le biais d’une balance aérodynamique. Le soufflage continu et le forçage périodique ont été utilisés dans ce cas comme stratégies de contrôle en boucle ouverte permettant ainsi de faire une comparaison avec les algorithmes SMC et MLC. La pré-évaluation des paramètres de contrôle a permis d’obtenir des informations importantes en vue d’une réduction de la traînée sur un véhicule réel. Dans ce cadre, les premiers essais de caractérisation sur véhicules réels ont été réalisés sur piste et un dispositif d’actionnement ainsi qu’un protocole expérimental sont également présentés en perspective à ce travail. / The present work aims to pre-evaluate flow control parameters to reduce the drag in a real vehicle. Two different actuation mechanisms (Murata’s micro-blower, and air-knives) are characterized and compared to define their advantages and limitations. Murata micro-blowers energized the boundary layer to directly perturb the vortex structures formed in the shear layer region. The air-knife has a rounded surface, adjacent to the slit exit, that could be considered as an active boat-tail (Coanda effect) for drag reduction. Different open-loop and closed-loop control strategies are examined, such as continuous blowing, periodic forcing, sliding mode control (SMC) and machine learning control (MLC). SMC is a robust closed-loop algorithm to track, reach and maintain a predefined set-point; this approach has on-line adaptivity in changing conditions. Machine learning control is a model-free control that learns an effective control law that is judged and optimized with respect to a problem-specific cost/objective function. A hybrid between MLC and SMC may provide adaptive control exploiting the best non-linear actuation mechanisms. Finally, all these parameters are brought together and tested in real experimental applications representative of the mean wake and shear-layer structures related to control of real cars. For the backward-facing step, the goal is to experimentally reduce the recirculation zone. The flow is manipulated by a row of micro-blowers and sensed by pressure sensors. Initial measurements were carried out varying the periodic forcing. MLC is used to improve performance optimizing a control law with respect to a cost function. MLC is shown to outperform periodic forcing. For the Ahmed body, the goal is to reduce the aerodynamic drag of the square-back Ahmed body. The flow is manipulated by an air-knife placed on the top trailing edge and sensed by a force balance. Continuous blowing and periodic forcing are used as open-loop strategies. SMC and MLC algorithms are applied and compared to the open-loop cases. The pre-evaluation of the flow control parameters yielded important information to reduce the drag of a car. The first real vehicle experiments were performed on a race track. The first actuator device concept and sensor mechanism are presented.

Nous développons une méthode de modélisation et de validation adaptée aux système parallèles structurés en couches hiérarchiques. Nous définissons deux notions : la concordance de modèle prouve que le modèle possède bien les propriétés dégagées par les spécifications; l'adéquation de service valide le protocole par rapport à son service. Nous appliquons notre méthode à la modélisation du protocole de télécommunication de niveau Transport (la couche 4 d'après la norme ISO sur l'interconnexion des systèmes ouverts). Nous étudions tout particulièrement la gestion de désynchronisations du Service de la couche Réseau, et le contrôle de flux avec réquisition de crédit du protocole de la couche Transport. Nous utilisons les réseaux de Petri à prédicats pour décrire le modèle du service rendu par le couche Réseau sous-jacente et nous en servir pour construire le modèle du protocole de ma couche Transport. nous prouvons que la notion d'abstraction peut s'étendre aux réseaux de Petri à prédicats. La preuve du déroulement correct du protocole est apportée en utilisant les invariants issus du modèle.

Le streaming adaptatif sur HTTP, désigné par HAS, est une technique de streaming vidéo largement déployée sur Internet. Elle utilise TCP comme protocole de transport. Elle consiste à segmenter la vidéo stockée sur un serveur web en petits segments indépendants de même durée de lecture et transcodés à plusieurs niveaux de qualité, désignés par "chunks". Le player, du côté du client HAS, demande périodiquement un nouveau chunk. Il sélectionne le niveau de qualité en se basant sur l’estimation de la bande passante du/des chunk(s) précédent(s). Étant donné que chaque client HAS est situé au sein d’un réseau d’accès, notre étude traite un cas fréquent dans l’usage quotidien: lorsque plusieurs clients partagent le même lien présentant un goulot d’étrangement et se trouvent en compétition sur la bande passante. Dans ce cas, on signale une dégradation de la qualité d’expérience (QoE) des utilisateurs de HAS et de la qualité de service (QoS) du réseau d’accès. Ainsi, l’objectif de cette thèse est d’optimiser le protocole TCP pour résoudre ces dégradations de QoE et QoS. Notre première contribution propose une méthode de bridage du débit HAS au niveau de la passerelle. Cette méthode est désignée par "Receive Window Tuning Method" (RWTM): elle utilise le principe de contrôle de flux de TCP et l’estimation passive du RTT au niveau de la passerelle. Nous avons comparé les performances de RWTM avec une méthode récente implémentée à la passerelle qui utilise une discipline particulière de gestion de la file d’attente, qui est désignée par "Hierarchical Token Bucket shaping Method" (HTBM). Les résultats d’évaluations indiquent que RWTM offre une meilleure QoE et une meilleure QoS de réseau d’accès que HTBM. Notre deuxième contribution consiste à mener une étude comparative combinant deux méthodes de bridages, RWTM et HTBM, avec quatre variantes TCP largement déployées, NewReno, Vegas, Illinois et Cubic. Les résultats d'évaluations montrent une discordance importante entre les performances des différentes combinaisons. De plus, la combinaison qui améliore les performances dans la majorité des scénarios étudiés est celle de RWTM avec Illinois. En outre, une mise à jour efficace de la valeur du paramètre "Slow Start Threshold", sthresh, peut accélérer la vitesse de convergence du player vers la qualité optimale. Notre troisième contribution propose une nouvelle variante de TCP adaptée aux flux HAS, qu’on désigne par TcpHas; c’est un algorithme de contrôle de congestion de TCP adapté aux spécifications de HAS. TcpHas estime le niveau de la qualité optimale du flux HAS en se basant sur l’estimation de la bande passante de bout en bout. Ensuite, TcpHas applique un bridage au trafic HAS en fonction du débit d’encodage du niveau de qualité estimé. TcpHas met à jour ssthresh pour accélérer la vitesse de convergence. Une étude comparative a été réalisée avec la variante Westwood+. Les résultats d’évaluations montrent que TcpHas est plus performant que Westwood+. / HTTP adaptive streaming (HAS) is a streaming video technique widely used over the Internet. It employs Transmission Control Protocol (TCP) as transport protocol and it splits the original video inside the server into segments of same duration, called "chunks", that are transcoded into multiple quality levels. The HAS player, on the client side, requests for one chunk each chunk duration and it commonly selects the quality level based on the estimated bandwidth of the previous chunk(s). Given that the HAS clients are located inside access networks, our investigation involves several HAS clients sharing the same bottleneck link and competing for bandwidth. Here, a degradation of both Quality of Experience (QoE) of HAS users and Quality of Service (QoS) of the access network are often recorded. The objective of this thesis is to optimize the TCP protocol in order to solve both QoE and QoS degradations. Our first contribution consists of proposing a gateway-based shaping method, that we called Receive Window Tuning Method (RWTM); it employs the TCP flow control and passive round trip time estimation on the gateway side. We compared the performances of RWTM with another gateway-based shaping method that is based on queuing discipline, called Hierarchical Token Bucket shaping Method (HTBM). The results of evaluation indicate that RWTM outperforms HTBM not only in terms of QoE of HAS but also in terms of QoS of access network by reducing the queuing delay and significantly reducing packet drop rate at the bottleneck.Our second contribution consists of a comparative evaluation when combining two shaping methods, RWTM and HTBM, and four very common TCP variants, NewReno, Vegas, Illinois and Cubic. The results show that there is a significant discordance in performance between combinations. Furthermore, the best combination that improves performances in the majority of scenarios is when combining Illinois variant with RWTM. In addition, the results reveal the importance of an efficient updating of the slow start threshold value, ssthresh, to accelerate the convergence toward the best feasible quality level. Our third contribution consists of proposing a novel HAS-based TCP variant, that we called TcpHas; it is a TCP congestion control algorithm that takes into consideration the specifications of HAS flow. Besides, it estimates the optimal quality level of its corresponding HAS flow based on end-to-end bandwidth estimation. Then, it permanently performs HAS traffic shaping based on the encoding rate of the estimated level. It also updates ssthresh to accelerate convergence speed. A comparative performance evaluation of TcpHas with a recent and well-known TCP variant that employs adaptive decrease mechanism, called Westwood+, was performed. Results indicated that TcpHas largely outperforms Westwood+; it offers better quality level stability on the optimal quality level, it dramatically reduces the packet drop rate and it generates lower queuing delay.