L’électrochromisme est la capacité de certains matériaux à changer de couleur en réponse à un stimulus électrique. Jusqu’ici réservés à des structures rigides, comme les fenêtres à opacité adaptative, les matériaux électrochromes possèdent de nombreux avantages qui rendent particulièrement intéressante leur utilisation au sein de structures souples, notamment textiles, afin de former des textiles « intelligents ». On peut citer leur large palette de couleurs, une consommation électrique faible et un changement de couleur visible selon tout angle de vue. Durant cette thèse, plusieurs structures électrochromes à base textile ont été réalisées. Une première étape a été la diminution du nombre de couches requises pour la réalisation d’un afficheur électrochrome, passant de 7 à 5, ainsi que l’ajout d’une épaisseur textile en tant que couche de stockage. Une deuxième étape a été le remplacement de tous les composants non textiles par des composants textiles, améliorant ainsi significativement la flexibilité et le toucher de la structure. Une dernière étape, enfin, a permis la conception d’une structure électrochrome flexible 100 % textile et monocouche. Des écrans textiles composés de plusieurs pixels électrochromes ont été réalisés et commandés automatiquement.Une méthode a été mise au point pour quantifier le vieillissement de ces afficheurs. Leur courte durée de vie est en effet un frein majeur à toute utilisation commerciale. Cette méthode a été appliquée à tous les types de structures développées. L’influence de plusieurs facteurs sur le processus de vieillissement a été étudiée, ce qui a permis d’identifier les conditions permettant l’optimisation de leur durée de vie. / Electrochromism is the ability of a material to change its color according to an electrical stimulus. Electrochromic materials have been so far only been used into rigid structures, such as smart windows. However, they have multiple advantages making their use for the development of flexible, textile-based structures particularly suitable. These are for example a large color palette, a low electrical consumption and a color change that is visible at every point of view. In this PhD project, different textile-based electrochromic structures have been realized. The first step was the decrease of the number of layers required for the realization of an electrochromic device, going from 7 to 5, and the addition of a textile layer used as a storage layer. Then, all the non-textile components were replaced by textile materials, which improved significantly the flexibility and the textile touch of the device. The final step was the conception of a single-layer electrochromic all-textile flexible device. Textile displays, composed of many electrochromic pixels, were realized and automatically commanded. An innovative method was developed in order to quantify the ageing of these devices. Indeed, their short lifetime is a major limitation to any commercial use. This method was applied to all the electrochromic textile-based developed devices. The influence of different parameters on their ageing process was studied, which allowed the identification of the optimal condition to apply in order to maximize their lifetime.

La nécessité de diminuer la consommation à la fois des systèmes autonomes communicants à haute fréquence et des circuits CMOS implique l’utilisation de transistors fonctionnant sous faible tension d’alimentation. Les performances des composants à base de silicium se dégradant rapidement dans ce régime de fonctionnement, les semiconducteurs III-V à faible bande interdite sont aujourd’hui envisagés comme une alternative. Parmi ceux-ci, l’InAs paraît le plus prometteur. Dans ce contexte, ce travail a pour but d’ouvrir la voie à l'utilisation d’un canal à base d'InAs pour les systèmes analogiques et numériques. Plus précisément, nous étudions la croissance par épitaxie par jets moléculaires des hétérostructures InAs/AlSb sur des substrats (001) GaAs et GaP par l’intermédiaire d'une couche tampon Ga(Al)Sb. La microscopie à force atomique, la microscopie électronique en transmission et la diffraction d’électrons de haute énergie sont utilisées afin de mettre en évidence l’influence critique des conditions de croissance sur la nucléation des antimoniures. Cette étude sert de base à l’optimisation de canaux InAs à haute mobilité sur ces deux substrats fortement désadaptés en maille. Les résultats obtenus dans le cas de GaP sont ensuite étendus au cas de pseudo-substrats commerciaux GaP/Si de haute qualité cristalline pour l’intégration de matériaux à base d’InAs sur des substrats Si (001) exactement orientés. Des mobilités électroniques atteignant 28 000 cm-2.V-1.s-1 à 300K et supérieures à 100 000 cm-2.V-1.s-1 à 77K sont démontrées. / Low power consumption transistors operating at low supply voltage are highly required for both high frequency autonomous communicating systems and CMOS technology. Since the performances of silicon-based devices are strongly degraded upon low voltage operation, low bandgap III-V semiconductors are now considered as alternative active materials. Among them, one of the best candidates is InAs. Therefore, the present work aims on paving the way to the use of InAs in transistor channels for both high-speed analog and digital applications. We particularly investigate the molecular beam epitaxy growth of InAs/AlSb heterostructures on both (001) GaAs and GaP via an antimonide metamorphic buffer layer. Using atomic force microscopy, transmission electron microscopy and reflection high energy electron diffraction, we first show the critical influence of the growth conditions on the III-Sb nucleation. From this study, we then achieve optimized high mobility InAs layers on these two highly mismatched substrates. The results obtained in the GaP case are extended to commercially available high quality GaP/Si platforms for the integration of InAs-based materials on an exactly oriented (001) Si substrate. State of the art mobility of 28 000 cm-2.V-1.s-1 at 300K and higher than 100 000 cm-2.V-1.s-1 at 77K are demonstrated.

Garantir le fonctionnement correct des systèmes informatisés est un enjeu chaque jour plus important. La vérification formelle est un ensemble de techniquespermettant d’établir la correction d’un modèle mathématique du système par rapport à des propriétés exprimées dans un langage formel.Le "Regular model checking" est une technique bien connuede vérification de systèmes infinis. Elle manipule des ensembles infinis de configurations représentés de façon symbolique. Le "Regular model checking" de systèmes à canaux non fiables (LCS) soulève des questions fondamentales de décision et de complexité concernant l’ordre sous-mot qui modélise la perte de messages. Nous abordons ces questions et résolvons un problème ouvert sur l’index de la congruence de Simon pour les langages testables par morceaux.L’accessibilité pour les LCS est décidable mais de complexité F_{omega^omega} très élevée, bien au delà des complexités primitives récursives. Plusieurs problèmes de complexité équivalente ont été découverts récemment, par exemple dans la vérification de mémoire faibles ou de logique temporelle métrique. Le problème de plongement de Post (PEP) est une abstraction de l’accessibilité des LCS, lui aussi de complexité F_{omega^omega}, et qui nous sert de base dans la définition d’une classe de complexité correspondante. Nous proposons une généralisation commune aux deux variantes existantes de PEP et donnons une preuve de décidabilité simplifiée. Ceci permet d’étendre le modèle des systèmes à canaux unidirectionnels (UCS) par des tests simples tout en préservant la décidabilité de l’accessibilité. / The increasing use of software and automated systems has made it important to ensure their correct behaviour. Formal verification is the technique that establishes correctness of a system or a mathematical model of the system with respect to properties expressed in a formal language.Regular model checking is a common technique for verification of infinite-state systems - it represents infinite sets of configurations symbolically in a finite manner and manipulates them using these representations. Regular model checking for lossy channel systems brings up basic automata-theoretic questions concerning the subword relation on words which models the lossiness of the channels. We address these state complexity and decision problems, and also solve a long-standing problem involving the index of the Simon's piecewise-testability congruence.The reachability problem for lossy channel systems (LCS), though decidable, has very high F_{omega^omega} complexity, well beyond primitive-recursive. In recent times several problems with this complexity have been discovered, for example in the fields of verification of weak memory models and metric temporal logic. The Post Embedding Problem (PEP) is an algebraic abstraction of the reachability problem on LCS, with the same complexity, and is our champion for a "master" problem for the class F_{omega^omega}. We provide a common generalization of two known variants of PEP and give a simpler proof of decidability. This allows us to extend the unidirectional channel system (UCS) model with simple channel tests while having decidable reachability.

Étude de méthodes de spécification et vérification des protocoles de communication. La méthode de vérification mise en œuvre consiste a évaluer les spécifications du protocole sur un modèle fini qui le représente. Le langage de spécification est basé sur un mu calcul permettant l'expression aussi bien de comportements que de propriétés

Le système de vérification propose permet de réduire et de comparer des systèmes de transitions étiquetées en tenant compte d'une relation d'équivalence. Les relations d'équivalence considérées sont la congruence forte, l'équivalence et la congruence observationnelles et la congruence par modèle d'acceptation. Les bases théoriques d'Aldebaran sont présentées ainsi que des algorithmes efficaces pour la comparaison et les réductions de systèmes de transition étiquetées et une réalisation en langage C

Description d'un outil d'aide à la conception et à la vérification de systèmes communicants qui est basé sur le calcul CCS de Milner.

Cette thèse porte sur la réalisation d'une maquette du système CESAR, système d'aide à l'analyse d'applications réparties. L'outil réalisé permet de comparer une application décrite par un programme parallèle avec ses spécifications données par un ensemble de formules d'une logique temporelle.

Le système CESAR proposé dans cette thèse est un système d'aide à la conception des applications reparties. Il permet de décrire l'application étudiée dans un langage algorithmique en termes de processus communiquant par rendez-vous; de spécifier les propriétés de comportement souhaitées au moyen d'une logique temporelle. Le modèle sur lequel ces formules sont analysées est un réseau de Petri interprété généré automatiquement à partir de la description fournie. L'analyse repose sur une évaluation des opérateurs temporels comme points fixes de transformateurs de prédicats sur l'espace d'états du modèle.

Cette thèse a fait partie du projet MIMOC (Méthodes d'Intégration et de Miniaturisation d'Objets Communicants) qui a été mené à terme en partenariat avec le laboratoire IM2NP de Marseille, la société InsightSiP à Sophia Antipolis et Orange Labs La Turbie. Le projet cible les systèmes de transmission par impulsions occupant une très large bande de fréquences (signaux Ultra Large Bande : ULB). Au sein de ce projet, les travaux de cette thèse ont été concentrés sur le développement, la miniaturisation et l'intégration des antennes dans des systèmes de communications ULB conformes aux normes Américaines (FCC :3.1-10.6 GHz) et Européennes (ECC : 6-8.5 GHz). Le développement d'une antenne consiste à en maîtriser les différents paramètres en analysant leurs influences sur l'adaptation et le rayonnement de celle-ci. Une étude préliminaire a permis de créer une base de données qui a été utilisée par la suite dans les différentes phases du projet afin de réadapter l'élément en fonction de l'évolution de son environnement. Un élément rayonnant imprimé constitué de plusieurs étages rectangulaires, alimenté par la ligne ground coplanaire (GCPW), adapté dans la bande de fréquence FCC, a servi de base d'étude. Cette antenne a été étudiée dans deux configurations correspondant à deux types d'applications : un format carte de crédit et un format clé USB, principalement distinguées par leur encombrement lié à la largeur des plans de masse. L'étude a débuté avec une structure à plan de masse large et a été suivie, dans une deuxième phase, par des travaux de miniaturisation. La miniaturisation consiste à réduire la largeur des plans de masse en modifiant la géométrie de la structure afin de conserver ses performances radioélectriques. Plusieurs techniques ont été étudiées, notamment la réduction de l'encombrement par repliements 2D et 3D. La technique la plus efficace fut celle basée sur l'insertion de découpes au niveau des plans de masse latéraux ainsi qu'au niveau des plans de masse inférieurs. Une bonne maîtrise des dimensions de ces encoches a permis d'obtenir une structure réduite d'un facteur 5 avec une bonne adaptation sur toute la bande de fréquences. Ces structures ont ensuite été réalisées et les prototypes ont été caractérisés. La caractérisation s'est déroulée lors de plusieurs campagnes de mesures au LEAT et à Orange Labs à La Turbie. Un banc de test a été entièrement développé et des mesures dans les domaines temporel et fréquentiel ont permis d'extraire les performances des antennes : gain, diagramme de rayonnement, réponse impulsionnelle, facteur de fidélité, etc. La capacité d'une transmission à travers ces prototypes a été vérifiée en environnement réel. Des débits allant jusqu'à 500Mbits/s ont été atteint. La troisième phase des travaux a consisté à modéliser une puce génératrice d'impulsions ULB et l'intégrer en l'assemblant avec l'antenne dans un système. Cette étude a été réalisée dans la bande ULB européenne ECC. Un nouvel élément imprimé et miniaturisé adapté dans cette bande de fréquences a du être conçu. La puce a totalement été modélisé et paramétrée de façon à ce qu'elle soit prise en compte lors de la conception du système. Le projet MIMOC a été achevé avec succès. Le bon partenariat avec tous les membres s'est avéré très constructif et a permis de réaliser le codesign de la partie "antenne" et de la partie "microélectronique". Suite à ces travaux, un autre projet qui consiste à développer des systèmes communicants en contact avec le corps humain (RUBY) vient de démarrer.

L'approche objet permet des applications plus évoluées et plus fiables et des développements spécifiques moins coûteux et évolutifs. Les objectifs de ce travail sont, d'une part, de contribuer à la conceptualisation complète de modèles de simulation à objet et d'autre part, de les implémenter en utilisant des techniques de programmation concurrente. Après une présentation, au chapitre I, des concepts des systèmes de production et de leur gestion, nous avons évalué, au chapitre II, les différents modèles de structure et de simulation pour les systèmes de production. Le chapitre ID propose une démarche d'analyse pour identifier des classes d'objets en cinq types du domaine: physiques, rôles, incidents, interactions et spécifications. Chacune de ces classes est spécifiée par quatre modèles: communication, information, transition d'état et processus. Dans le chapitre IV, nous avons conceptualisé une architecture générale des objets actifs, une plateforme de simulation à objets concurrents et des classes d'objets sémantiques tels que les transactions, les moyens de production et les décisions pour l'établissement des modèles de simulation de production. Nous avons illustré, au chapitre V, l'implémentation des coopérations spatiales et temporelles entre objets concurrents dans la simulation avec des concepts processus "légers" basés sur l'outil Meijin++.