Cette thèse porte sur la vérification des automates temporisés, un modèle bien établi pour les systèmes temps-réels. La thèse est constituée de trois parties. La première est dédiée à la déterminisation des automates temporisés, problème qui n'a pas de solution en général. Nous proposons une méthode approchée (sur-approximation, sous-approximation, mélange des deux) fondée sur la construction d'un jeu de sûreté. Cette méthode améliore les approches existantes en combinant leurs avantages respectifs. Nous appliquons ensuite cette méthode de déterminisation à la génération automatique de tests de conformité. Dans la seconde partie, nous prenons en compte des aspects quantitatifs des systèmes temps-réel grâce à une notion de fréquence des états acceptants dans une exécution d'un automate temporisé. Plus précisément, la fréquence d'une exécution est la proportion de temps passée dans les états acceptants. Nous intéressons alors à l'ensemble des fréquences des exécutions d'un automate temporisé pour étudier, par exemple, le vide de langages seuils. Nous montrons ainsi que les bornes de l'ensemble des fréquences sont calculables pour deux classes d'automates temporisés. D'une part, les bornes peuvent être calculées en espace logarithmique par une procédure non-déterministe dans les automates temporisés à une horloge. D'autre part, elles peuvent être calculées en espace polynomial dans les automates temporisés à plusieurs horloges ne contenant pas de cycles forçant la convergence d'horloges. Finalement, nous étudions le problème de l'accessibilité des états acceptants dans des réseaux d'automates temporisés qui communiquent via des files FIFO. Nous considérons tout d'abord des automates temporisés à temps discret, et caractérisons les topologies de réseaux pour lesquelles l'accessibilité est décidable. Cette caractérisation est ensuite étendue aux automates temporisés à temps continu. / This thesis is about verification of timed automata, a well-established model for real time systems. The document is structured in three parts. The first part is dedicated to the determinization of timed automata, a problem which has no solution in general. We propose an approximate (over-approximation/under-approximation/mix) method based on the construction of a safety game. This method improves both existing approaches by combining their respective advantages. Then, we apply this determinization approach to the generation of conformance tests. In the second part, we take into account quantitative aspects of real time systems thanks to a notion of frequency of accepting states along executions of timed automata. More precisely, the frequency of a run is the proportion of time elapsed in accepting states. Then, we study the set of frequencies of runs of a timed automaton in order to decide, for example, the emptiness of threshold languages. We thus prove that the bounds of the set of frequencies are computable for two classes of timed automata. On the one hand, we prove that bounds are computable in logarithmic space by a non-deterministic procedure in one-clock timed automata. On the other hand, they can be computed in polynomial space in timed automata with several clocks, but having no cycle that forces the convergence between clocks. Finally, we study the reachability problem in networks of timed automata communicating through FIFO channels. We first consider dicrete timed automata, and characterize topologies of networks for which reachability is decidable. Then, this characterization is extended to dense-time automata.

L’Onera développe des capteurs inertiels MEMS vibrants avec des performances qui peuvent intéresser des applications spatiales. Les électroniques analogiques traditionnellement associées ne sont à priori pas limitantes par rapport aux performances physiques des capteurs. En revanche, elles se montrent encombrantes, non reconfigurables, et ne délivrent pas les grandeurs mesurées sous forme numérique à l’ordinateur de bord. En outre,dans le cadre d’une utilisation spatiale, elles sont sujettes à dépendance et à obsolescence :le remplacement d’un composant implique une nouvelle qualification.Cette thèse propose une nouvelle architecture numérique générique, limitant au maximum les composants analogiques nécessaires. Les travaux portent principalement sur deux capteurs développés par l’Onera : l’accéléromètre à lame vibrante VIA et le gyromètre vibrant à effet Coriolis VIG, mais sont justement transposables à d’autres familles. Une première fonction clé identifiée est la datation d’évènements pour la mesure de fréquence et de phase, une seconde concerne la synthèse numérique directe de fréquence pour le pilotage de résonateurs, et une troisième traite la génération de signaux sinusoïdaux purs à partir des trains binaires délivrés par le système numérique. Ces fonctions sont réalisées sous forme de périphériques numériques autour d’un processeur embarqué, le tout synthétisé sur composant programmable FPGA. Le manuscrit débute par un rappel des lois physiques et des technologies de mesure inertielle, suivi d’une revue des oscillateurs, analogiques et numériques, afin de déterminer l’architecture numérique souhaitée. Le chapitre suivant aborde de façon théorique les fonctions numériques envisagées, et en détermine les éléments de performance. La mise en oeuvre de ces fonctions et les premiers résultats expérimentaux sont ensuite présentés d’abord au niveau de la fonction seule, et enfin dans une architecture complète incluant le capteur et le logiciel embarqué, pour fournir de vraies mesures inertielles. Ces résultats encouragent le déploiement d’électronique numérique dans les prochaines générations de capteurs. / Onera has been developing vibrating inertial MEMS sensors with performances good enough for space uses. Associated conventional analog electronics are not limiting the physical performances of the sensors. They are, however, bulky, not reconfigurable, and do not deliver digital measurements to the on-board computer. Furthermore, when used for space applications, they have to cope with dependency and obsolescence requiring a new qualification when any part is changed.This thesis offers a new digital generic architecture with as few analog parts as possible. Work has been focused on two sensors developed by Onera: the VIA, a vibrating beam accelerometer, and the VIG, a Coriolis vibrating gyro, but can address other sensors. A first digital function identified is event timestamping for frequency and phase measurements; a second key function is the direct digital synthesis of the oscillating sensors driving signal; the third one generates pure sine signals from binary sequences output from the digital platform. These function are implemented as peripherals of an embedded processor on a FPGA.This dissertation firstly reminds physical laws and technologies of inertial measurements, followed by a quick review of oscillators, analog and digital, in order to introduce the chosen digital architecture. A following chapter studies the theory of the digital functions considered and identifies their performances. Afterwards, realisations and first experimental results are exposed, at a function level first, at a global level then, with the sensor and the embedded software to provide real inertial readings. The results gathered boost the idea of deploying digital electronics in future sensor releases.

Les capteurs sans fil ont un avenir prometteur c’est pourquoi leur développement est àl’origine de nombreuses recherches. Leur autonomie reste cependant un problème à résoudre.Les travaux de cette thèse se concentrent précisément sur cette problématique : trouverune stratégie permettant aux capteurs d’être autonomes en énergie.L’énergie nécessaire à l’alimentation du capteur, quel que soit son mode de fonctionnement,doit en effet être récupérée de l’environnement dans lequel le capteur se trouve. Deplus, en cas d’absence ou d’insuffisance d’énergie environnante, le fonctionnement du capteurdoit pouvoir perdurer. À cela s’ajoute la nécessité de connaitre à tout instant la quantitéd’énergie disponible afin de pouvoir maintenir un niveau de charge constant et ainsi prolongerla vie du capteur. Enfin, toute cette gestion de l’énergie doit pouvoir garantir le meilleurrendement possible.Cette étude a conduit à la conception et au test d’un circuit en technologie CMOS 90nm.Ce même circuit a été intégré dans les capteurs sans fil d’un réseau en cours de développement.Et enfin, une méthode permettant de connaitre le niveau d’énergie embarquée a étémise au point et pourra permettre à l’avenir la conception d’un nouveau circuit de power managementpour capteurs autonomes en énergie. / Wireless sensors have a bright future so their development is causing a lot of research.However, their autonomy is still an issue.This work focuses on this problem : find a strategy for the sensors to be autonomous.The energy required to power the sensor, whatever its working mode, must indeed be harvestedfrom the environment wherein the sensor is located. Moreover, in case of absence ora lack of available energy, the sensor has to keep working. Additionnaly the state-of-chargehas to be known in real time in order to extend the sensor lifetime. Finally, the energy managementhas to give the highest efficiency.This study led to the design and the test of a circuit in CMOS 90nm technology. Thiscircuit was integrated in wireless sensors for networks under development. Finally, a methodto estimate the level of energy in the sensor has been developed and will allow to design anew circuit of power management for wireless sensor network.

L'objectif de cette thèse est d'améliorer la compréhension des phénomènes jouant un rôle dans la mesure effectuée dans un analyseur sanguin, en particulier le comptage et la mesure de volumétrie d'une population de globules rouges reposant sur l'effet Coulter. Des simulations numériques sont effectuées dans le but de prédire la dynamique des globules rouges dans les zones de mesure et pour reproduire la mesure électrique associée, servant au comptage et à la volumétrie des cellules. Ces simulations sont effectuées à l'intérieur de configurations industrielles d'analyseur sanguin, en utilisant un outil numérique développé à l'IMAG, le solveur YALES2BIO. En utilisant la méthode des frontières immergées avec suivi de front, un modèle de particule déformable est introduit, celui-ci prend en compte le contraste de viscosité ainsi que les effets mécaniques de la courbure et de l'élasticité sur la membrane. Le solveur est validé grâce à de nombreux cas tests parcourant différents régimes et effets physiques. L'écoulement fluide dans cette géométrie d'analyseur sanguin est caractérisée par un fort gradient de vitesse axial dans la direction de l'écoulement, impliquant la présence d'un écoulement extensionnel au niveau du micro-orifice, là où a lieu la mesure. La dynamique des globules rouges est étudiée par des simulations numériques pour différentes conditions initiales, telles que sa position ou son orientation. Il est observé que les globules rouges vont se réorienter selon l'axe principal de l'analyseur sanguin dans tous les cas. Pour comprendre le phénomène, des modèles analytiques sont adaptés au cas des écoulements extensionnels et reproduisent correctement les tendances de réorientation.Cette thèse présente également la reproduction de la mesure électrique utilisée pour le comptage et la mesure de la distribution des volumes de globules rouges. De nombreuses simulations de la dynamique des globules rouges sont effectuées et utilisées pour générer l'impulsion électrique correspondant au passage du globule rouge dans le micro-orifice. Les amplitudes d'impulsions électriques résultantes permettent la caractérisation de la réponse électrique en fonction des paramètres initiaux de la simulation par une approche statistique. Un algorithme de Monte-Carlo est utilisé pour la quantification des erreurs de mesure liées à l'orientation et la position des globules rouges dans le micro-orifice. Ceci permet la génération d'une distribution de volume mesurée pour une population de globules rouges bien définie et la caractérisation des erreurs de mesure associées. / The aim of this thesis is to improve the understanding of the phenomena involved in the measurement performed in a blood analyzer, namely the counting and sizing of red blood cells based on the Coulter effect. Numerical simulations are performed to predict the dynamics of red blood cells in the measurement regions, and to reproduce the associated electrical measurement used to count and size the cells. These numerical simulations are performed in industrial configurations using a numerical tool developed at IMAG, the YALES2BIO solver. Using the Front-Tracking Immersed Boundary Method, a deformable particle model for the red blood cell is introduced which takes the viscosity contrast as well as the mechanical effects of the curvature and elasticity on the membrane into account. The solver is validated against several test cases spreading over a large range of regimes and physical effects.The velocity field in the blood analyzer geometry is found to consist of an intense axial velocity gradient in the direction of the flow, resulting in a extensional flow at the micro-orifice, where the measurement is performed. The dynamics of the red blood cells is studied with numerical simulations with different initial conditions, such as its position or orientation. They are found to reorient along the main axis of the blood analyzer in all cases. In order to understand the phenomenon, analytical models are adapted to the case of extensional flows and are found to reproduce the observed trends.This thesis also presents the reproduction of the electrical measurement used to count red blood cells and measure their volume distribution. Numerous dynamics simulations are performed and used to generate the electrical pulse corresponding to the passage of a red blood cell inside the micro-orifice. The resulting electrical pulse amplitudes are used to characterize the electrical response depending on the initial parameters of the simulation by means of a statistical approach. A Monte-Carlo algorithm helps quantifying the errors on the measurement of cell depending on its orientation and position inside the micro-orifice. This allows the generation of a measured volume distribution of a well defined red blood cell population and the characterization of the associated measurement errors.

En 2010, ERDF (Electricité Réseau Distribution France) a entamé la mise en place du projet « Linky » dont l'objectif est d'installer 35 millions de compteurs intelligents en France. Ces compteurs permettront de collecter les données de consommation en « temps réel », avec lesquelles des modèles de charge plus précis pourront être envisagés. Dans ce contexte, cette thèse définit deux objectifs: la définition de modèles prédictifs de charge pour la conduite et la conception de modèles d'estimation de charge pour la planification. En ce qui concerne la conduite, nous avons développés deux modèles. Le premier exploite le formalisme mathématique des séries chronologiques ; le second est basé sur un réseau de neurones. Les deux modèles cherchent à prévoir la charge des jours « J+1 » et « J+2 » à partir des informations collectées jusqu'au jour « J ». Le modèle « série chronologique » repose sur les propriétés temporelles des courbes de charge. Ainsi on découpe la courbe de charge en trois parties : la tendance, la périodicité et le résidu. Les premiers deux sont déterministes et indépendamment développés en deux modèles : le modèle de tendance et le modèle de cyclicité. La somme de la prévision de ces deux modèles est la prévision finale. Le résidu quant à lui capture les phénomènes aléatoires que présente la courbe de charge. Le modèle de prédiction ainsi développé s'aide de nombreux outils statistiques (e.g., test de stationnarité, test ANOVA, analyse spectrale, entres autres) pour garantir son bon fonctionnement. Enfin, modèle « série chronologique » prend en compte plusieurs facteurs qui expliquent la variation dans la courbe de consommation tels que la température, les cyclicités, le temps, et le type du jour, etc. En ce qui concerne le modèle à base de réseaux de neurones, nous nous focalisons sur les stratégies de sélection de la structure pour un modèle optimal. Les choix des entrées et du nombre de neurones cachés sont effectués à travers les méthodes dites de «régression orthogonale » et de « leave-one-out-virtuel ». Les résultats montrent que la procédure proposée permet de choisir une structure de réseau de neurones qui garantisse une bonne précision de prédiction. En ce qui concerne la planification, un modèle non paramétrique est proposé et comparé avec le modèle actuel « BAGHEERA » d'EDF. Avec l'ouverture du marché d'électricité, la relation entre les fournisseurs, les clients et les distributeurs devient flexible. Les informations qualitatives d'un client particulier telles que sa puissance souscrite, son code d'activité, ses tarifs etc. sont de moins en moins disponibles. L'évolution du modèle BAGHEERA qui dépend ces informations pour classer les clients dans différentes catégories est devenue indispensable. Le modèle non paramétrique est un modèle individuel centré sur le relevé des compteurs. Trois variables de régression non paramétriques : Nadaraya Watson, Local Linear et Local Linear adapted ont été analysées et comparées. Les scénarios de validation montrent que le modèle non paramétrique est plus précis que le modèle « BAGHEERA ». Ces nouveaux modèles ont été conçus et validés sur de vraies données collectées sur le territoire français. / From 2010, ERDF (French DSO) started the “Linky” project. The project aims at installing 35 millions smart meters in France. These smart meters will collect individual client's consumption data in real time and transfer these data to the data center automatically in a certain frequency. These detailed consumption information provided by the smart metering system enables the designs of more accurate load models. On this purpose, two distinctive objectives are defined in this dissertation: the forecasting load models for the operation need and the estimation load models for the planning need. For the operation need, two models are developed, respectively relying on the “time series” and the “neural network” principals. They are both for the objective of predicting the loads in “D+1” and “D+2” days based on the historical information till “D” day. The “time series” model divides the load curve into three components: the trend, the cyclic, and the residual. The first two parts are deterministic, from which two models named the trend model and the cyclic model are made. The sum of the prevision of these two models is the final prediction result. For a better precision, numerous statistical tools are also integrated such that the stationary test, the smoothed periodogram, the ANOVA test and the gliding window estimation, etc. The time series model can extract information from the influence factors such as the time, the temperature, the periodicities and the day type, etc. Being the most popular non linear model and the universal approximator, the neural network load forecasting model is also studied in this dissertation. We focus on the strategy of the structure selection. The work is in collaboration with Prof. Dreyfus (SIGMA lab), a well known expert in the machine learning field. Input selection and model selection are performed by the “orthogonal forward regression” and the “virtual-leave-one-out” algorithms. Results show that the proposed procedure is efficient and guarantees the chosen model a good accuracy on the load forecasting. For the planning, a nonparametric model is designed and compared with the actual model “BAGHEERA” of the French electricity company EDF. With the opening of the electricity market, the relationship among the regulators, suppliers and clients is changing. The qualitative information about a particular client such as his subscribed power, his activity code and his electricity tariffs becomes less and less available. The evolution from the BAGHEERA model to a data-driven model is unavoidable, since the BAGHEERA model depends on these information to attribute every client in the French territory into a pre-defined category. The proposed nonparametric model is individualized and can deal with both temperature sensitive (possessing an electrical heater) and temperature insensitive clients. Three nonparametric regressors are proposed: the Nadaraya Watson, the local linear, and the local linear adapted. The validation studies show that the nonparametric model has a better estimation precision than the BAGHEERA model. These novel models are designed and validated by the real measurements collected in the French distribution network.

Le détecteur proportionnel sphérique gazeux, SPC (Spherical Proportional Counter), est un nouveau concept de détecteur de particules. Ses principales caractéristiques sont : un seuil très bas en énergie indépendant du volume (faible capacité électronique), une bonne résolution en énergie, une grande robustesse et une seule voie de lecture. SEDINE, un détecteur bas bruit de fond, destiné à la recherche de matière noire légère, a été fabriqué et installé au Laboratoire Souterrain de Modane. Il est actuellement opérationnel et vise à mesurer les évènements rares à bas seuil en énergie. La sensibilité dans la détection d’événements rares étant à basse énergie directement corrélée au niveau du bruit de fond du détecteur, la diminution du seuil en énergie ainsi que celle du bruit de fond ont été la problématique principale de cette thèse. Un effort important a été consacré à la mise en opération du dispositif expérimental. Plusieurs paramètres de détection ont été optimisés : homogénéité du champ électrique dans le volume de l’enceinte, tenue aux étincelles, niveau du bruit de fond électronique et l’étanchéité du détecteur. Le détecteur a été optimisé pour assurer un fonctionnement avec un gain stable à haute pression. La modification du blindage, les nettoyages de l’enceinte du détecteur et l’ajout d’une tente anti-Radon ont permis de réduire significativement le bruit de fond de SEDINE. Les progrès accomplis ont permis d’augmenter la sensibilité du détecteur à basse énergie à une valeur comparable, pour des WIMPs à basse masse, aux autres expériences de recherche souterraines. Nous présentons donc des résultats avec un bruit de fond mesuré, dans la région du keV, qui nous permet de donner une figure d’exclusion compétitive pour la production de la matière noire légère. / The Spherical gaseous detector (or Spherical Proportional Counter, SPC) is a novel type of a particle detector, with a broad range of applications. Its main features in- clude a very low energy threshold which is independent of the volume (due to its very low capacitance), a good energy resolution, robustness and a single detection readout channel. SEDINE, a low background detector installed at the underground site of Laboratoire Souterrain de Modane is currently being operated and aims at measuring events at a very low energy threshold, around 40 eV. The sensitivity for the rare events detection at low energy is correlated to the detector background and to the decreasing the level of energy threshold, which was the main point of this thesis. A major effort has been devoted to the operating of the experimental detector. Several detection parameters were optimized: the electric field homogeneity in the sphere, keeping clear of sparks, the electronic noise level and the leak rate of the detector. The detector is optimized for operation with a high pressure stable gain. The modification of the shield, cleanings of the detector and the addition of an anti-Radon tent have significantly reduced the background of SEDINE. Progress has increased the sensitivity of the detector at low energy up to a value comparable to the results other underground research experiences for the low mass WIMPs. We will present the results with a measured background in the region of keV, which has allowed us to show a competitive figure of exclusion for the production of light dark matter.

Ce travail porte sur la réalisation d'un microspectromètre SWIFTS (Stationary Wave Integrated Fourier Transform Spectrometer) incluant des compteurs de photons SNSPD (Superconducting Nanowire Single Photon Detector). Il met en œuvre un interféromètre intégré à guide d'onde en arête bouclé, en SiN, sous lequel sont disposés 24 nanofils supraconducteurs SNSPD en NbN échantillonnant les interférences au pas de 160nm, à une longueur d'onde centrée sur 1.55µm. La conception, l'étude des composantes optique et électronique, la fabrication et la caractérisation à 4.2K sont décrites, jusqu'à la mise en évidence d'une modulation de puissance lumineuse dans le guide conformément à la formation attendue d'interférences. Le SWIFTS-SNSPD constitue le premier dispositif optoélectronique supraconducteur à part entière, doublement intégré. Sa capacité unique d'échantillonnage direct de franges d'interférences ouvre de nombreuses perspectives, pour des applications allant de l'astrophysique aux télécoms. / This work presents the realization of a SWIFTS (Stationary Wave Integrated Fourier Transform Spectrometer) micro-spectrometer with SNSPD (Superconducting Nanowire Single Photon Detector) photon counters. The device features an integrated interferometer made of a SiN loop ridge-waveguide, with an array of 24 NbN-nanowire SNSPD underneath that samples at a 160nm period the interferogram of a laser light, at a wavelength centred on 1.55µm. The conception, preliminary studies of integrated optics and electronics, fabrication and characterization at 4.2K of the final device are described, in particular the observation of the detected signal modulation in the waveguide in agreement with the expected interference formation. The SWIFTS-SNSPD constitutes the first stand-alone, fully integrated superconducting optoelectronic device. Its unique capability of direct sampling of light interferogram opens numerous perspectives, with possible applications ranging from astrophysics to telecommunications.

.