Ce travail a pour objectif de développer des techniques de surveillance non-invasives sur des machines électriques tournantes de sorte que leurs mises en place soient aisées en environnement industriel. A cet effet, deux méthodes indépendantes sont décrites dans ce mémoire : un diagnostic de défaillances électriques dans des alternateurs connectés au réseau et une étude exploratoire afin d'évaluer la température interne de machines électriques industrielles.La première méthode repose sur l'analyse de deux grandeurs physiques : le champ magnétique rayonné à l'extérieur de la carcasse et les vibrations de la machine tournante. Des modèles mathématiques ont été développés afin de corréler des phénomènes magnétiques et mécaniques qui interviennent dans trois états de la machine : sain et en deux défauts de courts-circuits au stator et au rotor. Ces résultats ont ensuite été validés expérimentalement en laboratoire ainsi que sur des machines de grande puissance en environnement industriel. Un prototype de diagnostic capable de réaliser un examen de défaillance de courts-circuits sur des machines à fort courant a été proposé.Dans un deuxième temps, la méthode d'estimation de la température s'appuie sur des constats relatifs à la variation des caractéristiques des matériaux qui composent un enroulement lorsque la température augmente. Ainsi, la localisation des fréquences de résonances de l'impédance sont impactées. Ce dernier constat a été vérifié expérimentalement.Ce travail de thèse a permis de vérifier la faisabilité des méthodes de diagnostic et de surveillance en ligne dans des machines tournantes avec un minimum d'intrusivité, ceci dans un environnement industriel. / This work aims to develop non-invasive monitoring techniques on AC rotating machines so that their implementation is easy in an industrial environment. For this purpose, two independent methods are described: a fault diagnosis in alternators connected to the local power gird and an exploratory study to evaluate the internal temperature of AC rotating machines.The first method relies on the analysis of two physical magnitudes: the stray magnetic field radiated outside from the external frame and the vibrations content of machine structure. Mathematical models have been developed in order to correlate magnetic and mechanical phenomena which occur in three different machine states: healthy and in two winding short-circuit faults both in the stator and in the rotor. These results were then validated experimentally in laboratory as well as on large machines in industrial environment. A first diagnostic prototype is presented capable to be implemented in industrial environment in order to detect short-circuit faults in larges alternators.In a second time, a temperature estimation method is proposed based on observations concerning variations in material characteristics of windings as temperature increases. Thus, the localizations of impedance resonant frequencies are impacted, which was verified experimentally as well.This thesis work allowed to verify diagnostic feasibility and on-line monitoring methods in rotating machines in a non-invasive way in industrial environments.

La commande prédictive de type Model Predictive Control (MPC) s’est imposée au fil du temps dans de nombreux domaines industriels. Elle permet en effet d’optimiser avec succès les performances du système contrôlé tout en respectant de nombreuses contraintes propres à l’application visée. Cependant, l’utilisation de la commande MPC dans les domaines de la commande de moteurs et de générateurs demeure problématique. En effet, ces applications à forte dynamique imposent de choisir de faibles périodes d’échantillonnage, or, ce type d’algorithme demande de résoudre pour chaque période d’échantillonnage un problème d’optimisation complexe. Cette difficulté est renforcée car le champ applicatif visé portant sur les applications embarquées aéronautiques où la vitesse de base des machines électriques est très élevée, de même que leur fréquence d’alimentation. De plus, du fait que les systèmes étudiés sont embarqués, il est également très important de minimiser les pertes énergétiques de l’ensemble convertisseur-machine. Dans ce contexte la commande prédictive par approche MPC peut être d’un grand intérêt. De plus, ce type d’application intègre des contraintes supplémentaires liées à l’environnement sévère dans lequel évoluent ces systèmes, contraintes additionnelles de fiabilité qu’il faut bien sûr ajouter dans l’algorithme de commande prédictif. La conséquence immédiate sera de renforcer la complexité des algorithmes et donc rendre plus difficile l’implantation en temps réel. Cependant, les gains attendus en termes de performance et de fiabilité sont importants. Le sujet proposé demande ainsi dans une première partie, de synthétiser une loi de commande prédictive d’un actionneur synchrone aéronautique. Une mission type sera choisie et l’optimisation portera à la fois sur le niveau des performances du contrôle que la minimisation de la dépense énergétique. Par ailleurs, une étude de robustesse sera menée qui prendra en compte l’impact de l’environnement de l’actionneur. L’aspect robustesse sera ainsi intégré à l’étude de la commande. La seconde partie du travail portera sur le portage de l’algorithme sur cible FPGA. Une attention toute particulière sera apportée à la minimisation du temps de calcul sans détérioration des performances, le tout sous contrainte de place. Il faudra privilégier une architecture de type Système-sur-Puce qui allie la flexibilité d’un ou plusieurs cœurs processeurs et de modules matériels dédiés à l’accélération de certaines parties critiques du traitement. / Nowadays, Model Predictive Control (MPC) has emerged in many industrial fields. It allows the optimization of the controlled drive performances while respecting a number of constraints specific to the application. However, the use of MPC in the fields of motors and generators control remains problematic. Indeed, these highly dynamic applications require small sampling periods. However, these types of algorithms necessitate the resolution of complex optimization problems at each sampling period. These difficulties are reinforced in our case as the chosen field is the aeronautical embedded applications where the drive speed, as well as the frequency, is important. In addition, as the systems are embedded ones, it is important to minimize the overall energy losses of the inverter-drive system. In this context, the Model Predictive Control can be of great interest. Moreover, this type of applications integrates additional constraints related to the harsh environment in which the systems evolve, such as the reliability, which must be added in the predictive control algorithm. The immediate consequence of these constraints results in an increase of the complexity of the algorithms and therefore it becomes more difficult to implement in real time. However, the expected gains in performance and reliability are important. The proposed subject requires in the first part, to synthesize a predictive control law of an aeronautical synchronous drive. A typical mission will be selected and the optimization will be performed on both the performance level of the control and the minimization of the energy cost. Furthermore, a robustness study is to be conducted that takes into account the environmental impact of the motor drive. The second part will be on the implementation of the algorithm on FPGA target. Particular attention will be paid to minimizing the computational time without any degradation in the performances. Focus will be upon architectures of the type System-on-chip (SoC) that combines the flexibility of one or more processor cores and dedicated hardware modules for accelerating critical parts of the treatment.

Intuitivement, une simulation graphique (monde virtuel, jeu,...) peut etre vue comme un espace borne dans lequel plusieurs entites, disposant chacune d'un comportement propre, evoluent en parallele. Il parait donc naturel d'utiliser des langages concurrents pour programmer ces comportements. Cependant, c'est rarement le cas pour des raisons de complexite de programmation et de deboguage, de non-determinisme et d'efficacite. Nous proposons d'utiliser l'Approche Reactive introduite par F. Boussinot qui permet de definir clairement les comportements d'entites graphiques. Nous avons enrichi les Icobjs qui est un modele d'objets reactifs graphiques. Il offre la possibilite a des non-specialistes de construire graphiquement des comportements complexes a partir de comportements simples et de constructeurs graphiques. Nous avons realise une implementation dont l'objet central est Icobj. Il definit une structure minimale dynamiquement extensible pour permettre une construction graphique generique. Un icobj particulier, le Workspace, execute et affiche les icobjs qu'il contient. Les comportements sont executes par un moteur reactif dedie aux Icobjs appele Reflex. Il reprend les principales primitives du formalisme Junior en modifiant la semantique de certaines instructions et en y ajoutant de nouvelles. Toutes les instructions sont formalisees par des regles de reecritures au format SOS. De plus, nous avons developpe un environnement qui permet d'interagir dynamiquement avec les simulations. Enfin, nous presentons quelques experimentations autour de l'utilisation des Icobjs dans le cadre de simulations distribuees, de simulations physiques ou de simulations multi-horloges.

Ce travail porte sur le test structurel des programmes réactifs synchrones érits en Lustre et sur la définition de critères de couverture pour assurer ce test structurel. Lustre est un langage réactif synchrone flot de données, largement utilisé pour la spécification et la programmation des applications critiques dans des domaines comme l'aéronautique, l'énergie ou les transports. L'application à Lustre des critères de couverture usuels basés sur le flot de contrôle (couverture des instructions, couverture des branches,...) n'est pas significative. <br /><br />Nous avons, en conséquence, défini une hiérarchie de critères adaptés au paradigme flot de données synchrone. Les critères permettent de mesurer la couverture des chemins dans un réseau d'opérateurs. Un réseau d'opérateurs est une modélisation graphique des flots de données dans un programme Lustre. Les critères sont basés sur le calcul symbolique des conditions d'activation de ces chemins. <br /><br />Un outil nommé Lustructu, a été réalisé pour mesurer la couverture atteinte par un jeu de tests selon ces critères. Lustructu analyse le programme sous test et calcule les chemins et leurs conditions d'activation. L'évaluation de la couverture par Lustructu est non-intrusive (pas d'instrumentation du code). L'applicabilité et la pertinence des critères ont été évaluées sur une étude de cas significative issue du secteur de l'aéronautique.

Le travail décrit dans cette thèse s'inscrit dans le contexte du développement et de la validation des systèmes réactifs synchrones. Il vise à tirer parti de certaines formes de structuration des programmes durant le processus de développement et de validation. Nous étudions premièrement l'utilisation d'opérateurs réguliers de types "itérateurs" qui permettent d'exprimer assez facilement des programmes réguliers manipulant des tableaux. Nous montrons aussi comment, au moment de la validation, on peut tirer partie de ces structures régulières pour rendre la preuve d'une propriété plus<br />simple. Nous nous intéressons ensuite à la spécification dite "par contrat" où un couple (assume, guarantee) est associé à chaque composant pour spécifier les hypothèses sur l'environnement et les<br />propriétés satisfaites par le composant sous ces hypothèses. Nous montrons l'intérêt de tels contrats à la fois en terme de spécification et de vérification pour le cas particulier des systèmes synchrones.<br />Nous proposons une série d'algorithmes de transformations de programmes (aussi bien autour de l'utilisation des itérateurs que des contrats) utilisable comme pre-processeur d'objectifs de preuve pour les outils de validation. Nos propositions, notamment sur l'aspect langage des itérateurs, ont répondu à des besoins rencontrés dans les applications industrielles, particulièrement autour du langage Lustre, auquel nous appliquons nos résultat. Ces propositions seront bientôt incluses dans la version industrielle du langage.

Notre thèse se situe dans le domaine des méthodes formelles appliquées aux systèmes réactifs. Nous modélisons et traitons ces systèmes, en continuelle interaction avec leur environnement, grâce au langage<br />synchrone Lustre.<br /><br />D'abord, sur la base d'un travail précurseur, nous établissons pour Lustre une méthode de preuve inductive des propriétés de sûreté. Cette méthode est optimisée, afin de prendre en compte au mieux la dynamique des systèmes. Elle est implémentée dans un outil de preuve, Gloups.<br /><br />Ensuite, suivant le modèle de la méthode B, nous définissons un calcul de raffinement pour Lustre. Ce calcul est à la fois adapté à Lustre et exprimé en ce langage. Les obligations de preuve qui assurent la<br />correction du raffinement peuvent être traitées par Gloups. Pour faciliter le développement, un autre outil, Flush, génère automatiquement les obligations pour Gloups.<br /><br />Ainsi, nous utilisons Lustre à la fois comme langage de programmation et comme cadre formel d'un développement maîtrisé. L'intérêt de ce<br />procédé réside dans la simplicité du langage et dans son adaptation aux systèmes réactifs : en ce domaine, notre méthode de raffinement est suffisamment expressive, sans être inutilement compliquée. Des exemples viennent démontrer l'intérêt de la méthode.

Ce travail aborde le problème de la validation de spécifications de services téléphoniques et notamment la recherche d'interactions entre services. Une interaction correspond à la modification du comportement d'un ou plusieurs services, du fait de la coexistence des services. L'interaction est un obstacle majeur au développement de l'offre de services de télécommunications. La validation de spécifications requiert une modélisation des services et du réseau sous-jacent. Nous proposons une méthode de spécification formelle et de validation de services. Celle-ci est basée sur l'utilisation d'un formalisme synchrone pour la modélisation et la spécification, et sur la mise en oeuvre de méthodes de test pour la validation. Nous avons à cette fin proposé une méthode de test adaptée au problème. Cette méthode a été intégrée à Lutess, un environnement de test fonctionnel de systèmes réactifs synchrones, reposant sur un principe de génération de données dynamique et aléatoire. Elle est basée sur la notion de "guidage par schémas". Un schéma représente une classe de comportements de l'environnement du système sous test, comportements que l'on souhaite tester principalement, soit parce qu'ils sont réalistes, soit parce qu'ils conduisent à une situation estimée critique. Cette méthode a été formalisée, puis validée expérimentalement dans plusieurs études de cas conséquentes, en particulier lors du premier concours de détection d'interaction proposé en marge de la conférence "Feature Interaction Workshop", qui a consacré Lutess "Meilleur outil pour la détection d'interactions".

Le mémoire décrit une méthode de modélisation et de validation de composants micro-programmes pour l'implantation de protocole de communication de réseaux. Cette mèthode a été développée dans le cadre de la conception du composant FICOMP qui met en oeuvre la norme de bus de terrain FIELDBUS. Le premier chapitre décrit le contexte industriel du projet FICOMP, les différents niveaux de spécification du composant et les outils de simulation et de vérification utilisés. Le chapitre deux présente le langage VOVHDL, une extension de VHDL pour la spécification des communications et des synchronisations entre processus concurrents, et en donne une sémantique synchrone en termes de systèmes à transitions étiquetées. Le chapitre trois présente une approche de modélisation pour les descriptions VOVHDL hiérarchiques, et en illustre l'application au composant FICOMP : les modules internes sont reliés à un module de communication pour former un module de niveau supérieur ; ce module est alors traduisible dans le format d'entrée de l'outil de vérification ASA+. Le chapitre quatre rappelle les primitives essentielles du langage VHDL, et formalise la sémantique de simulation de ce langage en termes de systèmes à transitions étiquetées. Les annexes détaillent l'application de la méthode, par la spécification et la traduction dans le modèle propose de deux modules du projet FICOMP

Dans les machines parallèles les performances des programmes posent de manière cruciale le problème de l'efficacité des communications dans les réseaux d'interconnexion des processeurs d'une machine sans mémoire commune. Les communications point-à-point ne sont qu'un cas très particulier des schémas de communications complexes utilisés par les applications. Les communications globales, basées sur la construction correcte de protocoles à diffusion, sont une classe de ces schémas de communication. Ce problème comprend deux aspects : l'acheminement des messages pour la diffusion et la construction de protocoles de communication/synchronisation inter-processus. Nous considérons d'abord le problème de l'acheminement pour la diffusion, que nous construisons à partir d'une fonction de routage correcte pour des réseaux généraux de topologies quelconques. La famille d'algorithmes de diffusion obtenus s'adapte à la fois à la représentation de la fonction de routage, et à la topologie d'interconnexion entre processeurs. Un aspect de l'efficacité des algorithmes produits est l'espace mémoire nécessaire à une telle fonction de routage à diffusion. Nous développons des algorithmes qui requierent un espace mémoire constant et qui de plus, en utilisant une représention par intervalles de la fonction de routage, peuvent être intégrés dans un circuit routeur. Nous nous intéressons ensuite à la construction de divers types de protocoles à diffusion (synchrone et asynchrone) et proposons une machine virtuelle parallèle à diffusion (PDVM). Cette machine virtuelle s'inscrit dans l'architecture du micro-noyau pour systèmes parallèles ParX, développé par notre équipe, qui offre un support d'exécution générique pour de multiples machines virtuelles. PDVM se présente sous la forme de deux de protocoles nécessaires à l'élaboration de la plupart des schémas de communication par diffusion. L'interface d'accès à ces protocoles permet de gérer des groupes de processus à diffusion toujours cohérents. Dans sa conception cette machine virtuelle est un support minimal pour implémenter efficacement et correctement les diverses interfaces et bibliothèques de communications globales pour les standards de programmation parallèle qui émergent (PVM, MPI, etc.). L'ensemble des solutions proposées a été intégré dans le prototype de ParX; et leurs résultats d'évaluation de performances sont produits.

AADL est dédié à la conception de haut niveau et l'évaluation de systèmes embarqués. Il permet de décrire la structure d'un système et ses aspects fonctionnels par une approche à base de composants. Des processus localement synchrones sont alloués sur une architecture distribuée et communiquent de manière globalement asynchrone (système GALS). Une spécificité du modèle polychrone est qu'il permet de spécifier un système dont les composants peuvent avoir leur propre horloge d'activation : il est bien adapté à une méthodologie de conception GALS. Dans ce cadre, l'atelier Polychrony fournit des modèles et des méthodes pour la modélisation, la transformation et la validation de systèmes embarqués. Cette thèse propose une méthodologie pour la modélisation et la validation de systèmes embarqués spécifiés en AADL via le langage synchrone multi-horloge Signal. Cette méthodologie comprend la modélisation de niveau système en AADL, des transformations automatiques du modèle AADL vers le modèle polychrone, la distribution de code, la vérification formelle et la simulation du modèle polychrone. Notre transformation prend en compte l'architecture du système, décrite dans un cadre IMA, et les aspects fonctionnels, les composants logiciels pouvant être mis en œuvre en Signal. Les composants AADL sont modélisés dans le modèle polychrone en utilisant une bibliothèque de services ARINC. L'annexe comportementale d'AADL est interprétée dans ce modèle via SSA. La génération de code distribué est obtenue avec Polychrony. La vérification formelle et la simulation sont effectuées sur deux études de cas qui illustrent notre méthodologie pour la conception fiable des applications AADL.