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 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.

Les travaux présentés dans ce mémoire proposent une méthodologie d'étude des interférences électromagnétiques dans les systèmes intégrés RF. Cette thèse se focalise sur les problèmes de couplage rayonné en champ proche entre différentes parties d'une puce électronique ou entre circuits intégrés d'une carte.Ensuite cette méthodologie est appliquée sur deux cas d'études à différentes échelles, dans le premier cas l'étude du couplage entre un amplificateur de puissance 3G et un transceiver est présentée puis un modèle de couplage est réalisé reproduisant les effets parasites observés lors des mesures. Puis une étude pour extraire et évaluer les couplages entre blocs, ici inductance d'un VCO et structures proches, d'une puce électronique. Ensuite un modèle d'émission champ proche de ce circuit est proposé.Ces travaux mettent en évidence l'intérêt de réaliser des études CEM à chaque phase de conception d'un circuit ou d'un système ainsi que l'intérêt des mesures champ proche qui permettent de réaliser de l'investigation et du diagnostic CEM / The work presented in this PhD suggest a methodology for the study of electromagnetic interference in RF integrated systems. This thesis focuses on the problems of near-field radiated coupling between different parts of a chip or between ICs.Then this methodology is applied to two case studies on different scales, in the first case study the coupling between a 3G power amplifier and a transceiver is presented then a model of the coupling is made reproducing parasitic effects observed in measurements. Then a study to extract and evaluate the coupling between blocks, between a VCO inductor and nearby structures of a microchip. Then a near-field emission model of this circuit is proposed.These works demonstrate the interest of EMC studies in all phases of designing a circuit or system and the interest of near-field measurements that allow the realization of the investigation and diagnosis of EMC

Nous nous intéressons à l'analyse des exigences de performabilité des systèmes communicants mobiles par model checking. Nous modélisons ces systèmes à l'aide d'un formalisme de haut niveau issu du π-calcul, permettant de considérer des comportements stochastiques, temporels, déterministes, ou indéterministes. Cependant, dans le π-calcul, la primitive de communication de base des systèmes est la communication en point-à-point synchrone. Or, les systèmes mobiles, qui utilisent des réseaux sans fil, communiquent essentiellement par diffusion locale. C'est pourquoi, dans un premier temps, nous définissons la communication par diffusion dans le π-calcul, afin de mieux modéliser les systèmes que nous étudions. Nous proposons d'utiliser des versions probabilistes et stochastiques de l'algèbre que nous avons défini, pour permettre des études de performance. Nous en définissons une version temporelle permettant de considérer le temps dans les modèles. Mais l'absence d'outils d'analyse des propriétés sur des modèles spécifiés en une algèbre issue du π-calcul est un obstacle majeur à notre travail. La définition de règles de traduction en langage PRISM, nous permet de traduire nos modèles, en modèles de bas niveau supports du model checking, à savoir des chaînes de Markov à temps discret, à temps continu, des automates temporisés, ou des automates temporisés probabilistes. Nous avons choisi l'outil PRISM car, à notre connaissance, dans sa dernière version, il est le seul outil à supporter les formalismes de bas niveau que nous venons de citer, et ainsi il permet de réaliser des études de performabilité complètes. Cette façon de procéder nous permet de pallier à l'absence d'outils d'analyse pour nos modèles. Par la suite, nous appliquons ces concepts théoriques aux réseaux de capteurs sans fil mobiles.

Nous proposons de concevoir et de mettre en oeuvre un environnement logiciel pour une "gestion guidée par les modèles" des changements dans les architectures des applications distribuées coopératives. Les aspects adaptabilité des applications, les aspects transformations de graphe et les aspects particuliers des applications distribuées coopératives sont étudiés. Une approche d'adaptation s'appuyant sur une modélisation par les graphes et un style architectural de type Poducteur/Consommateur est présentée pour des applications communicantes collaboratives sensibles au contexte. Une démarche de raffinement est proposée permettant de garantir un certain degré d'adaptabilité en faisant un compromis entre les différents paramètres du contexte. Ces travaux de recherche ont aussi permis de définir un cadre algorithmique générique de reconfiguration architecturale multi-niveaux pour la sélection des architectures de déploiement les plus adaptées à un contexte et aux situations associées. Ce cadre a été appliqué au cas de la communication et de la coopération de groupe. Elle a aussi permis de modéliser le style architectural Producteur/Consommateur pour une communication orientée événement. Des règles d'adaptation ont été définies. Elles comportent une partie basée sur SWRL pour la description du contexte et des règles d'adaptation, et une partie basée sur les grammaires de graphes pour la transformation des configurations de déploiement / In this work, we study dynamic reconfiguration of collaborative communicating applications. Providing generic and scalable solutions for automated self-reconfiguration in group collaboration support systems can be driven by rule-based reconfiguration policies. To achieve this goal, we elaborate a dynamic graph-based modeling approach and we develop structural models that can represent the different interaction dependencies from different configuration-related point of views: communication flows between the distributed machines, the networked deployment nodes, and the service composition. Our solution is based on graph grammars rewriting. We provide graph transformation to specify rules for changing deployment architecture while being in conformance to an architectural style. In order to handle the complex design of communicating collaborative system architectures and the related adaptation issues, we propose a multi-layer modelling approach. This approach assures generic solutions for automatic context aware adaptation. Our approach is based on the observation that semantic data analysis that can be exploited to manage priorities and more generally to manage communications. This allows us to represent, in a richer way, the semantics of the managed systems

Nous nous intéressons à l'analyse des exigences de performabilité des systèmes communicants mobiles par model checking. Nous modélisons ces systèmes à l'aide d'un formalisme de haut niveau issu du π-calcul, permettant de considérer des comportements stochastiques, temporels, déterministes, ou indéterministes. Cependant, dans le π-calcul, la primitive de communication de base des systèmes est la communication en point-à-point synchrone. Or, les systèmes mobiles, qui utilisent des réseaux sans fil, communiquent essentiellement par diffusion locale. C'est pourquoi, dans un premier temps, nous définissons la communication par diffusion dans le π-calcul, afin de mieux modéliser les systèmes que nous étudions. Nous proposons d'utiliser des versions probabilistes et stochastiques de l'algèbre que nous avons défini, pour permettre des études de performance. Nous en définissons une version temporelle permettant de considérer le temps dans les modèles. Mais l'absence d'outils d'analyse des propriétés sur des modèles spécifiés en une algèbre issue du π-calcul est un obstacle majeur à notre travail. La définition de règles de traduction en langage PRISM, nous permet de traduire nos modèles, en modèles de bas niveau supports du model checking, à savoir des chaînes de Markov à temps discret, à temps continu, des automates temporisés, ou des automates temporisés probabilistes. Nous avons choisi l'outil PRISM car, à notre connaissance, dans sa dernière version, il est le seul outil à supporter les formalismes de bas niveau que nous venons de citer, et ainsi il permet de réaliser des études de performabilité complètes. Cette façon de procéder nous permet de pallier à l'absence d'outils d'analyse pour nos modèles. Par la suite, nous appliquons ces concepts théoriques aux réseaux de capteurs sans fil mobiles. / We are interested in analyzing the performability requirements of mobile communication systems by using model checking techniques. We model these systems using a high-level formalism derived from the π-calculus, for considering stochastic, timed, deterministic or indeterministic behaviors. However, in the π-calculus, the basic communication primitive of systems is the synchronous point-to-point communication. However, mobile systems that use wireless networks, mostly communicate by local broadcast. Therefore, we first define the broadcast communication into the π-calculus, to better model the systems we study. We propose to use probabilistic and stochastic versions of the algebra we have defined to allow performance studies. We define a temporal version to consider time in the models. But the lack of tools for analyzing properties of models specified with π-calculus is a major obstacle to our work and its objectives. The definition of translation rules into the PRISM language allows us to translate our models in low-level models which can support model checking, namely discrete time, or continuous time Markov chains, timed automata, or probabilistic timed automata. We chose the PRISM model checker because, in our best knowledge, in its latest version, it is the only tool that supports the low-level formalisms that we have previously cited, and thus, makes it possible to realize complete performability studies. This approach allows us to overcome the lack of model checkers for our models. Subsequently, we apply these theoretical concepts to analyse performability of mobile wireless sensor networks.