Ce travail de thèse, effectué dans la cadre du projet FUI Minalogic Bluesky, porte sur le test fonctionnel automatisé d'une classe particulière de contrôleurs logiques programmables (em4) produite par InnoVista Sensors. Ce sont des systèmes synchrones qui sont programmés au moyen d'un environnement de développement intégré (IDE). Les personnes qui utilisent et programment ces contrôleurs ne sont pas nécessairement des programmeurs experts. Le développement des applications logicielles doit être par conséquent simple et intuitif. Cela devrait également être le cas pour les tests. Même si les applications définies par ces utilisateurs ne sont pas nécessairement très critiques, il est important de les tester d'une manière adéquate et efficace. Un simulateur inclu dans l'IDE permet aux programmeurs de tester leurs programmes d'une façon qui reste à ce jour informelle et interactive en entrant manuellement des données de test. En se basant sur des recherches précédentes dans le domaine du test des programmes synchrones, nous proposons un nouveau langage de spécification de test, appelé SPTL (Synchronous Programs Testing Language) qui rend possible d'exprimer simplement des scénarios de test qui peuvent être exécutées à la volée pour générer automatiquement des séquences d'entrée de test. Il permet aussi de décrire l'environnement où évolue le système pour mettre des conditions sur les entrées afin d'arriver à des données de test réalistes et de limiter celles qui sont inutiles. SPTL facilite cette tâche de test en introduisant des notions comme les profils d'utilisation, les groupes et les catégories. Nous avons conçu et développé un prototype, nommé "Testium", qui traduit un programme SPTL en un ensemble de contraintes exploitées par un solveur Prolog qui choisit aléatoirement les entrées de test. La génération de données de test s'appuie ainsi sur des techniques de programmation logique par contraintes. Pour l'évaluer, nous avons expérimenté cette méthode sur des exemples d'applications EM4 typiques et réels. Bien que SPTL ait été évalué sur em4, son utilisation peut être envisagée pour la validation d'autres types de contrôleurs ou systèmes synchrones. / This thesis work done in the context of the FUI project Minalogic Bluesky, concerns the automated functional testing of a particular class of programmable logic controllers (em4) produced by InnoVista Sensors. These are synchronous systems that are programmed by means of an integrated development environment (IDE). People who use and program these controllers are not necessarily expert programmers. The development of software applications should be as result simple and intuitive. This should also be the case for testing. Although applications defined by these users need not be very critical, it is important to test them adequately and effectively. A simulator included in the IDE allows programmers to test their programs in a way that remains informal and interactive by manually entering test data.Based on previous research in the area of synchronous test programs, we propose a new test specification language, called SPTL (Synchronous Testing Programs Language) which makes possible to simply express test scenarios that can be executed on the fly to automatically generate test input sequences. It also allows describing the environment in which the system evolves to put conditions on inputs to arrive to realistic test data and limit unnecessary ones. SPTL facilitates this testing task by introducing concepts such as user profiles, groups and categories. We have designed and developed a prototype named "Testium", which translates a SPTL program to a set of constraints used by a Prolog solver that randomly selects the test inputs. So, generating test data is based on constraint logic programming techniques.To assess this, we experimented this method on realistic and typical examples of em4 applications. Although SPTL was evaluated on EM4, its use can be envisaged for the validation of other types of synchronous controllers or systems.

Cette thèse étudie la vérification automatique de propriétés de sûreté de systèmes logico-numériques discrets ou hybrides. Ce sont des systèmes ayant des variables booléennes et numériques et des comportements discrets et continus. Notre approche est fondée sur l'analyse statique par interprétation abstraite. Nous adressons les problèmes suivants : les méthodes d'interprétation abstraite numériques exigent l'énumération des états booléens, et par conséquent, ils souffrent du probléme d'explosion d'espace d'états. En outre, il y a une perte de précision due à l'utilisation d'un opérateur d'élargissement afin de garantir la terminaison de l'analyse. Par ailleurs, nous voulons rendre les méthodes d'interprétation abstraite accessibles à des langages de simulation hybrides. Dans cette thèse, nous généralisons d'abord l'accélération abstraite, une méthode qui améliore la précision des invariants numériques inférés. Ensuite, nous montrons comment étendre l'accélération abstraite et l'itération de max-stratégies à des programmes logico-numériques, ce qui aide à améliorer le compromis entre l'efficacité et la précision. En ce qui concerne les systèmes hybrides, nous traduisons le langage de programmation synchrone et hybride Zelus vers les automates hybrides logico-numériques, et nous étendons les méthodes d'analyse logico-numérique aux systèmes hybrides. Enfin, nous avons mis en oeuvre les méthodes proposées dans un outil nommé ReaVer et nous fournissons des résultats expérimentaux. En conclusion, cette thèse propose une approche unifiée à la vérification de systèmes logico-numériques discrets et hybrides fondée sur l'interprétation abstraite qui est capable d'intégrer des méthodes d'interprétation abstraite numériques sophistiquées tout en améliorant le compromis entre l'efficacité et la précision. / This thesis studies the automatic verification of safety properties of logico-numerical discrete and hybrid systems. These systems have Boolean and numerical variables and exhibit discrete and continuous behavior. Our approach is based on static analysis using abstract interpretation. We address the following issues: Numerical abstract interpretation methods require the enumeration of the Boolean states, and hence, they suffer from the state space explosion problem. Moreover, there is a precision loss due to widening operators used to guarantee termination of the analysis. Furthermore, we want to make abstract interpretation-based analysis methods accessible to simulation languages for hybrid systems. In this thesis, we first generalize abstract acceleration, a method that improves the precision of the inferred numerical invariants. Then, we show how to extend abstract acceleration and max-strategy iteration to logico-numerical programs while improving the trade-off between efficiency and precision. Concerning hybrid systems, we translate the Zelus hybrid synchronous programming language to logico-numerical hybrid automata and extend logico-numerical analysis methods to hybrid systems. Finally, we implemented the proposed methods in ReaVer, a REActive System VERification tool, and provide experimental results. Concluding, this thesis proposes a unified approach to the verification of discrete and hybrid logico-numerical systems based on abstract interpretation, which is capable of integrating sophisticated numerical abstract interpretation methods while successfully trading precision for efficiency.

Cette Thèse présente une méthodologie pour la conception optimale multidisciplinaire des générateurs synchrones à aimants permanents appliqués à l'énergie éolienne. Telle méthodologie prend en compte les comportements électriques, géométriques, thermiques, électroniques, mécaniques et économiques de l'éolienne. La courbe d'occurrence du vent, modélisée par une fonction de densité statistique, est également prise en compte par la méthodologie de conception proposée. Considérer cette courbe dans la conception optimale permet de calculer la quantité d'énergie produite par l'éolienne, qui fonctionne sous vitesse et puissance variables par l'influence de la vitesse du vent. La proposition d'utiliser l'optimisation dans la conception est d'améliorer la compétitivité de l'énergie éolienne en concevant un générateur avec une bonne relation entre son coût et sa capacité de produire de l'énergie. Plusieurs études portent sur la conception optimale des machines électriques liées à l'énergie éolienne, mais peu ont présenté une méthode permettant d'estimer la production d'énergie éolienne, ce qui est obligatoire pour obtenir un générateur rentable. De plus, les aspects multidisciplinaires approfondis du générateur électrique ont été considérés par la méthode proposée plus en détail que d'autres études trouvées dans la littérature. Prendre en compte tous ces aspects entraîne un grand problème d'optimisation qui compte environ 2000 variables, dont environ 250 ont des contraintes imposées. Un algorithme d'optimisation déterministe a été choisi pour traiter ce problème. Un tel algorithme est capable de trouver la solution en quelques itérations et un court laps de temps grâce au calcul de la matrice jacobienne, contenant les gradients exacts du modèle (utilisé pour décrire le comportement de l'éolienne). Les résultats présentés explorent le potentiel méthodologique proposé. La première conception optimale réalisée minimise le coût du matériau actif du générateur, ce qui présente une réduction significative des coûts par rapport à un générateur non optimal. Ensuite, la contradiction entre le coût du générateur et son efficacité est analysée et l'importance d'inclure la production d'énergie éolienne dans la conception du générateur devient évidente. En utilisant l'énergie éolienne estimée générée par l'éolienne, le générateur avec un bénéfice net maximal (égal au produit de l'énergie éolienne moins le coût du générateur) a été obtenu. Ce générateur a un bon rapport entre son coût et sa capacité de produire de l'énergie. Ensuite, des analyses de sensibilité ont été effectuées pour vérifier comment le prix de l'électricité et la vitesse moyenne annuelle du vent influencent la conception. Enfin, deux éoliennes de différents diamètres et différents vitesses nominales du vent ont été utilisées, compte tenu de trois profils de vent distincts. Ces résultats fournissent les générateurs plus adaptés à chaque éolienne appliquée à chaque profil de vent, montrant que la méthodologie de conception proposée a la capacité de faciliter le choix de l'éolienne adéquate à chaque parc éolien. / This Ph.D. dissertation presents a multidisciplinary optimum design methodology to permanent magnet synchronous generators applied to wind power. Such a methodology considers the electrical, the geometrical, the thermal, the electronic, the mechanical and the economical behaviors of the wind turbine. The wind occurrence curve, modelled by a statistical density function, is also take into account by the proposed design methodology. Considering this curve in the optimal design allows to calculate the amount of energy produced by the wind turbine, which operates under variable speed and power by the influence of the actual wind speed. The proposal of using the optimization in the design is to enhances the competitiveness of wind power by designing a generator with a good relation between its cost and its capacity to generate energy. Several studies are addressed to electrical machines optimum design related to wind power, however, few have presented a method able to estimate the wind turbine energy generation, which is mandatory to obtain a cost-effective generator. Further, the electric generator in-depth multidisciplinary aspects have been considered by the proposed method in more detail than other studies found in literature. Take into consideration all these aspects results in a large optimization problem that has approximately 2000 variables, among which approximately 250 have constraints imposed on. A deterministic optimization algorithm has been chosen to deal with this problem. Such an algorithm is capable of finding the solution within few iterations and a short time thanks to the computation of the Jacobean matrix, containing the exact gradients of the model (used to describe the wind turbine behavior) outputs. The presented results explore the proposed methodology potential. The first optimal design performed minimizes the generator active material cost, presenting a significant cost reduction compared to a non-optimal generator. Next, the contradiction between the generator cost and its efficiency is analyzed and the importance of including the wind turbine energy generation into the generator design becomes evident. Using the estimated wind turbine generated energy, the generator with maximum net earnings (equal to the wind turbine energy proceeds less the generator cost) has been obtained. This generator has a good ratio between its cost and capability to generate energy. Then, sensibility analysis have been carried out to verify how the electricity price and the annual mean wind speed influence the design. Finally, two wind turbines with different diameters and rated wind speeds have been employed, considering three distinct wind profiles. These results provide the generators more suited to each wind turbine applied to each wind profile, showing that the proposed design methodology has the ability to helps choosing the wind turbine adequate to each wind farm.

Nowadays, new approaches to fabricate high-performance electrode materials are of vital importance in the renewable energy field. Here, we present a facile synthesis procedure of 3D Ni(OH)2/graphene hybrids for supercapacitors via synchronous electrochemical-assisted exfoliation and assembly of graphene on 3D Ni(OH)2 networks. With the assistance of an electric field, the electrochemically exfoliated high-quality graphene can be readily, uniformly assembled on the surfaces of 3D Ni(OH)2. When serving as electrode materials for supercapacitors, the resulting 3D Ni(OH)2/graphene composites exhibited excellent specific capacitance (263 mF cm−2 at 2 mA cm−2), remarkable rate capability and super-long cycle life (retention of 94.1% even after 10 000 continuous charge–discharge cycles), which may be attributed to their highly porous, stable 3D architecture as well as uniform, firm anchoring of ultrathin graphene on their surfaces. Therefore, our approach provides a facile strategy for the large-scale synthesis of high-quality graphene based composites towards various applications.

Ce travail de recherche présente la mise au point d’une méthodologie de conception par optimisation globale des machines synchrones sans encoches à aimants permanents à haute vitesse utilisant des matériaux magnétiques composites doux (SMC) au stator et des frettes au rotor éventuellement conductrices. Cette méthodologie tient compte des différentes contraintes imposées par la haute vitesse, notamment les courants de Foucault induits dans les pièces massives, les pertes, l’alimentation en commutation électronique et les efforts mécaniques sur le rotor. Un outil de dimensionnement générique est développé pour différentes structures de machines sans encoches fonctionnant en moteur ou en générateur et alimentées par divers types de convertisseurs statiques à commutation de tension ou de courant. Il utilise un modèle de dimensionnement analytique basé sur la prédiction du champ magnétique 2D par une résolution harmonique des équations de Maxwell en magnétodynamique en tenant compte des courants de Foucault induits dans les parties conductrices. Ce modèle intègre un modèle électrique équivalent global de l’ensemble convertisseur-machine et un modèle détaillé de calcul des pertes validés par un calcul numérique du champ en 2D. Une validation expérimentale des pertes magnétiques dans le stator en SMC est effectuée. Le modèle de dimensionnement est associé à une procédure d’optimisation et à un mécanisme de correction itératif, basé sur le calcul numérique du champ en 3D, pour tenir compte des effets de bord sur les pertes par courants de Foucault dans le stator. Lorsque la machine est couplée à un convertisseur à commutation de courant, un autre mécanisme de correction, permettant la résolution du couplage fort entre la machine et son convertisseur, est utilisé. Les différents outils de modélisation et de conception réalisés sont utilisés pour dimensionner et comparer plusieurs topologies de machines sans encoches pour des cahiers des charges spécifiques. Différentes études de faisabilité et de sensibilité sont aussi effectuées. / This research work presents the development of a design methodology with global optimization of high-speed permanent-magnet slotless synchronous machines using soft magnetic composite materials (SMC) in the stator and retaining sleeves in the rotor that can be conductive. This methodology takes into account the different constraints imposed by the high speed such as the eddy currents induced in the massive parts, the losses, the converter-machine interactions and the mechanical stress in rotor. A generic design tool is developed for different slotless machines structures used as motors or generators and coupled to different kind of static power converters with voltage or current commutation. It uses a design model based on analytical prediction of the two-dimensional magnetic field by a harmonic resolution of Maxwell equations taking into account the eddy currents induced in the conductive parts. This model includes an equivalent electric model of the converter-machine system and a detailed losses calculation model validated by 2D finite element analysis. Experimental validation of magnetic losses in the SMC stator is also performed. The design model is associated to an optimization procedure and an iterative correction mechanism performed by 3D finite element simulations to take into account the influence of end-effects on the SMC stator eddy current losses. When the machine is coupled to a current static converter, another correction mechanism is used in order to resolve the strong coupling between the machine and its converter. The developed modeling and design tools are used to design and compare different slotless machines topologies for specific requirements. Various feasibility and sensitivity studies are also performed.

Cette thèse s’inscrit dans une thématique de recherche prioritaire développée par le laboratoire GREAH et portant sur l’optimisation de l'efficacité énergétique des systèmes de gestion et de production de l’énergie électrique. Dans ce cadre, les performances de convertisseurs d’énergie (machines électriques pour la conversion de l'énergie électromécanique) ont un impact déterminant sur l'efficacité énergétique de la conversion et sur la qualité de gestion de l'énergie électrique en termes de rendement, de maximisation de la puissance massique, de réduction des émissions, de réduction des coûts, ce qui nécessite, par conséquent, un effort particulier de conception et de dimensionnement. L’objectif principal de cette thèse vise à développer un modèle léger permettant d’exploiter assez rapidement l’espace des solutions potentiellement optimales dans la première phase de la conception des machines synchrones à aimants permanents. Les travaux présentés dans ce mémoire de thèse portent sur la modélisation électromagnétique pour le pré-dimensionnement et la conception des machines synchrones à aimants permanents intégrées dans l’éolien de fort puissance. Dans ce manuscrit, deux approches de modélisation des machines électriques ont été proposées. La modélisation par réseau de réluctances présentée consiste à découper le domaine d’étude en un certain nombre d’éléments volumiques dont chacun est décomposé en tubes de flux. La modélisation analytique hybride proposée est basée sur un couplage fort entre un réseau de réluctances généré à partir d’un maillage du domaine d’étude et une solution formelle des équations de Maxwell dans les régions de faible perméabilité (entrefer magnétique). Les résultats obtenus à partir de ces modèles sont validés par les résultats correspondants issus de la méthode des éléments finis. Pour montrer le gain obtenu en temps de calcul, les temps d’exécutions des codes de calcul sont comparés aux temps mis par le logiciel Flux. / This subject of the thesis is part of a priority research theme developed by the GREAH laboratory on the optimization of the energy efficiency of electrical energy management and production systems. In this context, the performance of energy converters (electrical machines for the conversion of electromechanical energy) have a decisive impact on the energy efficiency of the conversion and on the quality of electrical energy management in terms of efficiency, reduction of emissions, reduction of costs, which therefore requires a special effort to design. The main objective of this thesis is to develop a light model allowing to exploit fairly quickly the space of potentially optimal solutions in the first phase of machine design. The work presented in this thesis focuses on electromagnetic modeling for the pre-design of permanent magnets synchronous machines integrated into high power wind turbines. In this manuscript, two modeling approaches of electric machines have been proposed. The presented reluctance network modeling is generated from the mesh of studied domain as the finite element method. Reluctance elements are used for the mesh. The proposed hybrid analytical modeling is based on a strong coupling between a reluctances network generated from a mesh of the study domain and analytical models based on the formal solution of Maxwell’s equations in regions of low permeability (magnetic gap). This approach can help solve the problem of air-gap modeling in MEC method, and the consideration of the local magnetic saturation in modeling approaches involving analytical technique. The results obtained from these models are validated by the corresponding results from the finite element method and very good has been observed. To indicate the gain obtained in time, the execution times of the programs are compared to the times set by the Flux software.

Pour certaines applications de positionnement dans les systèmes embarqués la puissance ou les couples mis jeu en peuvent être faibles. Les actionneurs utilisés pour ces applications sont équipés de machines pas à pas telles que les machines réluctance variable excitées ou non, ou encore des machines synchrones à aimants permanents. En aéronautique, ces actionneurs doivent être les plus compacts possibles et la continuité de service est exigée. La redondance partielle ou totale de l'actionneur est solution permettant d'assurer la continuité de service. Nous avons étudiés plusieurs structures de machines notamment les machines à deux voies d'enroulement pour leurs compacité telles les machines à reluctance variable à excitation homopolaire (MRVH-2C) et les machines synchrones à aimants permanent (MSAP-DE). Dans le but faciliter ou motiver le choix de l'une ou l'autre des structures, nous avons développé des modèles de machines capables de fournir des informations sur les grandeurs mesurables ou non, et sur le comportement des actionneurs. Ainsi à partir d'un calcul éléments finis 2D nous avons mis au point plusieurs modèles couplés EF 2D réseau de perméances de la MRVH-2C qui tiennent compte de l'état de saturation magnétique et du caractère tridimensionnel de cette machine. Ceux-ci ont été utilisés pour simuler le comportement de l'actionneur dans différents situations. Toujours pour une application de positionnement à faibles puissance et basse vitesse, nous avons dimensionné, modélisé et simulé une MSAP-DE commandée en boucle fermée et qui, de façon intrinsèque tolère le défaut de court-circuit triphasé grâce à sa résistance de phase qui est élevée / For certain applications of positioning in embedded systems power or torque needed can be low. Actuators used for these applications can be equipped with stepper machinery such as variable reluctance machines excited (or not) or permanent magnets synchronous machine. In aeronautic these actuators should be as compact as possible and continuity of service is required. Partial or total redundancy of the actuator can ensure the continuity of service. We have studied various structures of machines particularly double channel machines for their compactness such as two channels hybrid variable reluctance machines (2C-HVRM) and double channel permanent magnets synchronous machines (DC-PMSM). In the aim of facilitating or of justifying the choice of one or the other of these structures, we have developed models of able to provide information on measurable (or non measurable) features, and the behavior of the actuators. So from a 2D finite element calculation we have developed several coupled 2D FE permeances network models of a 2C-HVRM tacking account of the magnetic saturation state of this machine and its three-dimensional character. These models were used to simulate the behavior of the actuator in different situations. Always for positioning application with low power and low speed, we sized, modeled and simulated a DC-PMSM close loop controlled. That machine is intrinsically tolerant to phase short-circuit fault, thanks to its high phase resistance

La mise en place d’un nouveau canal d’alimentation électrique incorporant un générateur à aimants permanents PMG (Permanent Magnet Generator) en remplacement de l’actuel canal de génération hydraulique est l’un des sujets de recherche en cours dans le secteur aéronautique. Le choix de cette solution est motivé par de nombreux avantages : réduction de masse, meilleure disponibilité du réseau hydraulique et maintenance plus aisée. Cependant, l’utilisation d’un PMG en tant que générateur électrique au sein d’un avion implique de nouvelles problématiques, notamment en ce qui concerne la sûreté de fonctionnement lors de défaillances internes au PMG. En effet, tant que le rotor est en rotation, la présence d’une excitation permanente due aux aimants entretient la présence du défaut même si le stator n’est plus alimenté, ce qui complexifie la mise en sécurité du PMG. Il est ainsi nécessaire de connaître précisément l’état de santé du PMG afin d’assurer une bonne continuité de service en évitant d’ordonner la mise en sécurité du PMG sur des défaillances externes au générateur. C’est pourquoi les travaux de cette thèse portent sur la détection des courts-circuits inter-spires dans les PMG, ces défauts ayant été identifiés comme les plus critiques pour ce type de machine. Compte tenu du contexte aéronautique, il a été choisi de travailler sur les méthodes de détection basées sur l’estimation de paramètres via un modèle mathématique de la machine en utilisant le Filtre de Kalman Etendu (FKE). En effet, s’il est correctement paramétré, le FKE permet d’obtenir une bonne dynamique de détection et s’avère être très robuste aux variations du réseau électrique (vitesse, déséquilibre, …), critère important pour garantir un canal de génération fiable. Deux types de modèle mathématique sont présentés pour la construction d’un indicateur de défaut utilisant les estimations fournies par le FKE. Le premier est basé sur une représentation saine du PMG où l’indicateur de défaut est construit à partir de l’estimation de certains paramètres de la machine (résistance, inductance, constante de fem ou pulsation électrique). Le second modèle utilise une formulation d’un PMG défaillant qui permet d’estimer le pourcentage de spires en court-circuit. Après avoir comparé et validé expérimentalement le comportement des différents indicateurs sur un banc de test à puissance réduite, la mise en place d’un indicateur de court-circuit inter-spires au sein d’un réseau électrique aéronautique et son interaction avec les protections existantes sur avion sont étudiées dans la dernière partie de ce mémoire. / The establishment of an electrical power supply channel including a Permanent Magnet Generator (PMG) to replace an hydraulic power channel is one of the current topics of research in the aeronautic field. This choice is motivated by several benefits : weight reduction, improvement of the hydraulic network avaibility and easier maintenance. However, the use of PMG as an electrical generator in an aircraft implies new issues, particularly as regards safety considerations when an internal fault occurs in the PMG. Indeed, as long as the rotor in rotating, the presence of the persistent excitation due to the magnets maintains the internal fault even if the stator is de-energized. This makes the safety procedure of PMG more complex. Therefore, it is necessary to precisely know the behavior of the PMG (healthy or faulty) to ensure the avaibility of this power supply channel in order to avoid triggering PMG safety procedure when an external fault occurs. Thus, this work deals with the on-line detection of inter-turn short-circuits in PMG, these faults have been identified as the most critical for this kind of machine Given the aeronautic context, it has been decided to work on detection methods based on parameter estimation via a mathematical model of the machine using the Extended Kalman Filter (EKF). Indeed, with an appropriate setting, the EKF provides a fast dynamic detection and can be very robust to variations in the electrical network (speed, unbalanced, ...) which is an important characteristic to ensure a reliable generation channel. Two types of mathematical model are presented for fault indicator construction using the estimations provided by the EKF. The first one is based on an healthy representation of the PMG where the fault indicator is built from the estimation of PMG electrical parameters (resistance, inductance, electromotive force constant or electrical rotational velocity). The second model uses a faulty PMG formulation to estimate the ratio of short-circuited turns. After the comparison and the experimental validation of the fault indicators behavior on a test bench at reduced power, the establishment of a inter-turn short-circuit indicator within an aircraft electrical system and its interaction with existing protections are studied in the last part of this thesis.

Les activités du Laboratoire de recherche en Électronique, Électrotechnique et Systèmes (L2ES) sont dans le champ des transports que ce soit pour la génération d'énergie au moyen de PACs ou pour la chaîne de traction. Les travaux de recherche, dans ce dernier domaine, portent essentiellement sur les MSAPs à entraînement direct lent du type synchrone avec balais ou autopiloté à commande trapézoïdale ou sinusoïdale.<br />L'objectif consiste maintenant à orienter les recherches vers les actionneurs à vitesse élevée. Une application importante concerne l'entraînement de compresseurs pour le système PAC. Des études menées au L2ES ont montré que les turbocompresseurs constituaient une solution intéressante pour limiter la taille et la puissance absorbée.<br />Nous proposons dans cette thèse de mettre au point une méthodologie de conception de MSAPs montés en surface à vitesse élevée en vue de leur optimisation en prenant en considération les contraintes magnétiques, électriques et thermiques. Cette méthodologie prend en compte des contraintes spécifiques de la grande vitesse, et notamment les pertes électromagnétiques dans la partie tournante induites par la fréquence élevée d'alimentation. Les pertes magnétiques dans l'induit denté créées par une aimantation radiale ou parallèle des aimants permanents sont également modélisées. En effet, deux modèles analytiques complexes (magnétostatique et magnétodynamique) ont été développés pour prédire ces pertes fer significatives dans les MSAPs sans pièces polaires à inducteur intérieur ou extérieur. La méthode est générale, parce qu'elle est basée sur le calcul de champ électromagnétique bidimensionnel (2D) en coordonnées polaires (résolution des équations de Laplace/Poisson/Diffusion). L'analyse prend en compte les notions de courbures, les harmoniques de temps et d'espace de la répartition des courants de l'induit produite par un bobinage quelconque, l'effet du champ de réaction d'induit par courant de Foucault, et enfin différentes configurations de bobinages statoriques ("généralisation" des bobinages) ainsi que deux types d'aimantation (radiale et parallèle). L'hypothèse principale consiste dans le fait que l'on néglige la variation de perméance due au stator denté. Les contraintes mécaniques ont été traitées en liaison avec le mécanicien de la société NOVELTE Système de Belfort (90).<br />La MSAP réalisée tourne à 10 000 tr/min avec un résolveur analogique "sin-cos" à aimants permanents constitué de capteurs à effet Hall. Le moteur construit servira de base de validation dans la zone de vitesse concernée (i.e., de 0 à 10 000 tr/min).

<p>Les travaux de cette thèse s'inscrivent dans le cadre de la validation formelle et le contrôle réactif de calculs à haute performance sur systèmes-sur-puce (SoC). </p> <p>Dans ce contexte, la première contribution est la modélisation synchrone accompagnée d'une transformation d'applications en équations synchrones. Les modéles synchrones permettent de résoudre plusieurs questions liées à la validation formelle via l'usage des outils et techniques formels offerts par la technologie synchrone. Les transformations sont développées selon l'approche d'Ingénierie Dirigé par les Modèles (IDM). </p> <p>La deuxième contribution est une extension et amélioration des mécanismes de contrôle pour les calculs à haute performance, sous forme de constructeurs de langage de haut-niveau et de leur sémantique. Ils ont été défini afin de permettre la vérification, synthèse et génération de code. Il s'agit de déterminer un niveau d'abstraction de représentation des systèmes où soit extraite la partie contrôle, et de la modéliser sous forme d'automates à états finis. Ceci permet de spécifier et implémenter des changements de modes de calculs, qui se distinguent par exemple par les ressources utilisées, la qualité de service fournie, ou le choix d'algorithme remplissant une fonctionnalité. </p> <p>Ces contributions permettent l'utilisation d'outils d'analyse et vérification, tels que la vérification de propriétés d'assignement unique et dépendance acyclique, model checking. L'utilisation de techniques de synthèse de contrôleurs discrets est également traitée. Elles peuvent assurer la correction de faˆ on constructive: à partir d'une spécification partielle du contrôle, la partie manquante pour que les propriétés soient satisfaites est calculée. Grâce à ces techniques, lors du développement de la partie contrôle, la spécification est simplifiée, et le résultat est assuré d'être correct par construction. </p> <p>Les modélisations synchrone et de contrôle reposes sur MARTE et UML. Les travaux de cette thèse sont été partiellement implémentés dans le cadre de Gaspard, dédié aux applications de traitement de données intensives. Une étude de cas est présentée, dans laquelle nous nous intéressont à une application de système embarqué pour téléphone portable multimédia.</p>