Cette thèse propose une nouvelle approche du parallélisme et de la concurrence, posant les bases d'un langage de programmation à la fois sûr et "secure" (garantissant la sécurité des données), fondé sur une sémantique formelle claire et simple, tout en étant adapté aux architectures multi-cœur. Nous avons adopté le paradigme synchrone, dans sa variante réactive, qui fournit une alternative simple à la programmation concurrente standard en limitant l'impact des erreurs dépendant du temps ("data-races"). Dans un premier temps, nous avons considéré un langage réactif d'orchestration, DSL, dans lequel on fait abstraction de la mémoire (Partie 1). Dans le but de pouvoir traiter la mémoire et la sécurité, nous avons ensuite étudié (Partie 2) un noyau réactif, CRL, qui utilise un opérateur de parallélisme déterministe. Nous avons prouvé la réactivité bornée des programmes de CRL. Nous avons ensuite équipé CRL de mécanismes pour contrôler le flux d'information (Partie 3). Pour cela, nous avons d'abord étendu CRL avec des niveaux de sécurité pour les données, puis nous avons défini dans le langage étendu, SSL, un système de types permettant d'éviter les fuites d'information. Parallèlement (Partie 4), nous avons ajouté la mémoire à CRL, en proposant le modèle DSLM. En utilisant une notion d'agent, nous avons structuré la mémoire de telle sorte qu'il ne puisse y avoir de "data-races". Nous avons également étudié l'implémentation de DSLM sur les architectures multi-cœur, fondée sur la notion de site et de migration d'un agent entre les sites. L'unification de SSL et de DSLM est une piste pour un travail futur.

Les centrales hydrauliques de pompage turbinage fonctionnent principalement en utilisant des alternateurs de type synchrone évoluant à vitesse fixe. Cependant, utiliser des alternateurs à vitesse variable et, en particulier, des Machines Asynchrones à Double Alimentation (MADA) apporte des avantages non négligeables : contrôle de la puissance en mode pompe, opération au point de meilleur rendement en mode turbine et plus grande stabilité en cas de perturbation. Cette thèse a pour objectifs la progression des connaissances des phénomènes électromagnétiques régissant le fonctionnement de la MADA et d'établir une démarche en vue de son optimisation. Tout d'abord, un modèle analytique reposant en partie sur la méthode des intégrales de frontière est proposé et validé par simulations éléments finis. Ce modèle analytique prend en compte plusieurs éléments tels que la saturation du circuit magnétique, les harmoniques générés par les bobinages du stator et du rotor mais également les harmoniques dus à la forme non constante de l'entrefer. Ensuite, le modèle est appliqué à l'étude de quatre sujets d'importance pour l'ingénieur électricien : calcul des harmoniques de tension statorique à vide, calcul des pertes fer, calcul des harmoniques de couple et calcul des forces radiales électromagnétiques. Enfin une procédure de dimensionnement de la MADA reposant sur l'optimisation par algorithme génétique est décrite. Cette procédure est appliquée à la transformation d'une machine synchrone existante à pôles saillants en une MADA. Deux cas sont traités : dans un premier temps seul le rotor est remplacé tandis que le stator reste le même, dans un deuxième temps la machine est entièrement redimensionnée.

Le travail présenté dans cette thèse porte sur la conception de logiciels pour systèmes embarqués. Outre les contraintes de programmation provenant des faibles quantité de mémoire et capacité de calcul, ces plates-formes matérielles ne disposent parfois que de peu d'énergie pour fonctionner. Les applications usuelles de ces systèmes imposent de plus des objectifs en matière de réactivité et de durée de vie. Par ailleurs, quelques-unes des ressources fournies sont partagées entre les composants, qu'il s'agisse de l'énergie délivrée par une batterie, ou encore des bus de communication qui les relient. Il est donc nécessaire de pouvoir assurer des propriétés globales portant sur l'ensemble de la plate-forme, telles que le contrôle des accès aux bus, ou encore la maîtrise de la puissance électrique consommée. Cependant, les pilotes des différents périphériques sont d'ordinaire programmés individuellement. La connaissance nécessaire à l'implantation d'une politique de contrôle global est alors distribuée parmi diverses portions du logiciel. Nous exposons une solution au problème du contrôle global des ressources, basée sur une vue centralisée des états des composants matériels de la plate-forme. Bâtie sur un principe de para-virtualisation, notre approche consiste en l'introduction d'une couche de contrôle ; le système d'exploitation invité est adapté afin de communiquer avec le matériel à l'aide de celle-ci. La couche de contrôle incorpore les pilotes des périphériques, conçus à partir d'automates dont les états correspondent aux modes de fonctionnement ou de consommation du composant géré. Un contrôleur est ajouté, dont le rôle est d'assurer les propriétés globales. L'ensemble de ces automates est programmé à l'aide d'un langage synchrone, puis compilé en code séquentiel. Nous proposons une implantation de la couche de contrôle pour une architecture de nœuds de réseaux de capteurs sans fil, qui constitue une plate-forme représentative des systèmes embarqués contraints. Nous évaluons qualitativement et quantitativement ce prototype afin de montrer la viabilité de l'approche. Son impact sur le reste du logiciel est également apprécié, que celui-ci soit construit selon un modèle d'exécution purement événementiel ou multi-fils. Enfin, nous passons en revue plusieurs extensions possibles, et identifions quelques bonnes pratiques pour son usage dans d'autres contextes.

Les approches de parallélisme structuré sont un compromis entre la parallélisation automatique et la programmation concurrentes et réparties telle qu'offerte par MPI ou les Pthreads. Le parallélisme à squelettes est l'une de ces approches. Un squelette algorithmique peut être vu comme une fonction d'ordre supérieur qui capture un algorithme parallèle classique tel qu'un pipeline ou une réduction parallèle. Souvent la sémantique des squelettes est simple et correspondant à celle de fonctions d'ordre supérieur similaire dans les langages de programmation fonctionnels. L'utilisation combine les squelettes disponibles pour construire son application parallèle. Lorsqu'un programme parallèle est conçu, les performances sont bien sûr importantes. Il est ainsi très intéressant pour le programmeur de disposer d'un modèle de performance, simple mais réaliste. Le parallélisme quasi-synchrone (BSP) offre un tel modèle. Le parallélisme étant présent maintenant dans toutes les machines, du téléphone au super-calculateur, il est important que les modèles de programmation s'appuient sur des sémantiques formelles pour permettre la vérification de programmes. Les travaux menés on conduit à la conception et au développement de la bibliothèque Orléans Skeleton Library ou OSL. OSL fournit un ensemble de squelettes algorithmiques data-parallèles quasi-synchrones. OSL est une bibliothèque pour le langage C++ et utilise des techniques de programmation avancées pour atteindre une bonne efficacité. Les communications se basent sur la bibliothèque MPI. OSL étant basée sur le modèle BSP, il est possible non seulement de prévoir les performances des programmes OSL mais également de fournir une portabilité des performances. Le modèle de programmation d'OSL a été formalisé dans l'assistant de preuve Coq. L'utilisation de cette sémantique pour la preuve de programmes est illustrée par un exemple.

Les langages synchrones ont été fondés pour modéliser et implémenter les systèmes réactifs temps-réels critiques. Avec la complexité toujours croissante des systèmes contrôlés, la vitesse d'exécution devient un critère important. Nous sommes donc à la recherche d'une exécution parallèle, combinant efficacité et sûreté.Les langages synchrones ont toujours intégré la notion de parallélisme, mais ce, pour l'expressivité de la modélisation. Leurs compilations visent principalement les circuits ou la génération de code séquentiel. Tous ont une sémantique formelle, qui rend possible la distribution correcte du code. Mais la préservation de cette sémantique peut être un obstacle à l'efficacité du code généré, particulièrement s'il est nécessaire de préserver une notion d'instant global au système.Le modèle sémantique qui nous intéresse est celui des réseaux de Kahn. Ces réseaux modélisent des calculateurs distribués, communiquant au travers de files de taille non bornée. Dans ce cadre, la distribution ne demande aucune communication ni synchronisation supplémentaire. En considérant l'histoire des files de communication, la sémantique de Kahn permet de s'abstraire de l'exécution effective, tout en garantissant le déterminisme du calcul. Pour cela, chaque nœud du réseau doit avoir une sémantique fonctionnelle continue.Le langage que nous développons est Heptagon, un langage synchrone fonctionnel du premier ordre, déscendant de Lustre. Son compilateur est un prototype universitaire, apparenté à l'outil industriel Scade. Grâce à sa sémantique de Kahn, la distribution d'un programme Heptagon ne pose pas de question, son efficacité beaucoup plus.L'efficacité requiert de minimiser les synchronisations. Cela revêt deux aspects non indépendants. Avoir un découplage suffisant des calculs : il y a des délais dans les dépendances entre calculs. Avoir une granularité importante des calculs : un fort ratio temps de calcul sur fréquence de communication. Or la sémantique synchrone et les horloges d'un programme Heptagon reflètent exactement l'inverse. Elles permettent au programmeur de se contenter d'un découplage d'un instant et à chaque instant, au maximum une valeur est calculée. De plus, les instants sont typiquement courts, pour assurer que le système réagit rapidement.Des précédents travaux sur le sujet, nous tirons deux constats.Le premier est que nous souhaitons le contrôle du parallélisme par le programmeur, directement dans le code source. Il doit pouvoir maîtriser à quels instants il y a communication ou synchronisation. La solution que nous proposons dans ce manuscrit est l'utilisation des futures dans Heptagon. Ils fournissent ce pouvoir au programmeur, tout en restant des annotations qui peuvent être supprimées sans changer la sémantique dénotationnelle du programme.Le deuxième constat est que la question de la granularité des calculs est une question profonde, touchant en particulier aux questions de dépendance de données, de choix des horloges et de compilation modulaire. Heptagon, comme ses parents, restreint les réseaux de Kahn qui peuvent être écrits, de telle sorte que ces trois questions se traitent séparément. Pour mieux comprendre le lien entre ces éléments, nous revenons aux réseaux de Kahn. Notre principal résultat est la définition de la sous-classe des réseaux ordonnés réactifs. Ceux-ci sont les seuls pour lesquels nous pouvons décrire modulairement le comportement avec des horloges, sans restreindre les contextes d'appels. Ces réseaux ont une signature d'horloge en forme normale, qui maximise la granularité. Pour l'exprimer, nous introduisons les horloges entières, décrivant la communication de plusieurs valeurs en un seul instant. Nous appliquons ensuite nos résultats pour voir sous un nouveau jour Heptagon, Signal, les politiques des objets de Lucid Synchrone, mais aussi proposer une analyse pleinement modulaire de Lucy-n langage synchrone le plus fidèle aux réseaux de Kahn. / Synchronous languages are used to program critical reactive systems. Today, systems require to find a way to execute them safely and in parallel. Parallelism has always been part of synchronous langages, but for modeling purpose. Their formal semantics allow to distribute them, but preserving the semantics may be ressource costly and prevent good parallel execution.The Kahn networks model is of great interest. It models distributed computers, communicating through unbounded FIFOs, ensuring that the computed values are deterministic, without any need of added synchronization.We develop the langage Heptagon, a first order functional synchronous son of Lustre.The compiler is an academic prototype of the industrial tool Scade. Thanks to its Kahn semantics, it can be distributed. In order to be efficient, one need to maximize the decoupling of computations and maximize the computation granularity. However, synchronous langages allow for very tight computation coupling and usually require thin computation granularity to ensure reactivity of the system.We opt for two research directions. The first one is to give the control of the execution parallelism to the programer. To this mean, we add futures to the source langage Heptagon. They provide control over starting and end of parallel computations, while preserving the functional semantics. Moreover, we provide a compilation for embedded systems, using statically allocated memory. The second one is to study Kahn synchronous semantics to understand data dependencies and maximize granularity of the computations. This touches deeply to the synchronous languages, mixing the usually separated questions of causality and clock calculus. We define the class of reactive ordered Kahn networks. They are the one which may be modularly compiled and whose behavior may be expressed with a clock signature. Moreover, we show that their is a normal form for this signature, maximizing the granularity of the network. To express it, we extend clocks to integer clocks. Then we come back to the synchronous languages we know to understand how to use it. The result is fully used and explained on Lucy-n, the synchronous language closest to Kahn networks.

Le développement du trafic aérien international est une composante majeure de la croissance des échanges internationaux intervenue depuis la seconde guerre mondiale. La traduction terrestre en est le développement des plateformes aéroportuaires. Avec les dérégulations intervenues dans les années 1990 les hubs sont des éléments majeurs de l’espace européen. Ils ont généré des territoires aéroportuaires allant au-delà des limites administratives et domaniales des aéroports ; ceux-ci sont des espaces importants de l’économie de la connaissance et de l’innovation. A ce titre, ils sont des polarités métropolitaines majeures. Nous en avons choisi trois majeures situées sur deux continents : Paris- Charles de Gaulle, Amsterdam- Schiphol et Seoul- Incheon. En raison de leur accessibilité multimodale synchrone, ces aéroports sont parties prenantes de territoires aéroportuaires importants et multifonctionnels. Ils participent sous de formes et des degrés divers à l’économie de la connaissance et de l’innovation et en particulier à ses circulations. / The development of international air traffic is a major component of the international exchanges occurred since the Second World War. The terrestrial translation is the development of airport. With the deregulations occurred in the years the 1990, hubs are major elements of European space. They generated airport territories going beyond the administrative and domanial limits of the airports; those are important spaces of the knowledge and innovation economy. For this reason, they are major metropolitan polarities. We chose three major located out of two continents: Paris Charles de Gaulle, Amsterdam Schiphol and Seoul Incheon... Because of their synchronous multimode accessibility, these airports are recipients of important and multipurpose airport territories. They take part in various forms and degrees in the knowledge and innovation economy and in particular in its circulations

Les approches de parallélisme structuré sont un compromis entre la parallélisation automatique et la programmation concurrentes et réparties telle qu'offerte par MPI ou les Pthreads. Le parallélisme à squelettes est l'une de ces approches. Un squelette algorithmique peut être vu comme une fonction d'ordre supérieur qui capture un algorithme parallèle classique tel qu'un pipeline ou une réduction parallèle. Souvent la sémantique des squelettes est simple et correspondant à celle de fonctions d'ordre supérieur similaire dans les langages de programmation fonctionnels. L'utilisation combine les squelettes disponibles pour construire son application parallèle. Lorsqu'un programme parallèle est conçu, les performances sont bien sûr importantes. Il est ainsi très intéressant pour le programmeur de disposer d'un modèle de performance, simple mais réaliste. Le parallélisme quasi-synchrone (BSP) offre un tel modèle. Le parallélisme étant présent maintenant dans toutes les machines, du téléphone au super-calculateur, il est important que les modèles de programmation s'appuient sur des sémantiques formelles pour permettre la vérification de programmes. Les travaux menés on conduit à la conception et au développement de la bibliothèque Orléans Skeleton Library ou OSL. OSL fournit un ensemble de squelettes algorithmiques data-parallèles quasi-synchrones. OSL est une bibliothèque pour le langage C++ et utilise des techniques de programmation avancées pour atteindre une bonne efficacité. Les communications se basent sur la bibliothèque MPI. OSL étant basée sur le modèle BSP, il est possible non seulement de prévoir les performances des programmes OSL mais également de fournir une portabilité des performances. Le modèle de programmation d'OSL a été formalisé dans l'assistant de preuve Coq. L'utilisation de cette sémantique pour la preuve de programmes est illustrée par un exemple. / Structured parallelism approaches are a trade-off between automatic parallelisation and concurrent and distributed programming such as Pthreads and MPI. Skeletal parallelism is one of the structured approaches. An algorithmic skeleton can be seen as higher-order function that captures a pattern of a parallel algorithm such as a pipeline, a parallel reduction, etc. Often the sequential semantics of the skeleton is quite simple and corresponds to the usual semantics of similar higher-order functions in functional programming languages. The user constructs a parallel program by combined calls to the available skeletons. When one is designing a parallel program, the parallel performance is of course important. It is thus very interesting for the programmer to rely on a simple yet realistic parallel performance model. Bulk Synchronous Parallelism (BSP) offers such a model. As the parallelism can now be found everywhere from smart-phones to the super computers, it becomes critical for the parallel programming models to support the proof of correctness of the programs developed with them. . The outcome of this work is the Orléans Skeleton Library or OSL. OSL provides a set of data parallel skeletons which follow the BSP model of parallel computation. OSL is a library for C++ currently implemented on top of MPI and using advanced C++ techniques to offer good efficiency. With OSL being based over the BSP performance model, it is possible not only to predict the performances of the application but also provides the portability of performance. The programming model of OSL is formalized using the big-step semantics in the Coq proof assistant. Based on this formal model the correctness of an OSL example is proved.

Le travail présenté dans cette thèse porte sur la conception de logiciels pour systèmes embarqués. Outre les contraintes de programmation provenant des faibles quantité de mémoire et capacité de calcul, ces plates-formes matérielles ne disposent parfois que de peu d'énergie pour fonctionner. Les applications usuelles de ces systèmes imposent de plus des objectifs en matière de réactivité et de durée de vie. Par ailleurs, quelques-unes des ressources fournies sont partagées entre les composants, qu'il s'agisse de l'énergie délivrée par une batterie, ou encore des bus de communication qui les relient. Il est donc nécessaire de pouvoir assurer des propriétés globales portant sur l'ensemble de la plate-forme, telles que le contrôle des accès aux bus, ou encore la maîtrise de la puissance électrique consommée. Cependant, les pilotes des différents périphériques sont d'ordinaire programmés individuellement. La connaissance nécessaire à l'implantation d'une politique de contrôle global est alors distribuée parmi diverses portions du logiciel. Nous exposons une solution au problème du contrôle global des ressources, basée sur une vue centralisée des états des composants matériels de la plate-forme. Bâtie sur un principe de para-virtualisation, notre approche consiste en l'introduction d'une couche de contrôle ; le système d'exploitation invité est adapté afin de communiquer avec le matériel à l'aide de celle-ci. La couche de contrôle incorpore les pilotes des périphériques, conçus à partir d'automates dont les états correspondent aux modes de fonctionnement ou de consommation du composant géré. Un contrôleur est ajouté, dont le rôle est d'assurer les propriétés globales. L'ensemble de ces automates est programmé à l'aide d'un langage synchrone, puis compilé en code séquentiel. Nous proposons une implantation de la couche de contrôle pour une architecture de nœuds de réseaux de capteurs sans fil, qui constitue une plate-forme représentative des systèmes embarqués contraints. Nous évaluons qualitativement et quantitativement ce prototype afin de montrer la viabilité de l'approche. Son impact sur le reste du logiciel est également apprécié, que celui-ci soit construit selon un modèle d'exécution purement événementiel ou multi-fils. Enfin, nous passons en revue plusieurs extensions possibles, et identifions quelques bonnes pratiques pour son usage dans d'autres contextes. / This thesis is about the design of software for embedded systems. The hardware platforms usually employed in these systems provide a limited amount of memory, computational power and energy. The software they execute is then constrained by such limited resources. Usual applications involve further objectives, such as reactivity and lifetime. In addition, these platforms comprise shared resources like buses or even the energy provided by a battery. Hence, global properties concerning the whole platform must be enforced, for instance to control concurrent accesses to a bus or power consumption. As device drivers are commonly developed individually, the knowledge necessary to implement global control policies is distributed among several pieces of software. We propose a global control approach, based on a centralized view of the devices' states. Built upon para-virtualization principles, it operates on the hardware/software interface. It involves a simple adaptation of the guest operating system, to communicate with the hardware via a control layer. The control layer itself is built from a set of simple automata: the device drivers, whose states correspond to functional or power consumption modes, and a controller to enforce global properties. All these automata are programmed using a synchronous language, and compiled into a single piece of sequential code. As a suitable representative of embedded systems hardware, we choose the node of a wireless sensor network. To show that our approach is practical, we propose a proof-of-concept implementation of the control layer to manage this platform, and evaluate it both qualitatively and quantitatively. We also demonstrate its use and benefits with an event-driven or multithreading operating system, and estimate the impact of the adaptation on guest software. Finally, we audit several extensions and draw guidelines for its use in other contexts.

Depuis l'essor des ordinateurs et des capacités de calcul, la conception des composants du génie électrique repose largement sur des simulations informatiques et sur des calculs numériques. Dans les systèmes complexes, où de nombreux composants interagissent pour le bon fonctionnement du système, le dimensionnement optimal du composant dépend nécessairement de son environnement systémique. La conception de celui-ci est fortement liée au fonctionnement du système global. La conception intégré du composant dans son environnement systémique permet ainsi de repousser les limites de l'efficacité énergétique, pour des systèmes plus performants et moins consommateurs. En support à ce contexte méthodologique, nous proposons de dimensionner par optimisation un moteur électrique pour un véhicule hybride dans le but d'améliorer l'efficacité énergétique globale du véhicule. Dans ce travail, nous avons modélisé le moteur électrique par un schéma réluctant, et nous proposons deux approches méthodologiques différentes du même problème. Les points clés de notre approches sont : la prise en compte de l'environnement du moteur, du cycle de fonctionnement et de la gestion de l'énergie du système. / Since the development of computers and calculation capacities, the design of electrical components in electrical engineering is widely based on computing simulations and on numeral calculations. In complex systems, where numerous components interact for the working of the system, the optimal sizing of the component deeply depends on its systemic environment. The design of each component is strongly linked to the functioning of the global system. Therefore, the joint design of the component into its systemic environment allows to improve the efficiency of the system. In this methodological context, we optimize an electric machine for a hybrid vehicle. The aim of this work is to improve the global efficiency of the vehicle. In this work, we build a magnetic circuit model, and we propose two approaches for solving the optimization problem. The key points of this work are : the consideration of the environment of the electrical machine, the driving cycle and the energy management of the system.

Le monitoring des écosystèmes terrestres nécessite une connaissance approfondie des interactions entre microorganismes, minéraux et métaux dans les sols. Afin d'évaluer in vivo la disponibilité de métaux tel que le fer dans des systèmes bactéries-minéraux, une approche basée sur l’utilisation de biosenseurs bactériens fluorescents et d’une analyse spectroscopique non-invasive a été explorée. Ce travail a notamment conduit à la construction chez Pseudomonas aeruginosa de fusions génétiques couplant des promoteurs régulés par le fer à des rapporteurs fluorescents multicolores. Les souches obtenues ont été utilisées comme senseur de la disponibilité du fer constitutif de différents minéraux (Nontronites). La réponse de ces biosenseurs bactériens a été étudiée en couplant la spectroscopie de fluorescence à balayage synchrone (SFS) à la décomposition canonique polyadique Candecomp / Parafac (CP). Avec des plans d’expérience privilégiant la diversité des réponses, le couplage SFS-CP garantit une estimation conjointe et rapide de l’expression de plusieurs promoteurs d’intérêts, y compris dans des milieux auto-fluorescents. Cette méthode originale permet, entre autres, de s’affranchir des problèmes liés aux recouvrements spectraux des protéines fluorescentes et fournit une estimation robuste et précise de la réponse des biosenseurs. Appliquée à d’autres plans d’expériences, elle démontre également que la bio-dissolution des nontronites par P. aeruginosa est assurée par la production de sidérophores et contrôlée par la cristallochimie des feuillets des smectites, notamment par la distribution des atomes de fer(III) entre les tétraèdres et les octaèdres / Monitoring terrestrial ecosystems requires a better understanding of the interactions between microorganisms, minerals and metals in the environment. To assess in vivo availability of metals such as iron in bacteria-mineral system, an approach based on whole-cell fluorescent biosensors and non-invasive spectroscopy was explored. This work led to the construction in Pseudomonas aeruginosa of a set of gene fusions coupling iron-regulated promoters to multicolour fluorescent reporters. The recombinant strains were used as sensors of structural iron availability in nontronites NAu-1 and NAu-2. The response of these biosensors was studied by coupling synchronous fluorescence spectroscopy (SFS) with canonical polyadic Candecomp/Parafac (CP) decomposition. On the basis of experimental designs favouring response diversity, the coupled SFS-CP method guarantees a joint estimate of gene expression from multiple promoters, even in highly fluorescent media. This novel method can solve the issue of spectral bleed-through of fluorescent proteins and provides a means to integrate multiple signals from combinations of whole-cell fluorescent bioreporters. In addition, we could show using SFS-CP that P. aeruginosa indirectly mobilize Fe(III) from nontronites primarily through the production of pyoverdine siderophore. The structural Fe(III) present on the edges of NAu-2 rather than NAu-1 particles appears to be more bioaccessible, suggesting that the distribution of Fe, in the tetrahedron and/or in the octahedron sites, governs the solubilization process