Le travail présenté dans ce document consiste en une approche de test fonctionnel, destinée à per- mettre la validation de systèmes hybrides pour lesquels on dispose d'une spécification composée de propriétés de sûreté. La validation consiste à vérifier que le système satisfait à sa spécification, et donc aux besoins qui motivent sa création (sous réserve que la spécification traduise correctement les besoins).

Cette thèse traite l'étude de la fiabilité et de la durabilité des systèmes photovoltaïques (PV). Face à l'absence de retour d'expériences, réaliser une telle étude sous-entend, à la fois, de proposer des procédures expérimentales de qualification basées sur des essais accélérés conduits sur les composants critiques des systèmes PV, et de développer des outils de simulation de la fiabilité de l'assemblage de ces composants constituant un système considéré complexe. Ainsi dans un premier temps, nous nous sommes consacrés à l'étude de la fiabilité des modules PV. Une méthodologie originale basée sur les essais de dégradation accélérée nous a permis d'estimer la fiabilité de ces composants sous leurs deux modes prédominants de défaillance que sont la corrosion et la décoloration de l'encapsulant. L'originalité réside dans la prise en compte des variabilités des conditions environnementales et sur le couplage des essais accélérés et de dégradation. Un outil a été développé à cet effet. Dans un second temps, nous nous sommes placés à l'échelle des systèmes PV. Nous avons proposé de simuler certains paramètres caractérisant leur sûreté de fonctionnement en s'appuyant sur une représentation du système avec ces différents modes de fonctionnement et de dysfonctionnement (défaillances et dégradation) à l'aide de plusieurs Réseaux de Petri Stochastiques imbriqués sur plusieurs niveaux afin de se situer, pour chaque composant, aux échelles pour lesquelles les modes de défaillance pouvaient être saisis et formulés. Notre travail de thèse permet finalement de donner les bases méthodologiques et les outils de simulations pour qualifier et garantir la durée de vie de systèmes PV.

Le processus de dimensionnement des structures et des systèmes mécaniques comportent plusieurs étapes, allant de la définition des conditions et des besoins tout au long du cycle de vie, en vue de la spécification de la capacité et de la résistance requises pour accomplir les missions escomptées. La fiabilité figure parmi les objectifs les plus importants pour les fabricants, en plus de l'aspect économique, facteur clé qui influence largement le processus de conception. Dans ce contexte, la conception doit être élaborée afin de définir le meilleur compromis entre la fiabilité et le coût. Ce qui implique une étude précise et détaillée de tout le cycle de vie du produit, de la naissance jusqu'à la mise au rebus. Cette étude couvre les différentes phases du cycle de vie du produit, en intégrant la nécessité de démontrer la fiabilité du produit avant de commencer la production en série sous des contraintes de coût et de délais. Ce travail vise à donner des éléments de réponse aux trois questions suivantes : Comment peut-on démontrer la fiabilité du produit à partir de quelques essais ? Quel est le critère permettant une conception robuste sous des charges répétitives pour un système non dégradable ? Quelle est l'approche générale permettant de traiter les mécanismes de dégradation ?

Cette thèse vise à la conception d'un environnement pour le calcul haute performance dans un cadre d'optimisation numérique. Les outils de conception et d'optimisation sont répartis dans plusieurs équipes distantes, académiques et industrielles, qui collaborent au sein des memes projets. Les outils doivent etre fédérésau sein d'un environnement commun afin d'en faciliter l'accès aux chercheurs et ingénieurs. L'environnement que nous proposons, pour répondre aux conditions précédentes, se compose d'un système de workflow et d'un système de calcul distribué. Le premier a pour objctif de faciliter la tache de conception tandis que le second se charge de l'exécution sur des ressources de calcul distribuées. Bien sur, des suystèmes de communication entre les deux systèmes doivent etre développés. Les calculs doivent etre réalisés de manière efficace, en prenant en compte le parallélisme interne de certains codes, l'exécution synchrone ou asynchrone des taches, le transfert des données et les ressources matérielles et logicielles disponibles. De plus, l'environnement doit assurer un bon niveau de tolérance aux pannes et aux défaillances logicielles, afin de minimiser leur influence sur le résultat final ou sur le temps de calcul. Une condition importante est de pouvoir implanter un dispositif de reprise sur erreur, de telle sorte que le temps supplémentaire de traitement des erreurs soit très inférieur au temps de ré-exécution total.Dans le cadre de ce travail, notyre choix s'est porté sur le moteur de workflow Yawl, qui présente de bonnes caractéristiques en termes i) d'indépendancze vis à vis du matériel et du logiciel et ii) de mécanisme de reprise sdur erreur. Pour la partie calcul distribué, nos expériences ont été réalisées sur la plateforme Grid5000, en utilisant 64 machines différentes réparties sur cinq sites géographiques. Ce document d&taille les choix de conception de cet environnement ainsi que les ajouts et modifications que nous avons apportées à Yawl pour lui permettre de fonctionner sur une plateforme distribuée.

Les réseaux de capteurs ont créé un domaine de recherche très intéressant avec un champs d'applications très large. L'assistance aux personnes est notamment une des nombreux champs potentiels. Les contraintes de ce type de réseaux sont nombreuses et nécessitent des mécanismes spécifiques. Les problématiques de consommation d'énergie et de sécurité sont particulièrement importantes et ont fait l'objet de travaux spécifiques. La thématique de l'assistance aux personnes impose notamment des contraintes de robustesse et de fiabilité des communications. Le but de ces travaux de recherche est de définir diverses solutions permettant de répondre à ces problématiques. Ces travaux se décomposent en trois parties. Dans un premier temps, une plate-forme de communications basée sur les réseaux personnels PAN a été définie. Cette plate-forme a été développée et intégrée dans une station de métro Parisienne. Une modélisation de cette plate-forme ainsi qu'une analyse des observations et des résultats issus de cette intégration nous ont permis d'identifier les faiblesses de l'architecture et des technologies mises en œuvre. Dans un deuxième temps, nous avons développé diverses solutions permettant de fiabiliser cette plate-forme. En particulier, nous avons conçu un algorithme d'ordonnancement permettant de réduire la consommation d'énergie dans les réseaux capteurs par l'utilisation d'une analyse sémantique des données. Nous avons ensuite proposé une architecture de sécurité, Tiny 3-TLS, qui permet de sécurisé les communications entre un capteur et une entité située sur un réseau disjoint. Enfin, nous nous sommes intéressés aux communications entre cette plate-forme et les terminaux mobiles. L'aspect fiabilité a en particulier fait l'objet de travaux spécifiques. C'est pourquoi dans un troisième temps, nous avons proposé une solution de routage définissant une nouvelle métrique. Nous avons ensuite proposé un protocole coopératif permettant un apport de fiabilité dans les communications

L'electromigration est identifiée comme la principale cause de dégradation des interconnexions en cuivre limitant ainsi la fiabilité des produits issus de la microélectronique. Dans ces travaux nous proposons d'approfondir notre connaissance de ce phénomène en étudiant le lien qu'il présente avec les paramètres morphologiques du cuivre. Dans ce but, la technique de diffraction des électrons rétrodiffusés est utilisée. Nous avons d'abord développé les méthodes de préparation et d'acquisition nécessaires afin de pouvoir caractériser les structures issues des technologies 45 nm et au-delà que nous avons choisies pour cette étude. Un lien entre les joints de grains de forte désorientation et la localisation des cavités a alors pu être mis en évidence. Nous avons ensuite tenté de modifier la microstructure du cuivre pour impacter la fiabilité sans succès. Finalement, c'est l'intégration de nouveaux matériaux (Al, Co) renforçant l'interface supérieure, chemin de diffusion du phénomène, qui semble être la voie à adopter pour améliorer la résistance des lignes à l'électromigration.

Le but de la thèse a été de montrer que les cellules mémoires MRAM présentent de nombreux avantages pour une utilisation en tant que mémoire de configuration pour les architectures reconfigurables et en particulier les FPGAs (Field Programmable Gate Arrays). Ce type de composant est programmable et permet de concevoir un circuit numérique simplement en programmant des cellules mémoires qui définissent sa fonctionnalité. Un FPGA est principalement constitué de cellules mémoires. C'est pourquoi elles déterminent en grande partie ses caractéristiques comme sa surface ou sa consommation et influencent ses performances comme sa rapidité. Les mémoires MRAM sont composées de Jonctions Tunnel Magnétiques (JTMs) qui stockent l'information sous la forme d'une aimantation. Une JTM est composée de trois couches : deux couches de matériaux ferromagnétiques séparées par une couche isolante. Une des deux couches ferromagnétiques a une aimantation fixée dans un certaine direction (couche de référence) tandis que l'autre peut voir son aimantation changer dans deux directions (couche de stockage). Ainsi, la propagation des électrons est changée suivant que les deux aimantations sont parallèles ou antiparallèles c'est-à-dire que la résistance électrique de la jonction change suivant l'orientation relative des aimantations. Elle est faible lorsque les aimantations sont parallèles et forte lorsqu'elles sont antiparallèles. L'écriture d'une JTM consiste donc à changer l'orientation de l'aimantation de la couche de stockage tandis que la lecture consiste à déterminer si l'on a une forte ou une faible résistance. Les atouts de la JTM font d'elle une bonne candidate pour être une mémoire dite universelle, bien que des efforts de recherche restent à accomplir. Cependant, elle a de nombreux avantages comme la non-volatilité, la rapidité et la faible consommation à l'écriture comparée à la mémoire Flash ainsi que la résistance aux radiations. Grâce à ces avantages, on peut déjà l'utiliser dans certaines applications et en particulier dans le domaine du spatial. En effet, l'utilisation dans ce domaine permet de tirer parti de tous les avantages de la JTM en raison du fait qu'elle est intrinsèquement immune aux radiations et non-volatile. Elle permet donc de réaliser un FPGA résistant aux radiations et avec une basse consommation et de nouvelles fonctionnalités. Le travail de la thèse s'est donc déroulé sur trois ans. La première année a d'abord été dédiée à l'état de l'art afin d'apprendre le fonctionnement des JTMs, l'architecture des FPGAs, les techniques de durcissement aux radiations et de basse consommation ainsi que le fonctionnement des outils utilisés en microélectronique. Au bout de la première année, un nouveau concept d'architecture de FPGA a été proposé. Les deuxième et troisième années ont été dédiées à la réalisation de cette innovation avec la recherche de la meilleure structure de circuit et la réalisation d'un circuit de base d'un FPGA ainsi que la conception puis la fabrication d'un démonstrateur. Le démonstrateur a été testé avec succès et a permis de prouver le concept. La nouvelle architecture de circuit de FPGA a permis de montrer que l'utilisation des mémoires MRAM comme mémoire de configuration de FPGA était avantageuse et en particulier pour les technologies futures.

Cette thèse résume les travaux concernant les essais de fiabilité des commutateurs RF MEMS capacitifs et ohmiques développé par le CEA-Leti.Dans le premier chapitre les mesures de raideur par la technique de nano-indentation sur des commutateurs MEMS réels sont complétées par des observations AFM, MEB et FIB pour expliquer le comportement électrique des différents lots de commutateurs de type ohmique.Le deuxième chapitre présente les résultats de la caractérisation des propriétés structurales et physiques des diélectriques, qui sont généralement utilisés dans nos commutateurs RF MEMS ohmiques et capacitifs. Les analyses élémentaires confirment que tous les nitrures SiNx et oxydes SiO2 fabriqués par la technique PECVD ont une qualité inférieure par rapport à leurs homologues synthétisés à haute température.Les mécanismes de conduction sont identifiés dans SiNx et SiO2 PECVD en mesurant des courbes I-V sur les condensateurs MIM. Pour les deux nitrures SiNx, qui sont déposés en haute (HF) et fréquence mixte (MF), le mécanisme de conduction de type Poole-Frenkel. Pour le SiO2 le mécanisme de conduction est plus susceptible d'être contrôlé par émission Schottky. Les mesures I-V révèlent que tous ces matériaux piègent des charges parasites, il y a en effet une forte hystérésis entre les parties aller et retour de la courbe I-V.Pour étudier la cinétique de piégeage de charge des condensateurs MIM sont utilisés. Pour identifier les propriétés des pièges la technique d'injection à courant constant est utilisée. Le diélectrique SiNx PECVD montre une dépendance logarithmique de la cinétique de piégeage, tandis que le SiO2 montre une dépendance exponentielle. La concentration totale de pièges ne montre aucune dépendance pour les SiNx HF et SiO2 MF, ou une dépendance faible en fonction du champ pour le SiNx MF. La section efficace de capture dépend du champ pour les deux types de nitrures, ce qui est cohérent avec le modèle de piégeage à effet répulsif. Pour le SiO2, où un modèle de piégeage du premier ordre a été utilisé, la section efficace de capture est indépendante du champ. Dans le chapitre 4, les dérives de tension expérimentales sont mesurées lors des tests de stress à tension constante, pour différents niveaux de contrainte de tension. Dans la partie suivante, nous proposons une approche originale de modélisation de la dérive de la tension de "pull-in" basée sur le mécanisme de conduction et les propriétés de piégeage des diélectriques. Nous démontrons que grâce a notre modèle, il est possible d'expliquer les dérives de tension mesurée en termes de propriétés diélectriques bien identifiées. Cette procédure donne des résultats simulés en bon accord avec les mesures pour tous les matériaux, et permet de prédire les résultats de n'importe quelle séquence de vieillissement électrique. Nous utilisons ensuite notre modèle pour étudier l'effet des propriétés diélectriques et de la conception du commutateur sur le comportement à long terme de nos commutateurs MEMS.

Les circuits électroniques embarqués dans les systèmes évoluant au niveau spatial ou dans l'atmosphère sont soumis à des particules naturellement présentes qui peuvent provoquer une perturbation de leur fonctionnement. Le type d'effet lié à ces particules le plus souvent rencontré dans les composants logiques est le SEU. Cet effet correspond à l'inversion de l'état logique d'un élément de mémorisation. De nombreuses études ont été menées pour mettre au point des outils et méthodologies permettant de caractériser la sensibilité des mémoires (SRAM principalement) vis-à-vis de ce type d'effets. Néanmoins, avec l'augmentation importante de l'électronique embarquée et plus particulièrement, l'utilisation de composants de plus en plus complexes comme les microprocesseurs multicoeurs, il est devenu difficile, à l'aide des outils jusque là disponibles, de déterminer l'impact réel d'une erreur déclenchée dans un élément de mémorisation sur une application exécutée par le système électronique. L'utilisation des outils et méthodologies actuellement disponibles ne constituent alors qu'une approche pire cas : tous les éléments de mémorisation non protégés du composant sont comptabilisés et considérés comme sensibles, ce qui amène à considérer des marges importantes lors de l'analyse de risque de l'équipement. Une réduction importante de ces marges est possible en analysant le comportement dynamique de l'application opérée par le composant complexe. En effet, tous les éléments de mémorisation ne sont pas sensibles 100% du temps et de nombreux mécanismes de masquage peuvent faire en sorte qu'une erreur au niveau composant n'ait pas d'incidence sur l'application. Ce sujet de thèse aboutira à la mise au point d'un outil permettant de connaitre avec plus de précisions la sensibilité réelle d'une application opérée sur un microprocesseur, en vue d'optimiser les protections nécessaires et plus particulièrement, de tirer profit de l'architecture spécifique des microprocesseurs multicoeurs. Pour réaliser cette étude, les axes suivants seront investigués : - Étude de l'architecture des microprocesseurs - Utilisation des modèles de performance de processeurs - Utilisation des techniques d'émulation par FPGA - Analyse logicielle du code de l'application Des validations expérimentales sous laser et faisceau de particules seront également réalisées.

In this thesis we address problems related to the verification of software-based systems. We aremostly interested in the (safe) design of decision procedures used in verification. In addition, we alsoconsider a modularity problem for a modeling language used in the Why verification platform.Many verification problems can be reduced to a satisfiability problem modulo theories (SMT). In orderto build satisfiability procedures Armando et al. have proposed in 2001 an approach based on rewriting.This approach uses a general calculus for equational reasoning named paramodulation. In general, afair and exhaustive application of the rules of paramodulation calculus (PC) leads to a semi-decisionprocedure that halts on unsatisfiable inputs (the empty clause is then generated) but may diverge onsatisfiable ones. Fortunately, it may also terminate for some theories of interest in verification, and thusit becomes a decision procedure. To reason on the paramodulation calculus, a schematic paramodulationcalculus (SPC) has been studied, notably to automatically prove decidability of single theories and oftheir combinations. The advantage of SPC is that if it halts for one given abstract input, then PC haltsfor all the corresponding concrete inputs. More generally, SPC is an automated tool to check propertiesof PC like termination, stable infiniteness and deduction completeness.A major contribution of this thesis is a prototyping environment for designing and verifying decisionprocedures. This environment, based on the theoretical studies, is the first implementation of theschematic paramodulation calculus. It has been implemented from scratch on the firm basis provided bythe Maude system based on rewriting logic. We show that this prototype is very useful to derive decidabilityand combinability of theories of practical interest in verification. It helps testing new saturationstrategies and experimenting new extensions of the original (schematic) paramodulation calculus.This environment has been applied for the design of a schematic paramodulation calculus dedicated tothe theory of Integer Offsets. This contribution is the first extension of the notion of schematic paramodulationto a built-in theory. This study has led to new automatic proof techniques that are different fromthose performed manually in the literature. The assumptions to apply our proof techniques are easyto satisfy for equational theories with counting operators. We illustrate our theoretical contribution ontheories representing extensions of classical data structures such as lists and records.We have also addressed the problem of modular specification of generic Java classes and methods.We propose extensions to the Krakatoa Modeling Language, a part of the Why platform for provingthat a Java or C program is a correct implementation of some specification. The key features arethe introduction of parametricity both for types and for theories and an instantiation relation betweentheories. The proposed extensions are illustrated on two significant examples: the specification of thegeneric method for sorting arrays and for generic hash map.Both problems considered in this thesis are related to SMT solvers. Firstly, decision procedures areat the core of SMT solvers. Secondly, the Why platform extracts verification conditions from a sourceprogram annotated by specifications, and then transmits them to SMT solvers or proof assistants to checkthe program correctness.