Cette thèse traite de systèmes embarqués contrôlés par un ensemble de processus périodiques non synchronisés. Chaque processus est activé quasi-périodiquement, c'est-à-dire périodiquement avec une gigue bornée. Les délais de communication sont également bornés. De tels systèmes réactifs, appelés 'quasi-périodiques', apparaissent dès que l'on branche ensemble deux processus périodiques. Dans la littérature, ils sont parfois qualifiés de systèmes distribués temps-réels synchrones. Nous nous intéressons aux techniques de conception et d'analyse de ces systèmes qui n'imposent pas de synchronisation globale. Les langages synchrones ont été introduits pour faciliter la conception des systèmes réactifs. Ils offrent un cadre privilégié pour programmer, analyser, et vérifier des systèmes quasi-périodiques. En s'appuyant sur une approche synchrone, les contributions de cette thèse s'organisent selon trois thématiques: vérification,implémentation, et simulation des systèmes quasi périodiques.Vérification: 'L'abstraction quasi-synchrone' est une abstraction discrète proposée par Paul Caspi pour vérifier des propriétés de sûreté des systèmes quasi-périodiques. Nous démontrons que cette abstraction est en général incorrecte et nous donnons des conditions nécessaires et suffisantes sur le graphe de communication et les caractéristiques temps-réel de l'architecture pour assurer sa correction. Ces résultats sont ensuite généralisés aux systèmes multi-périodiques.Implémentation: Les 'LTTAs' sont des protocoles conçus pour assurer l'exécution correcte d'une application sur un système quasi-périodique. Nous proposons d'étudier les LTTA dans un cadre synchrone unifié qui englobe l'application et les contrôleurs introduits par les protocoles. Cette approche nous permet de simplifier les protocoles existants, de proposer des versions optimisées, et de donner de nouvelles preuves de correction. Nous présentons également dans le même cadre un protocole fondé sur une synchronisation d'horloge pour comparer les performances des deux approches.Simulation: Un système quasi-périodique est un exemple de modèle faisant intervenir des caractéristiques temps-réels et des tolérances. Pour ce type de modèle non déterministe, nous proposons une 'simulation symbolique', inspirée des techniques de vérification des automates temporisés. Nous montrons comment compiler un modèle mêlant des composantes temps-réel non déterministes et des contrôleurs discrets en un programme discret qui manipule des ensembles de valeurs. Chaque trace du programme résultant capture un ensemble d'exécutions possibles du programme source. / In this thesis we study embedded controllers implemented as sets of unsynchronized periodic processes. Each process activates quasi-periodically, that is, periodically with bounded jitter, and communicates with bounded transmission delays. Such reactive systems,termed 'quasi-periodic', exist as soon as two periodic processes areconnected together. In the distributed systems literature they arealso known as synchronous real-time models. We focus on techniquesfor the design and analysis of such systems without imposing a globa lclock synchronization. Synchronous languages were introduced as domain specific languages for the design of reactive systems. They offer an ideal framework to program, analyze, and verify quasi-periodic systems. Based on a synchronous approach, this thesis makes contributions to the treatment of quasi-periodic systems along three themes: verification,implementation, and simulation.Verification: The 'quasi-synchronous abstraction' is a discrete abstraction proposed by Paul Caspi for model checking safety properties of quasi-periodic systems. We show that this abstractionis not sound in general and give necessary and sufficient conditionson both the static communication graph of the application and the real-time characteristics of the architecture to recover soundness. We then generalize these results to multirate systems.Implementation: 'Loosely time-triggered architectures' are protocols designed to ensure the correct execution of an application running on a quasi-periodic system. We propose a unified framework that encompasses both the application and the protocol controllers. This framework allows us to simplify existing protocols, propose optimized versions, and give new correctness proofs. We instantiate our framework with a protocol based on clock synchronization to compare the performance of the two approaches.Simulation: Quasi-periodic systems are but one example of timed systems involving real-time characteristics and tolerances. For such nondeterministic models, we propose a 'symbolic simulation' scheme inspired by model checking techniques for timed automata. We show how to compile a model mixing nondeterministic continuous-time and discrete-time dynamics into a discrete program manipulating sets of possible values. Each trace of the resulting program captures a set of possible executions of the source program.

Cette thèse traite des approches implicites et explicites, ainsi que de leur convergence, de l'exploration d'espace d'états atteignables de circuits logiques provenant de programmes réactifs synchrones écrits en Esterel, ECL ou SyncCharts. Nos travaux visent à réduire les coûts de ces explorations à l'aide de<br />techniques génériques ou spécifiques à notre cadre de travail. Nous utilisons les résultats de ces explorations à des fins de vérification formelle de propriétés de sûreté, de génération d'automates explicites ou de génération de séquences de tests exhaustives. Nous décrivons trois outils.<br />Le premier outil est un vérificateur formel implicite, à base de Diagrammes de Décisions Binaires (BDDs). Ce vérificateur présente plusieurs techniques permettant de réduire le nombre de variables impliquées dans les calculs d'espace d'états. Nous proposons notamment l'abstraction de variables à l'aide d'une logique trivaluée. Cette nouvelle méthode étend la technique usuelle de remplacement de variables d'états par des entrées libres. Ces deux méthodes calculant des sur-approximations de l'espace d'états atteignables, nous proposons différentes techniques utilisant des informations concernant la structure du modèle et permettant de réduire la sur-approximation.<br />Le deuxième outil est un moteur d'exploration explicite, basé sur l'énumération des états accessibles.<br />Ce moteur repose sur la simulation de la propagation du courant électrique dans les portes du circuit et supporte les circuits cycliques. Ce moteur comporte de nombreuses optimisations et fait appel à différentes heuristiques visant à éviter les explosions en temps ou en espace inhérentes à cette approche, ce qui lui<br />confère de très bonnes performances. Ce moteur a été appliqué à la génération d'automates explicites et à la vérification formelle.<br />Enfin, le troisième outil est une évolution hybride implicite/explicite du moteur purement explicite. Dans cette évolution, les états sont toujours analysés individuellement mais symboliquement à l'aide de BDDs. Ce moteur a également été appliqué à la génération d'automates explicites, mais il est plutôt destiné à la vérification formelle ou la génération de séequences de tests exhaustives.<br />Nous présentons des résultats d'expérimentations de ces différentes approches sur plusieurs exemples industriels.

Ce mémoire de thèse s'intéresse aux problèmes posés par l'intégration dans les technologies silicium des synthétiseurs de fréquence dans la gamme 1-5 GHz. Il est montré que l'intégration des architectures classiques n'est pas envisageable car la consommation excessive et le bruit de phase obtenus sont incompatibles avec les spécifications des applications radiofréquences modernes. Dans ce mémoire, un oscillateur original capable de se verrouiller sur l'harmonique d'un signal d'entrée basse fréquence appelé Oscillateur Synchrone (OS) est présenté. Une étude théorique permettant de prévoir la plage de synchronisation de l'OS est proposée rendant ainsi possible une conception optimisée. D'autre part elle confirme les propriétés attendues des OS, en particulier la recopie du bruit de phase du signal de synchronisation, au facteur de multiplication près. Deux prototypes d'OS, intégrés dans une technologie BiCMOS 0,8 μm, sont décrits. Le premier oscille aux alentours de 2,4 GHz et est synchronisé par un signal de fréquence voisine de 400 MHz.. Sa plage de synchronisation de 12 MHz . Le deuxième prototype est une version optimisée, à partir de la théorie développée, oscillant aux alentours de 2 GHz. Il est synchronisé par un signal de fréquence voisine de 330 MHz. Sa plage de synchronisation est de 112 MHz environ permettant de couvrir la plage de réception ou d'émission de l'application UMTS2000. Ces deux prototypes confirment les avantages de l'OS dans une architecture de synthétiseur à boucle double par le report des contraintes de bruit de phase sur la boucle basse fréquence et par sa consommation bien moins élevée qu'une boucle à verrouillage de phase fonctionnant à la même fréquence. Un dernier prototype implanté dans la technologie CMOS 0,25 μm de STMicroelectronics est ensuite décrit. Cet OS oscille à 5,2 GHz et présente une plage de synchronisation de 160 MHz lorsqu'un signal à 900 MHz est appliqué sur son entrée (6ème sous harmonique).

Dans un contexte ou la question de la préservation de l'environnement est devenue un sujet sociétal majeur, la recherche de nouvelles technologies pour remplacer la voiture à essence constitue un véritable enjeu industriel. Les véhicules hybrides et électriques sont une alternative prometteuse aux véhicules conventionnels. Ce travail de thèse porte sur la conception et l'optimisation des machines électriques pour la motorisation de ces voitures. Au cours de ces travaux, nous avons développé une nouvelle méthodologie de dimensionnement et d'optimisation des machines synchrones à double excitation. L'intérêt de cette méthode est son bon compromis entre la précision et le temps de calcul et sa capacité d'adaptation à plusieurs types de machines. Le second volet de la thèse est consacré à la proposition d'une nouvelle structure de machine synchrone à rotor bobiné. Une technique originale de compensation de la réaction magnétique d'induit est mise en place, elle consiste en l'insertion d'aimants secondaires permettant de créer un flux dans l'axe q de la machine. Ce dernier a pour rôle d'affaiblir le flux de la réaction magnétique d'induit.

Cette thèse est consacrée à l'étude expérimentale et théorique des propriétés quantiques d'un Oscillateur Paramétrique Optique pompé en mode synchrone (SPOPO) en dessous du seuil. Les relations d'entrée-sortie du champ quantique sont établies pour un tel dispositif en utilisant un formalisme symplectique à la fois en temps et en fréquence. On prédit que le champ produit est dans un état fortement multimode où les modes comprimés sont des peignes de fréquences de différents profils spectraux/temporels. On le démontre expérimentalement à l'aide d'un SPOPO composé d'une cavité en anneau et un cristal non-linéaire pompé par un train d'impulsions femtoscondes à 400 nm. Les états générés sont mesurés par une détection homodyne avec mise en forme de l'oscillateur local. Cela permet la construction d'une matrice de covariance dans une base de pixels de fréquences et la mise en évidence des corrélations quantiques entre les différentes régions du spectre optique. La diagonalisation de cette matrice donne les modes décorrélés en bruit et les niveaux de compression de bruit respectifs. La génération d'états décrits par au moins 4 modes décorrélés dans des états comprimés se propageant dans le même faisceau a été démontrée. Les résultats plus récents montrent des états à 8 modes, ouvrant la voie à la génération extensible d'états fortement multimodes de la lumière.

Suite aux directives européennes incitant les constructeurs de moteurs électriques à supprimer<br />de leur offre, les moteurs à faible rendement, une politique de conception de moteurs à haut<br />rendement est engagée. Toutefois, l'évaluation préalable, en simulation, de ce paramètre, et<br />notamment des pertes fer de la machine reste aujourd'hui un problème difficile. Dans cette<br />optique, depuis quelques années, un modèle, nommé « Loss Surface », de calcul a posteriori<br />des pertes fer sous le logiciel éléments finis Flux2D™ a été développé. Au cours de ce travail,<br />plusieurs améliorations sont apportées à ce modèle LS. Un nouveau banc de caractérisation à<br />partir d'un onduleur de tension performant a permis de prolonger en fréquence la surface<br />dynamique LS. Une nouvelle formulation de l'identification de la contribution dynamique, plus<br />simple, a également été réalisée. Au final, les gains apportés sont conséquents. Deux machines<br />synchrones à aimants aux caractéristiques très différentes ont ensuite été utilisées pour évaluer<br />les améliorations sur des structures complexes. La première machine, nous a permis de tester<br />l'impact du niveau d'induction sur l'évolution des pertes fer, et la seconde machine, l'influence<br />de la fréquence. Deux phénomènes physiques importants ont également été étudiés afin de<br />connaître leurs contributions aux pertes d'origine magnétique : les pertes par courants induits<br />dans un matériau massif tel qu'un aimant, et l'effet sur les propriétés magnétiques des contraintes<br /> mécaniques induites par le poinçonnage du circuit magnétique.

Thèse de doctorat : Génie électrique : INPL : 2007. / Titre provenant de l'écran-titre. Bibliogr.

Cette thèse étudie la vérification automatique de propriétés de sûreté de systèmes logico-numériques discrets ou hybrides. Ce sont des systèmes ayant des variables booléennes et numériques et des comportements discrets et continus. Notre approche est fondée sur l'analyse statique par interprétation abstraite. Nous adressons les problèmes suivants : les méthodes d'interprétation abstraite numériques exigent l'énumération des états booléens, et par conséquent, ils souffrent du probléme d'explosion d'espace d'états. En outre, il y a une perte de précision due à l'utilisation d'un opérateur d'élargissement afin de garantir la terminaison de l'analyse. Par ailleurs, nous voulons rendre les méthodes d'interprétation abstraite accessibles à des langages de simulation hybrides. Dans cette thèse, nous généralisons d'abord l'accélération abstraite, une méthode qui améliore la précision des invariants numériques inférés. Ensuite, nous montrons comment étendre l'accélération abstraite et l'itération de max-stratégies à des programmes logico-numériques, ce qui aide à améliorer le compromis entre l'efficacité et la précision. En ce qui concerne les systèmes hybrides, nous traduisons le langage de programmation synchrone et hybride Zelus vers les automates hybrides logico-numériques, et nous étendons les méthodes d'analyse logico-numérique aux systèmes hybrides. Enfin, nous avons mis en oeuvre les méthodes proposées dans un outil nommé ReaVer et nous fournissons des résultats expérimentaux. En conclusion, cette thèse propose une approche unifiée à la vérification de systèmes logico-numériques discrets et hybrides fondée sur l'interprétation abstraite qui est capable d'intégrer des méthodes d'interprétation abstraite numériques sophistiquées tout en améliorant le compromis entre l'efficacité et la précision.

L’importance des systèmes temps-réels embarqués dans les sociétés industrialisées modernes en font un terrain d’application privilégié pour les méthodes formelles. La prépondérance des contraintes temporelles dans les spécifications de ces systèmes motive la mise au point de solutions spécifiques. Cette thèse s’intéresse à une classe de systèmes temps-réels incluant ceux développés avec la chaîne d’outils OASIS, développée au CEA LIST. Nos travaux portent sur la notion de délai de bout-en-bout, que nous proposons de modéliser comme une contrainte temporelle concernant l’influence du flot d’informations des entrées sur celui des sorties. Afin de répondre à la complexité croissante des systèmes temps-réels, nous étudions l’applicabilité de cette notion nouvelle au développement incrémental par raffinement et par composition. Le raffinement est abordé sous l’angle de la conservation de propriétés garantes de la correction du système au cours du processus de développement. Nous délimitons les conditions nécessaires et suffisantes à la conservation du délai de bout-en-bout lors d’un tel processus. De même, nous donnons des conditions suffisantes pour permettre le calcul du délai de bout-en-bout de manière compositionnelle. Combinés, ces résultats permettent d’établir un formalisme permettant la preuve du délai de bout-en-bout lors d’une démarche de développement incrémentale. / Real-time embedded systems are at the core of modern industrialized societies. They are a privileged target for the application of formal methods. The importance of real-time constraints in the specification of these systems requires the design of ad-hoc solutions. This work considers a class of real-time systems including those developed using OASIS, a tool-chain targeting hard real-time embedded systems developed at CEA LIST. We study the notion of end-to-end delay, which we propose to model as a constraint bearing directly on the influence of the input information flow over the output information flow . In order to cope with the growing complexity of real-time embedded systems, we study the possibility to apply this new notion of delay to the incremental development of such systems, by using both stepwise refinement and composition operators. We define the necessary and sufficient conditions to the preservation of the end-to-end delay by stepwise refinement. Similarly, we give sufficient conditions to compute the end-to-end delay in a compositional fashion. Together, these results permit to establish a formalism allowing to prove end-to-end delay properties in stepwise development methodologies.

Nowadays, new approaches to fabricate high-performance electrode materials are of vital importance in the renewable energy field. Here, we present a facile synthesis procedure of 3D Ni(OH)2/graphene hybrids for supercapacitors via synchronous electrochemical-assisted exfoliation and assembly of graphene on 3D Ni(OH)2 networks. With the assistance of an electric field, the electrochemically exfoliated high-quality graphene can be readily, uniformly assembled on the surfaces of 3D Ni(OH)2. When serving as electrode materials for supercapacitors, the resulting 3D Ni(OH)2/graphene composites exhibited excellent specific capacitance (263 mF cm−2 at 2 mA cm−2), remarkable rate capability and super-long cycle life (retention of 94.1% even after 10 000 continuous charge–discharge cycles), which may be attributed to their highly porous, stable 3D architecture as well as uniform, firm anchoring of ultrathin graphene on their surfaces. Therefore, our approach provides a facile strategy for the large-scale synthesis of high-quality graphene based composites towards various applications.