Une entreprise industrielle n'est compétitive que si elle offre des produits satisfaisant à diverses exigences qualitatives (qualité, délai de livraison, variété, etc.) et en même temps à des exigences de coûts. Les travaux présentés dans ce mémoire s'intéressent simultanément à l'aspect production et à l'aspect financier d'une entreprise. Ce travail a deux objectifs principaux. Premièrement, la réalisation d'un modèle de simulation d'entreprises industrielles, SIM'l, dans lequel on modélise un système de production et son environnement. Cette maquette permet de construire une démarche pédagogique liée aux problèmes de l'intégration productique. Le principal apport de la maquette est de montrer l'intérêt d'une gestion conjointe des différentes fonctions d'une entreprise industrielle à savoir les approvisionnements, la comptabilité, le marketing et la production. La simulation détaillée de la production permet de montrer les conséquences des décisions et des aléas de la production sur les Résultats économiques de l'entreprise. Deuxièmement, la hiérarchisation des décisions et l'étude des performances d'une entreprise industrielle. L'application de méthodes d'analyse de données nous a permis de déterminer les niveaux de décision et de dégager les indicateurs les plus représentatifs caractérisant les performances du système à chaque niveau de décision. Les résultats obtenus montrent qu'une étude globale d'une entreprise industrielle (modélisation, simulation et évaluation des performances) dans laquelle sont pris en compte des indicateurs économiques peut être menée et peut aider à une bonne gestion à moyen et court terme.

Les mécanismes de dégradation des composites stratifiés sont aujourd'hui très bien connus mais la simulation jusqu'à rupture reste un challenge majeur. Un nouveau modèle de calcul microscopique hybride a récemment été proposé et permet de prendre en compte tous les modes de dégradations des stratifiés. Le modèle microscopique est hybride et couple à la fois des mécanismes discrets et continus. Celui-ci s'appuie sur l'introduction de surfaces de rupture minimales conférant ainsi au modèle un aspect discret. Un milieu continu endommageable est introduit pour modéliser les dégradations continues à l'échelle du pli. Très simple d'interprétation et reposant sur peu de quantités matériaux à identifier, le modèle n'est viable que s'il est associé à des moyens de calcul performants. Une stratégie multiéchelle avec homogénéisation en espace développée depuis plusieurs années est ici étendue pour traiter des problèmes complexes tridimensionnels et incluant de nombreuses surfaces de contact. Des développements spécifiques associés à la réduction du coût de calcul (taille du problème à résoudre et temps de résolution) ont été menés sur des exemples simples bidimensionnels. Le calcul du critère permettant la propagation des fissures a nécessité également des simplifications importantes. Ces différents points ont été mis en œuvre dans un code de calcul complet écrit en langage C++ dans la plateforme du LMT permettant de traiter des problèmes complexes non-linéaires bidimensionnels ou tridimensionnels et pouvant inclure les effets de l'environnement. Des exemples simples sont réalisés et permettent de simuler des scénarios de dégradation complexes.

Le coupleur de puissance utilisé pour les cavités supraconductrices de la section haute énergie du Linac de EUROTRANS doit transférer 150kW de puissance RF au faisceau de protons. Les pertes RF par effet Joule et diélectriques dans les différents éléments du coupleur (conducteur interne, conducteur externe et fenêtre) opérant à cette puissance sont relativement élevées. Par conséquent, il est nécessaire de le refroidir efficacement afin d'assurer un fonctionnement stable et fiable du système d'accélération (coupleur–cavité). Après avoir évaluer toutes les pertes dans le coupleur, les calculs thermiques et les résultats des simulations numériques ont permis de dimensionner et valider le circuit de refroidissement du conducteur interne. Nous avons également conçu, dimensionné et optimisé le circuit de refroidissement du conducteur externe en spécifiant ses caractéristiques hydrauliques et thermiques. Ensuite, nous avons mis en oeuvre et réalisée avec succès une expérience dédiée à l'étude de l'interaction thermique entre la cavité et le coupleur de puissance. Le principal résultat de cette expérience est la mesure expérimentale de la charge thermique critique que peut supporter la cavité sans dégradation sensible de ses performances RF. La valeur de la charge thermique critique mesurée, qui est comprise entre 3W et 5W, constitue un critère essentiel pour qualifier les performances de l'échangeur du conducteur externe qui utilise l'hélium supercritique comme fluide réfrigérant. Enfin, une station d'essai, destiné à la qualification de l'échangeur du conducteur externe dans des conditions similaires à celles de son fonctionnement dans le cryomodule, a été conçue et réalisée avec succès. Les résultats expérimentaux ont montré les excellentes performances thermiques de l'échangeur pour un fonctionnement à une puissance RF de l'ordre de ~750kW soit plus que cinq fois la puissance RF nominale 150kW. En effet, Le flux résiduel maximum mesuré pour une charge thermique de 127W, simulant les pertes RF dans le coupleur, est de 60mW. Par ailleurs, la comparaison entre les températures mesurées et calculées à l'aide d'un modèle thermique 2D axisymétrique a permis d'identifier un coefficient d'échange global pour différents débits. Enfin, une étude expérimentale préliminaire sur les instabilités thermohydrauliques de l'hélium supercritique, a été menée. Ainsi nous avons pu établir un diagramme de stabilité basé sur des paramètres adimensionnels. Ce diagramme montre clairement que nos données expérimentales sont en accord et complètent les données d'autres expériences similaires.

De plus en plus de calculs de surveillance, contrôle etc. sont effectués de façon logicielle. Notre objectif est de prouver formellement des calculs numériques qui offrent déjà un premier niveau de garantie sur leurs résultats, comme des calculs par intervalles, et en particulier des calculs avec des modèles de Taylor.<br /><br />Cette thèse présente la construction d'une bibliothèque de modèles de Taylor pour l'assistant de preuves PVS. Nous avons développé les modèles de Taylor pour les opérations d'addition, soustraction, multiplication par un scalaire, multiplication, élévation au carré, puissance et racine carrée. Nous avons également développé les modèles de Taylor pour l'exponentielle, le sinus, l'arctangente et les sinus et cosinus hyperboliques. Nous avons démontré dans PVS que les opérations et fonctions définies dans notre bibliothèque préservent la propriété d'inclusion, travail de preuve qui n'avait pas été fait auparavant dans les implantations des modèles de Taylor.<br /><br />Nous avons développé une stratégie PVS pour certifier des inégalités ou bornes d'expressions. Quand on utilise un assistant de preuves pour démontrer une inégalité, il peut être nécessaire de guider l'assistant pas à pas dans la démonstration. Pour cette raison, les utilisateurs effectuent rarement la démonstration. Par conséquent, simplifier la façon de prouver les inégalités et bornes d'expressions facilite l'utilisation de PVS.<br /><br />Notre bibliothèque peut être utilisée pour construire des modèles de Taylor pour des expressions données, pour dériver des bornes plus ou moins précises pour des expressions arithmétiques et également pour certifier des inégalités ou bornes d'expressions. Disposer d'une méthode pour vérifier des expressions dans un assistant de preuves permet de vérifier certaines expressions qui apparaissent dans des logiciels de missions critiques.<br /><br />Pour résumer, nous avons développé une bibliothèque de modèles de Taylor en PVS qui comprend les opérations arithmétiques et certaines fonctions élémentaires. Nous avons démontré la propriété d'inclusion pour les opérations et fonctions développées. Nous avons développé une stratégie appelée containment pour démontrer la propriété d'inclusion des modèles de Taylor construits à partir des opérations et fonctions précédemment définies. Nous avons développé une stratégie appelée taylors pour prouver des inégalités en utilisant les modèles de Taylor. Nous avons illustré sur deux applications l'intérêt de ces développements.

Ce manuscrit présente une double contribution expérimentale et théorique à l'étude des matériaux de type phase de Haucke AB5 substituée. Ces composés peuvent absorber l'hydrogène de manière réversible dans des conditions de pression et de température satisfaisantes pour de nombreuses applications technologiques dont le stockage de l'hydrogène.<br /><br />La caractérisation thermodynamique de la réaction solide-gaz a été réalisée pour des composés mono et polysubstitués. Dans le respect de bonnes conditions de croissance (décomposition) de la phase hydrure, nous avons cherché à déterminer les trajectoires thermodynamiques permises au cours des différentes transformations. Nous avons démontré expérimentalement que l'état d'avancement et la hiérarchie des points mémoires sont les seuls paramètres permettant de décrire une loi de comportement liée au caractère irréversible de l'hystérésis. Ces systèmes évoluent en mode « statique », indépendant du temps et quelle que soit la nature du composé hôte.<br /><br />De plus, l'étude par méthode ab initio de la structure électronique a permis de mettre en évidence le rôle des éléments de substitution ANi5 (A=La, Y, Ca) et LaNi5-xMx, où M est un élément de type s-p (Al, Si, Ge, Sn), de type s (Cu), ou un élément de transition (Mn, Fe, Co). Tout en dissociant l'aspect géométrique, le rôle de l'interaction chimique avec l'hydrogène a été analysé. Ces résultats ont permis d'identifier les facteurs qui contrôlent la stabilité des hydrures et leur capacité maximum d'absorption. Les modules de rigidité de ces matériaux ont été calculés et leur variation a été discutée en relation avec les propriétés d'absorption d'hydrogène

La généralisation et les puissances aujourd'hui disponibles des ressources informatiques, ordinateurs, espaces de stockages, réseaux, permettent d'imaginer de nouvelles méthodes de travail ou de loisir, inconcevables, il y a encore peu. Les ordinateurs monolithiques centralisés, ont peu à peu laissé place à des architectures distribuées "client/serveur" qui se trouvent elles mêmes concurencées par de nouvelles organisations de systèmes distribués, les systèmes "pair à pair". Cette migration n'est pas le fait de spécialistes; les utilisateurs les moins avertis utilisent tous les jours ces nouvelles technologies, que ce soit pour échanger des courriers électroniques, à des fins commerciales à travers le "e-commerce" sur le Web, ou encore pour échanger des fichiers, hors de toute infrastructure, "d'égal à égal".<br />Les mondes du commerce, de l'industrie et de la recherche, ont bien compris les avantages et les enjeux de cette révolution et investissent massivement dans la recherche et le développement autour de ces nouvelles technologies, que l'on appelle les "grilles", qui désignent des ressources informatiques globales et qui ouvrent une nouvelle approche. Une des disciplines autour des grilles concerne le calcul. Elle est l'objet des travaux présentés ici.<br /><br />Sur le campus de l'Université Paris-Sud, à Orsay, une synergie est née entre le Laboratoire de Recherche en Informatique (LRI) d'une part, et le Laboratoire de l'Accélérateur Linéaire (LAL), d'autre part, afin de mener à bien, ensemble, des travaux sur les infrastructures de grille qui ouvrent de nouvelles voies d'investigation pour le premier et de nouvelles méthodes de travail pour le second.<br /><br />Les travaux présentés dans ce manuscrit sont le résultat de cette collaboration pluridisciplinaire. Ils se sont basés sur XtremWeb, la plate-forme de recherche et de production de calcul global développée au LRI. Nous commençons par présenter un état de l'art des systèmes distribués à grande Èchelle, ses principes fondamentaux, son architecture basée sur les services.<br />Puis nous introduisons XtremWeb et détaillons les modifications que nous avons dû apporter, tant au niveau de son architecture que de son implémentation, afin de mieux répondre aux exigences et aux besoins de ce type de plate-forme. Nous présentons ensuite deux études autour de cette plate-forme permettant de généraliser l'utilisation de ressources inter grilles, d'une part, et d'utiliser sur une grille des services qui n'ont pas été prévus à cette fin, d'autre part. Enfin, nous présentons l'utilisation, les problèmes à résoudre et les avantages à tirer de notre plate-forme par la communauté de recherche en physique des hautes énergies, grande consommatrice de ressources informatiques.

L'objectif de ce travail est le portage efficace, sur différents calculateurs parallèles, d'une formulation permettant la modélisation de phénomènes électromagnétiques hyperfréquences en régime harmonique et en espace libre. Cette démarche découle du besoin accru de modéliser des dispositifs toujours plus grands et plus complexes qui ne peuvent êtrerésolus sur des calculateurs scalaires classiques. Les équations de Maxwell en régime fréquentiel sont discrétisées en 3 dimensions par la méthode des éléments finis couplée à des conditions aux limites absorbantes. Les calculateurs parallèles qui servent de support à l'implantation de la formulation sont à mémoire partagée ou distribuée. Le portage sur un CRAY C98 (mémoire partagée) est faite à partir du code séquentiel. Le parallélisme est introduit par l'adjonction manuelle de directives interprétées à la compilation. Les résultats ainsi obtenus tendent à prouver que la parallélisation des algorithmes séquentiels ont une granulité adaptée à ce type d'architecture. Néanmoins, le type de stockage du système matriciel est modifié afin d'accroître les performances vectorielles. L'utilisation de calculateurs à mémoire distribuée (ferme de stations, CRAY T3E) demande un modification complète des algorithmes de sorte à exploiter au mieux les ressources de ces calculateurs en distribuant le stockage de la matrice éléments finis et en minimisant le nombre de passages de messages. L'expérience acquise montre que le calcul parallèle permet la modélisation de géométries réalistes en 3D mais que l'utilisation de tels supports informatiques requière une bonne adéquation algorithmes - architecture cible. Des exemples de problèmes de diffractions par des objets de grande taille sont exposés. Une application de cette méthode aux problèmes de guide d'ondes ouverts de forte puissance est également décrite. Le calcul du champ lointain calculé à partir du champ proche est en bon accord avec les résultats expérimentaux.

Cette thèse porte sur l'étude théorique et pratique d'un système de typage appliqué à la preuve de programmes de style fonctionnels. Le système de base est le système ST créé par C.Raffalli; il comporte, outre le polymorphisme, du sous-typage et de l'omission de contenu non-algorithmique. Nous étudions tout d'abord les modèles de la théorie définie par le système de types, en construisant une axiomatique basée sur les treillis permettant de modéliser le calcul et la logique. Nous étudions sur cette base le système de types, montrons la réduction du sujet, et la possibilité de définir en interne la normalisabilité et la réductibilité des programmes. Dans la suite de la thèse, plus appliquée, nous étudions des codages de types de données riches inspirés des langages fonctionnels - y incluant notamment un système de modules du premier ordre- dans le Lambda-Calcul, et montrons qu'ils s'intègrent harmonieusement dans le système; la méthodologie développée dans cette partie permet d'étendre le langage de types et le langage de programmation en conservant un critère de consistance assurant la sûreté du code typé.

Cette étude aborde différents schémas d'intégration temporelle en calcul dynamique, et leur capacité à dissiper les hautes fréquences numériques introduites par les discrétisation temporelle et spatiale. La discrétisation temporelle d'un problème de dynamique peut être réalisée par la Méthode des Différences Finies ou celle des Eléments Finis et plus particulièrement la méthode de Galerkin - discontinue. Les résultats sont alors perturbés par des oscillations parasites d'origine purement numérique et issues des discrétisations temporelle et spatiale. Des méthodes permettent de les amortir en dissipant de l'énergie. Les schémas explicites amortissants de Tchamwa - Wielgosz et de Bonelli sont tout d'abord comparés au traditionnel Bulk-viscosity sur des cas 1D et 3D axi-symétriques. Un algorithme de pilotage de l'amortissement pour le schéma de Tchamwa - Wielgosz est ensuite développé de manière à obtenir une efficacité amortissante optimale tout au long des calculs sans pour autant observer une baisse trop importante de l'énergie. L'utilisation des méthodes amortissantes sur des exemples numériques issus d'essais expérimentaux (essais aux Barres de Hopkinson, impact transversal d'une tôle) est enfin étudiée. Des conclusions de cette étude, citons tout d'abord que l'utilisation des méthodes amortissantes s'avère très efficace pour filtrer les oscillations parasites mais en dissipant généralement trop d'énergie, ce qui a motivé le développement d'un pilotage original de l'amortissement. Une seconde innovation réside dans l'étude d'un schéma temporel explicite de type éléments finis permettant d'aboutir à des résultats se rapprochant de la solution théorique discrétisée.

Au coeur des liens entre Théorie de la Démonstration et Théorie des Types, la correspondance de Curry-Howard fournit des termes de preuves aux aspects calculatoires et équipés de théories équationnelles, i.e. des notions de normalisation et d'équivalence. Cette thèse contribue à étendre son cadre à des formalismes (comme le calcul des séquents) appropriés à des considérations d'ordre logique comme la recherche de preuve, à des systèmes expressifs dépassant la logique propositionnelle comme des théories des types, et aux raisonnements classiques plutôt qu'intuitionistes.<br />La première partie est intitulée Termes de Preuve pour la Logique Intuitioniste Implicationnelle, avec des contributions en déduction naturelle et calcul des séquents, normalisation et élimination des coupures, sémantiques en appel par nom et par valeur. En particulier elle introduit des calculs de termes de preuve pour le calcul des séquents depth-bounded G4 et la déduction naturelle multiplicative. Cette dernière donne lieu à un calcul de substitutions explicites avec affaiblissements et contractions, qui raffine la beta-réduction.<br />La deuxième partie, intitulée Théorie des Types en Calcul des Séquents, développe une théorie des Pure Type Sequent Calculi, équivalents aux Systèmes de Types Purs mais mieux adaptés à la recherche de preuve.<br />La troisième partie, intitulée Vers la Logique Classique, étudie des approches à la Théorie des Types classique. Elle développe un calcul des séquents pour une version classique du Système Fomega. Une approche à la question de l'équivalence de preuves classiques consiste à calculer les représentants canoniques de preuves équivalentes dans le cadre du Calcul des Structures.