Le travail présenté dans cette thèse vise à contribuer à l'analyse des phénomènes magnéto-mécanique et magnéto-thermique à l'aide de la méthode des éléments finis. Généralement, les problèmes magnéto-mécanique et magnéto-thermique sont constitués de plusieurs sous-problèmes dont la nature physique est différente. En utilisant la stratégie du couplage faible , ces sous-problèmes peut être calculés séparément en utilisant la méthode des éléments finis et donc sur leurs propres maillages afin d'assurer la précision. Pour obtenir une solution précise pour l'ensemble du problème multi-physique, il est très important d'assurer la transmission d'informations entre les sous-problèmes. Dans ce travail , nous étudions les méthodes de la projection. Les formulations de la projection sont données pour l'espaces L2 (scalaire et vectoriel), mais aussi pour H(grad), H(rot) et H(div ) afin d'améliorer la précision sur les dérivés. Une méthode de Petrov-Galerkin est présenté pour remplir l'espace test avec une base bi-orthogonale, qui permet de réduire le coût de calcul des projections L2 Ritz-Galerkin. Les techniques d'implémentation sont également exprimées en détails au niveau de la précision, la rapidité et la simplicité de réalisation. Ensuite avec les formulations énergétiques des champs électromagnétiques, des applications de la projection sont démontrées. La précision et l'efficacité de la projection sont données dans les problèmes multi -physiques. La thèse se termine avec les conclusions et des possibilités pour l'avenir. / The work presented in this thesis aims to contribute to finite element analysis of magneto-mechanical and magneto-thermal phenomena. In general, magneto-mechanical and magneto-thermal problems are made up of subproblems of which the physical nature differs. Using weak-coupling strategies, these subproblems can be calculated separately using finite element methods and thus on their own meshes in order to ensure precision. To obtain a precise solution for the entire problem, it is crucial to ensure the transmission of information between the subproblems. In this work, we study field projection methods on overlapping domains. Field projection formulations are given for classical L2 space, as well as for H(grad), H(curl) and H(div) in order to obtain increased projection accuracy for the distributional derivatives. A Petrov-Galerkin method is presented to fill the test space using a bi-orthogonal basis, in order to reduce the computation cost of L2 or L2 Ritz-Galerkin projections. Practical implementation techniques are also discussed in details for the consideration of accuracy, speed and simplicity of realization. Subsequently, with energy-conserving formulations for electromagnetic fields, applications of mesh-to-mesh projections are demonstrated. The accuracy and efficiency of the presented projection methods are given through multi-physics problems. The thesis closes with some conclusions and possibilities for future work.

La propension des systèmes informatiques à subir des défaillances matérielles est à l'origine d'une recherche abondante afin de concevoir des systèmes dits tolérants aux pannes. Le procédé couramment retenu consiste à procéder à des réplications, donnant alors naissance à ce que l'on nomme un système distribué. La question se pose alors de savoir si l'on peut garantir que les multiples copies sont cohérentes entre elles. Ainsi, la recherche d'un accord devient-elle un problème à résoudre, à portée paradigmatique : le Consensus. Or, la complexité des algorithmes de Consensus rend la tache ardue : il n'est donc pas rare que l'on commette des erreurs lors de leur conception. De là découle l'idée, développée depuis plus de trente ans, de recourir à des procédés de vérification mécanique des algorithmes et de leurs preuves de correction. Ces procédés prennent place parmi ce que l'on désigne usuellement comme étant des méthodes formelles. C'est à la croisée des recherches en algorithmique distribuée et en méthodes formelles que se situent nos travaux. Plus spécifiquement, il s'agit de faire usage d'un logiciel de certification formelle, Isabelle/HOL, afin de garantir l'exactitude des preuves de correction d'algorithmes de Consensus exprimés dans un cadre formel uniforme du nom de Heard-Of, proposé en 2009 par Charron-Bost et Schiper. Nous montrons que, du fait de leur expression dans un même cadre formel, et du fait de leur proximité, suivant les cas, soit de conception (nombre de rondes, recours à des mécanismes de vote, ...) soit de forme syntaxique, soit d'hypothèses de fonctionnement (synchronisme partiel, ...), ces algorithmes présentent des preuves dont une part conséquente d?arguments sont communs. Cela permet de copier certains d'entre eux d'une preuve à l'autre, afin de réduire l'effort de certification : ces arguments peuvent alors être automatiquement évalués par la machine pour chacun d'entre eux, l'utilisateur n'ayant à intervenir que là où celle-ci est en peine, c'est-à-dire lorsque les différences algorithmiques induisent qu'il faille réviser les détails de l'argumentation. L'exposé que nous faisons de la certification que nous avons effectuée pour six algorithmes distribués dédiés à la résolution du problème du Consensus illustre cette démarche. Par conséquent, nous présentons d'abord les portions communes des démonstrations, puis détaillons ce qui est propre à chacune, l'objectif n'étant pas de permettre une lecture linéaire de chaque démonstration mais de mettre en évidence notre proposition / Computer systems fail. Whatever the reason of these failures, it has been a widespread approach to try and increase the faults-tolerance of a computer system through its replication. The resulting system is said to be a distributed one, in which replicas have to be kept consistent with each others. Hence, reaching agreement, and Consensus in particular, becomes the problem to solve - indeed, the paradigm. Solving Consensus (under various assumptions) is a hard task : algorithms designed on this purpose are subtle and proving their being correct is error-prone - whenever they are, which occasionally appears not to be the case. For more that thirty years, researchers interested in what is called Formal Methods have been working on mechanizing the verification process, in order to increase confidence in the correctness of (distributed) algorithms. The work we present here is at the intersection of distributed algorithms and formal methods. We use the Isabelle/HOL software to certify the correctness proof of various Consensus algorithms expressed in a uniform framework based on the Heard-Of Model, introduced by Charron-Bost and Schiper in 2009. Expressed in a common model, these algorithms, which, depending on the case, share some common mecanisms (number of steps, intermediate votes, ...), some elements of syntax, or types of assumptions (partial synchronism...), can be proved using some common arguments. As a consequence, the certification effort can be reduced by copying some intermediate lemmas from one proof to another and let the computer automatically parse them until some manual adaptation is required. This lead to the idea of certifying the correctness of multiple algorithms all together, instead of proving them one after the other, as one would do on paper in a traditional way. The effort of translation in the formal language of the proof assistant is then possibly reduced. Of course, each proof will also contain specific arguments, which will have to be isolated and translated into the software. Here, we illustrate this proposition through the presentation of formal certificates of correctness for six Consensus algorithms. As a consequence, on should not expect to find here a comprehensive linear presentation of each proof : we first show the arguments shared by multiple proofs, followed by those which are specific to each o them

Les utilisateurs s'attendent à ce que les logiciels soient à la fois continuellement disponibles et mis-à-jour à la volée. L'introduction de nouvelles fonctionnalités et l'intégration de correctifs ne doit pas perturber la bonne marche d'une application. Les développeurs bénéficient aussi de la modification dynamique des logiciels en adaptant le code à de nouvelle situations ou bien an exécutant des analyses dynamiques à des fins de monitorage, de déboguage et d’optimisation. Les langages de programmation doivent donc fournir aux développeurs des mécanismes qui améliorent l'adaptabilité logicielle. Dans le même temps, l'augmentation de la taille et de la complexité des logiciels requièrent des applications faites de nombreux composants développés par différents groupes. Dans ce contexte chaque composant doit être convenablement protégé des autres. Les langages de programmation doivent donc aussi fournir des mécanismes qui améliorent l'encapsulation. Le besoin de supporter des adaptations dynamiques d'un côté, et le besoin d'avoir des composants convenablement confinés d'un autre, poussent la conception des langages de programmation dans deux directions opposées: soit plus de flexibilité, soit plus de contrôle. Cette dissertation étudie cette tension dans le contexte des langages orientée-objet dynamiquement typés via deux mécanismes qui promeuvent l'adaptabilité logicielle: la réflexion et les méthodes d’extension. Pour chacun de ces mécanismes, nous démontrons leur utilité, leurs effets néfastes sur l'encapsulation et proposons des solutions qui conservent leurs forces tout en maintenant l'encapsulation. / Users expect modern software to be both continually available and updated on the fly. Introduction of new features and integration of bug fixes should not trouble the smooth running of an application. Developers also benefit from dynamic modifications of software by adapting code to new unanticipated situations or by running dynamic analyses to get feedback about the behavior of running applications for monitoring, debugging and optimization purposes. Programming languages should thus provides developers with mechanisms that improve software adaptability. At the same time, the increasing size and complexity of software call for applications made up of many interacting components developed by different parties. In this context, each component needs to be properly protected from other ones. Programming languages should thus provide developers with mechanisms that improve encapsulation. The need for dynamic adaptations on the one hand and the need for properly confined components on the other hand pulls programming language design in two opposite directions: either more flexi-bility or more control.This dissertation studies this tension in the context of dynamically-typed object-oriented languages with two language mechanisms that promote software adaptability: reflection and extension meth-ods. For both mechanisms, we demonstrate their usefulness, their harmful effect on encapsulation and propose solutions to retain their power while maintaining encapsulation.

Safety-critical systems depend on the fact that their software components provide services that behave correctly (i.e. satisfy their requirements). Additionally, in many cases, these systems have to be adapted or reconfigured in case of failures or when changes in requirements or in quality of service occur. When these changes appear at the software level, they can be handled by the notion of substitution. Indeed, the software component of the source system can be substituted by another software component to build a new target system. In the case of safety-critical systems, it is mandatory that this operation enforces that the new target system behaves correctly by preserving the safety properties of the source system during and after the substitution operation. In this thesis, the studied systems are modeled as state-transition systems. In order to model system substitution, the Event-B method has been selected as it is well suited to model such state-transition systems and it provides the benefits of refinement, proof and the availability of a strong tooling with the Rodin Platform. This thesis provides a generic model for system substitution that entails different situations like cold start and warm start as well as the possibility of system degradation, upgrade or equivalence substitutions. This proposal is first used to formalize substitution in the case of discrete systems applied to web services compensation and allowed modeling correct compensation. Then, it is also used for systems characterized by continuous behaviors like hybrid systems. To model continuous behaviors with Event-B, the Theory plug-in for Rodin is investigated and proved successful for modeling hybrid systems. Afterwards, a correct substitution mechanism for systems with continuous behaviors is proposed. A safety envelope for the output of the system is taken as the safety requirement. Finally, the proposed approach is generalized, enabling the derivation of the previously defined models for web services compensation through refinement, and the reuse of proofs across system models.

L'objet de cette thèse est le développement de méthodes variationnelles pour l'étude des solutions presque-périodiques au sens de H. Bohr et au sens de Besicovitch de quelques classes d'équations différentielles ordinaires du second ordre à retard. Pour cela on utilise le Calcul des Variations en Moyenne Temporelle. Dans un premier temps on étudie une classe d'équations différentielles du type neutre, puis une classe d'équations différentielles à retard fini, enfin on s'intéresse à une classe d'équations différentielles à retard infini.

Cette HDR est dédiée à l'étude du management de l'innovation. Elle est orientée autour de trois axes : la complémentarité entre innovations technologique et organisationnelle, l'organisation de la propriété industrielle et une réflexion sur les méthodologies qualitatives en sciences de gestion.

Mes recherches au Commissariat à l'Énergie Atomique concernent principalement la modélisa- <br />tion mathématique et la simulation numérique pour la physique des plasmas. Ce mémoire présente <br />mes contributions dans ce domaine.

Les travaux présentés dans cette thèse portent sur la planification de tâches pour des systèmes robotiques qui prennent en compte des contraintes géométriques, cinématiques et symboliques. Nous souhaitons notamment traiter des problèmes nécessitant la manipulation et l'assemblage d'objets par plusieurs robots mobiles manipulateurs dans un environnement contraint. Dans le cadre de cette thèse nous avons développé un planificateur nommé "aSyMov" qui offre un cadre innovant pour combiner les techniques issues de la planification de mouvements et de la planification de tâches. Dans un premier temps nous faisons un état de l'art des techniques de la planification de mouvements. Puis une nouvelle représentation de l'espace de recherche et de nouvelles techniques de planifications seront développées afin de généraliser et de combiner les algorithmes décrits dans l'état de l'art. Dans un second temps nous abordons les techniques de la planification de tâches et définissons une manière originale de lier le domaine géométrique au domaine symbolique. Puis nous présentons l'architecture et les algorithmes de notre planificateur. ASyMov effectue une recherche en avant dans l'espace d'état. L'état d'aSyMov a la particularité de représenter l'ensemble des instanciations géométriques possibles pour un état symbolique donné. La procédure de validation des actions va essayer de minimiser les instances géométriques à vérifier. Ce ne sera que quand les actions vont contraindre la géométrie qu'une propagation arrière de ces contraintes sera faite pour trouver de nouvelles instances valides. Nous décrivons aussi comment il est possible de combiner à la fois l'apprentissage de la topologie de l'environnement et la recherche d'une solution avec les connaissances déjà acquises. Pour finir nous présentons plusieurs problèmes complexes qui ont été résolus par aSyMov.

Le traitement des systèmes pleins issus de modélisation d'interactions de type particulaires est un problème lourd que les méthodes multipôles proposent d'optimiser grâce à des approximations hiérarchiques basées sur la régularité des potentiels sous-jacents. Cette thèse offre des développements sur une nouvelle méthode multipôle pour l'électromagnétisme à la fois en terme d'un traitement unifié de l'ensemble des fréquences et informatique dans le cadre du paralléélisme et d'optimisations algorithmiques telles que le partitionnement par graphes et le recouvrement des communications par des calculs.

En 1993, le professeur C. Rubbia fait une première proposition concernant un réacteur souscritique piloté par un accélérateur de particules. En 1995 le concept de l'amplificateur d'énergie est développé, les caractéristiques principales de ce réacteur sont alors, outre la sous-criticité intrinsèque du réacteur nucléaire: l'utilisation de la filière thorium-232 - uranium-233 et l'utilisation du plomb comme source de spallation, comme milieu ralentisseur et comme fluide caloporteur. Ce système a un objectif double, celui de produire de l'énergie et celui de transmuter les produits de fission radioactifs à durée de vie longue tel le technétium-99. Ce travail de thèse s'intéresse plus particulièrement à l'étude des propriétés de transport des neutrons dans le plomb en vue de la transmutation des produits de fission à durée de vie longue. La première partie s'attache à la description du dispositif expérimental de l'expérience TARC. Des approches théoriques et numériques permettent de se familiariser avec les propriétés de transport des neutrons et leur lent ralentissement dans le plomb. La deuxième partie porte sur la détermination expérimentale, par le groupe de l'ISN de Grenoble, de la distribution énergétique et spatiale du flux de neutrons dans l'ensemble du bloc de plomb. Cette distribution est comparée aux résultats des simulations numériques et aux mesures collectées par les différents systèmes de détection utilisés en parallèle au sein de la collaboration. La troisième et dernière partie valide le concept de la traversée adiabatique des résonances de capture, pour la transmutation des produits de fission à durer de vie longue, dans le plomb. L'ensemble des résultats de la deuxième et de la troisième partie repose sur la relation liant l'énergie des neutrons à leur temps de ralentissement dans le plomb.