Cette thèse porte sur les techniques d'analyse formelle de systèmes hybrides à dynamiques continues non linéaire. Ses contributions portent sur les algorithmes d'atteignabilité et sur les problèmatiques liées à la representation des ensembles atteignables. This thesis deals with formal analysis of hybrid system with non linear continous dynamic. It contributes to the fields of reachability analysis algorithm and the set representation.

Ce manuscrit présente des résultats de recherche concernant une certaine classe de systèmes hybrides. Les systèmes hybrides peuvent être utilisés pour la modélisation de systèmes physiques complexes et hétérogènes dont l'évolution dans le temps présente des phénomènes discrets, tels que les commutations des convertisseurs ou les impacts des systèmes mécaniques. De la même manière, la théorie hybride peut être utilisée pour concevoir des contrôleurs hybrides, en général plus performants par rapport aux contrôleurs à temps continu. Dans ce cadre, les résultats de ce manuscrit peuvent être divisés en trois parties. D'abord des résultats de stabilité par rapport à un indice de performance de type Hinfini sont présentés pour une classe plutôt large de systèmes hybrides. Ensuite, nous introduisons de nouvelles architectures de contrôleurs hybrides pour les systèmes à temps continu, caractérisées par le fait que leur état peut être réinitialisé en fonction de la trajectoire. Enfin, nous présentons une technique de synthèse convexe pour la conception d'un contrôleur hybride multi-objectif. La comparaison avec les résultats classique met en évidence les avantages en termes de performance par rapport aux contrôleurs à temps continu classiques, tout en préservant la propriété de robustesse et la simplicité de conception. Bien que la théorie hybride soit en plein développement, ces travaux généralisent certains résultats existants, en améliorant la simplicité d'implémentation des solutions grâce à l'utilisation de la programmation semi-définie. En plus les architectures de contrôleurs hybrides présentées ont l'avantage de simplifier la généralisation de quelques résultats classiques concernant la synthèse optimale par rapport à des indices de performance communs.

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.

Le graphène épitaxié sur des substrats métalliques est un modèle prometteur pour le développement de nouveaux systèmes hybrides, dans lesquelles les effets d'interface peuvent être exploités pour concevoir de nouvelles propriétés. L'insertion d'espèces entre le graphène et son substrat, une opération connues sous le nom d'-"intercalation", est une approche très puissante à cet égard. Avec l'aide des outils de la physique des surfaces, nous avons étudié trois systèmes graphène/métal, dont deux sont des systèmes hybrides intercalés, et l'autre est un candidat pour un tel système : (i) le graphène/Ir(111) intercalé avec un oxyde ultra-mince, (ii) graphène/Ir(111) intercalé avec des couches sub-atomiques du cobalt et (iii) de graphène sur Re(0001). Nous avons montré que certains défauts, en particulier les ridules (délamination du graphène de son substrat) et d'autres régions courbées du graphène, jouent un rôle crucial, non anticipé, dans le processus d'intercalation. Nous avons également observé que l'intercalation se déroule d'une manière nettement différente sous ultravide et à pression atmosphérique. Dans le premier système, des espèces contenant de l'oxygène entrent à l'extrémité ouverte des ridules et diffusent au long de ces ridules pour former des nano-rubans d'oxyde. Ces rubans modifient le dopage électronique du graphène, ce qui se traduit également par des changements substantiels dans la réponse optique inélastique (Raman) du graphène. Dans le second système, l'efficacité de l'intercalation est apparue dépendante de l'interaction graphène-métal, laquelle varie entre les domaines de graphène orientés différemment sur_(111). Dans ce système, les sites d'entrée pour les espèces intercalées, des régions courbées dans le graphène, ont pu être identifiés grâce à l'observation in_operando (en cours de croissance) du processus. Enfin, la croissance de graphène dans un troisième système (graphène/Re(0001)), a été étudiée afin de permettre le développement de futurs systèmes graphène/Re hybrides supraconducteurs. Dans ce système, nous avons proposé deux voies de croissance, l'une étant basé sur un processus de croissance en surface d'un monocristal massif de Re(0001), l'autre reposant sur la ségrégation en surface, activée thermiquement, du carbone dissout à haute température dans des films minces de Re sur saphir.

Cette thèse a pour sujet la stabilisation de systèmes non-linéaires avec des mesures partielles et des entrées contraintes. Les deux premiers chapitres traitent du problème des entrées saturées dans le contexte des systèmes de dimension infinie pour des équations nonlinéaires abstraites et une équation aux dérivées partielles nonlinéaire particulière, l'équation de Korteweg-de Vries. Les outils mathématiques utilisés pour obtenir des résultats Le troisième chapitre propose une méthode de synthèse de retour de sortie pour deux équations de Korteweg-de Vries. Le quatrième chapitre concerne la synthèse d'un retour de sortie pour des systèmes non-linéaires de dimension finie pour lequel il existe un contrôle hybride. Une stratégie basée sur des observateurs grand gain est utilisée. / This thesis is about the stabilization of nonlinear systems with partial measurements and constrained input. The two first chapters deals with saturated inputs in the contex of infinite-dimensional systems for nonlinear abstract equations and for a particular partial differential equation, the Korteweg-de Vries equation. The third chapter provides an output feedback design for two Korteweg-de Vries equations using the backstepping method. The fourth chapter is about the output feedback design of nonlinear finite-dimensional systems for which there exists a hybrid controller. A high-gain observer strategy is used.

On nomme systèmes hybrides les systèmes qui intègrent des comportements continus et discrets. Leur comportement est en partie déterminé par des contraintes temporelles et/ou leur interaction avec un environnement physique via l'utilisation de capteurs et d'actionneurs. Il peut s'agir par exemple d'équipements de contrôle de procédés industriels ou de services domotiques. La validation de ces systèmes est un problème crucial, car ils sont parfois utilisés au sein d'applications où la sûreté de fonctionnement est critique (un système critique est un système dont la défaillance peut entraîner des blessures ou la mort d'êtres humains). Cette validation soulève plusieurs problèmes ; en particulier, une description détaillée du système à valider n'est pas toujours disponible, ou celle-ci est trop complexe pour qu'il soit possible en pratique d'établir avec certitude sa correction (par exemple parce que cette vérification exhaustive nécéssite des ressources en temps ou en matériel trop importantes). Dans ces conditions, nous nous intéressons à la validation de systèmes hybrides spécifiés par un ensemble de propriétés de sûreté. Une propriété de sûreté est une exigence portant sur le comportement du système qui ne contraint pas entièrement ce comportement, mais en spécifie des aspects particuliers. Elle peut ainsi porter sur la réaction attendue du système en réponse à une suite d'événements donnée, ou imposer des limites à l'évolution des grandeurs environnementales qu'il contrôle. Le travail présenté dans ce document consiste en une approche de test fonctionnel, destinée à permettre 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). / Hybrid systems posess a continuous and discrete behavior. This behavior is partially determined by temporal constraints, and/or interactions of the system with a physical environment by means of sensors and actuators. Hybrid systems include some industrial plant control software and home automation systems. The validation of hybrid systems is a crucial problem since they may be used in safety critical applications (a safety critical system is a system whose failure may lead to unacceptable financial or human costs). This validation raises several problems; in particular a complete description of the system to be validated is not always available. Its complexity may also prevent establishing the correction of the system with certainty (if for exampl a full proof computation requires too much time or equipment). Therefore we are interested in validating hybrid systems specified by a set of safety properties. A safety property is a requirement that constrains only some aspect of the system behavior and can be fullfilled by several implementations. It may for example specify the expected reaction of the system under specific circumstances or constrain the set of values that a variable is allowed to take. The work presented in this document is a functional testing approach aimed at allowing the validation of hybrid systems for which a specification composed of hybrid safety properties is available. Validation consists in verifying that the system satisfies its specification and therefore the needs that motivated its design (assuming the specification actually matches these needs).

Ces travaux de thèse portent sur l'étude de matériaux d'électrodes de supercondensateurs. Ce sont des dispositifs de stockage qui possèdent une densité de puissance importante de l'ordre de plusieurs kW/kg. Des systèmes asymétriques ont été développés dans le but d'augmenter la densité d'énergie de ces dispositifs, tout en essayant de maintenir une densité de puissance élevée. Ils font intervenir une électrode capacitive classique de carbone activé et une électrode faradique. Concernant cette électrode non-bloquante, deux orientations ont été abordées : • Principalement, l'utilisation de titanate de lithium Li4Ti5O12 qui est un matériau d'insertion du lithium habituellement utilisé dans les électrodes de batteries Li-ion. Il est apparu que pour les systèmes hybrides comportant une électrode négative composée uniquement de Li4Ti5O12, la densité d'énergie chute fortement au-delà de 1 kW/kg. L'utilisation d'électrodes négatives composites carbone activé + Li4Ti5O12 est donc préconisée pour maintenir de bonnes performances à la fois en énergie et en puissance. Ainsi, pour une densité de puissance de 2 kW/kg, la densité d'énergie du système hybride développé est encore 1,5 fois supérieure à celle d'un système symétrique carbone activé / carbone activé testé dans les mêmes conditions. • En second plan, l'utilisation du dioxyde de manganèse MnO2, matériau pseudo-capacitif qui fait intervenir des réactions redox. L'étude a porté sur la synthèse de l'oxyde métallique puis sur celle d'un matériau composite réalisé par auto-assemblage. Le but est d'agréger de fines particules de dioxyde de manganèse autour d'un squelette carboné. Une telle microstructure présente l'avantage d'offrir une grande surface spécifique de matière active directement en contact avec un réseau possédant une bonne conductivité électronique. Le matériau composite MnO2 + VGCF obtenu a été testé en électrode positive dans un système asymétrique face à une électrode négative de carbone activé. Cela a permis de multiplier par 1,5 l'étendue de la fenêtre de stabilité de l'électrolyte aqueux par rapport à un système carbone activé / carbone activé. Enfin, dans une optique exploratoire, l'utilisation du diamant en tant que matériau d'électrode de supercondensateur a été étudiée puisqu'il présente dans l'eau une fenêtre de stabilité électrochimique importante d'environ 3 V. L'intérêt de synthétiser des structures tridimensionnelles a été mis en évidence, en particulier une architecture de diamant « en aiguilles » permet de multiplier par 10 la capacité surfacique par rapport à une architecture plane. / This work deals with the study of electrode materials for supercapacitors. These storage devices have a significant power density of several kW/kg. Asymmetric systems have been developed in order to increase the energy density of these components while trying to maintain a high power density. They consist of a classic capacitive electrode made of activated carbon and a faradaic electrode. Two approaches have been broached regarding that non-blocking electrode: • Mainly, the use of lithium titanate Li4Ti5O12 which is a lithium insertion material usually used in Li-ion battery electrodes. It appeared that for hybrid systems including a negative electrode only made of Li4Ti5O12, the energy density is greatly reduced beyond 1 kW/kg. The use of composite negative electrodes made of activated carbon and Li4Ti5O12 is recommended so as to maintain good performances both in energy and power. Thus, for a power density of 2 kW/kg, the energy density of the developed hybrid system remains 1.5 superior to the one of an activated carbon / activated carbon symmetric system tested in the same conditions. • Secondly, the use of manganese dioxide MnO2, a pseudo-capacitive material involving redox reactions. The study has been focused on the synthesis of the metal oxide and then on the synthesis of a composite material by self-assembly. The aim is to aggregate small manganese dioxide particles around a carbon backbone. Such a microstructure offers a high specific surface area of active material directly in contact with a network having a good electronic conductivity. The obtained MnO2 + VGCF composite material has been tested as positive electrode in an asymmetric system, facing an activated carbon electrode. Thus, the stability window of the aqueous electrolyte has been multiplied by 1.5 compared to an activated carbon / activated carbon system. Finally, diamond has been considered as a supercapacitor electrode material in an explorative view since it offers a wide electrochemical stability window in water (around 3 V). The interest for tridimensional structures has been evidenced, e.g. a “needles” architecture allows to obtain a surfacic capacity ten times higher than the one obtained with a flat architecture.

Les techniques liées au vol en formation et aux opérations de proximité de satellites autonomes font partie des technologies opérationnelles spatiales les plus marquantes et les plus ambitieuses de ces dernières années. En particulier, cela nécessite la complète maitrise des phases de rendez-vous proche et de survol par un satellite actif avec un satellite, une station ou un débris passif. Le développement de systèmes GNC (Guidage Navigation Contrôle) associés performants et sûrs repose sur la connaissance d'un modèle dynamique réalisant un bon compromis entre faible complexité et prise en compte suffisante des principales caractéristiques dynamiques et cinématiques de ce type de systèmes. La première partie de cette thèse est consacrée au développement d'une modélisation unifiée de la dynamique relative couplée entre un satellite coopératif chasseur et un satellite cible non coopérative. En effet, lorsque deux satellites sont proches l'un de l'autre, ils ne peuvent plus être traités comme des masses ponctuelles, car leur forme et leur taille affectent le mouvement relatif entre les points de masse décentralisés, conduisant à un couplage des mouvements de translation et de rotation. Ce développement est abordé de manière progressive: le mouvement de translation relatif non linéaire est décrit sous hypothèses képlériennes dans le repère orbital de la cible ainsi que le modèle linéarisé associé. Ensuite, le modèle non linéaire d'attitude relative est présenté au moyen des paramètres d'Euler-Rodrigues. Enfin, le formalisme des quaternions duaux est utilisé afin d'obtenir le modèle relatif couplé en translation et en attitude. La phase de modélisation du mouvement relatif linéaire de translation a ainsi permis de mettre en évidence certaines transformations de coordonnées conduisant à une caractérisation intéressante des trajectoires périodiques du chasseur et ainsi de proposer un premier type de loi de contrôle de guidage pour la phase d'approche et de survol. Dans l'ensemble de notre travail, nous considérons un chasseur équipé de propulseurs chimiques et l'hypothèse classique des poussées impulsionnelles. Ce type de systèmes dynamiques conciliant dynamique continue et contrôle impulsionnel se définit naturellement comme une classe particulière de systèmes dynamiques hybrides. Plusieurs lois de contrôle hybrides sont alors proposées afin de stabiliser le chasseur sur une trajectoire de référence périodique proche de la cible. Les propriétés de stabilité et de convergence de ces différentes lois sont analysées et de nombreuses simulations numériques montrent les forces et les faiblesses de chaque contrôleur en termes d'indices de performance comme le temps de convergence, la consommation ainsi que des contraintes de sécurité. Dans un second temps, des contraintes opérationnelles supplémentaires (contraintes de visibilité par exemple) sont prises en considération en imposant une direction d'approche rectiligne (glideslope) au chasseur. Cette trajectoire impose au satellite chasseur de suivre une droite dans n'importe quelle direction du repère local reliant l'emplacement courant du chasseur à sa destination finale. Sous l'hypothèse de propulsion impulsionnelle, les résultats existant dans la littérature pour ce type d'approche ont été généralisés aux orbites elliptiques en identifiant une nouvelle formulation du problème comprenant des degrés de liberté utiles qui permettent de minimiser la consommation de carburant tout en contrôlant l'excursion de la trajectoire libre en dehors de la droite de glideslope en la confinant dans un couloir d'approche défini par l'utilisateur. La synthèse des lois de guidage ainsi obtenues repose sur la résolution de problèmes d'optimisation SDP dans le cas général ou linéaire pour les cas plus simples d'approche standards du type V-bar ou R-bar. / The techniques related to formation flying and proximity operations of autonomous satellites belong to the most significant and challenging operational space technologies of the last years. In particular, they require full mastery of the close-range rendezvous and observation phases by an active satellite with a passive satellite, station or debris. The development of efficient and safe associated GNC systems relies on the knowledge of a dynamic model that achieves a good trade-off between low complexity and sufficient inclusion of the main dynamic and kinematic characteristics of this type of systems.The first part of this thesis is devoted to the development of a unified modeling of the relative coupled dynamics between a cooperative chaser satellite and a non-cooperative target satellite. Indeed, when two satellites are close to each other, they can no longer be treated as point masses because their shape and size affect the relative motion between the decentralized points, leading to a translational-attitude motions coupling. This development is addressed in a progressive way: the relative nonlinear translational motion is described under Keplerian assumptions in the target's orbital reference frame, as well as the associated linearized model. Then, the nonlinear relative attitude model is presented by means of the Euler-Rodrigues parameters. Finally, the dual quaternion formalism is used to obtain the relative translational and attitude coupled model. The modeling phase concerning the linear relative translational motion has allowed us to highlight certain coordinates transformations leading to an interesting characterization of the chaser's periodic trajectories and thus, to propose a first type of control law for the close-phase rendezvous and observation phases.All along this work, we consider a chaser satellite equipped with chemical thrusters under the classical hypothesis of impulsive thrusts. This type of dynamic systems gathering continuous dynamics and impulsive control naturally belongs to a particular class of dynamical hybrid systems. Several hybrid control laws are then proposed in order to stabilize the chaser on a periodic reference trajectory close to the target. The stability and convergence properties of these different laws are analysed and several numerical simulations show the strengths and weaknesses of each controller in terms of performance indices such as convergence time, consumption and safety constraints. In a second step, additional operational constraints (line-of-sight constraints for example) are taken into account by imposing a rectilinear (glideslope) direction to the chaser. This trajectory requires the chaser satellite to follow a straight line in any direction of the local reference frame and connecting the current location of the chaser to its final destination. Under the impulsive propulsion assumptions, the results in the literature for this type of approach have been generalized to elliptic orbits by identifying a new formulation of the problem including useful degrees of freedom, which allow minimizing the fuel consumption while controlling the humps of the trajectory outside the glideslope line by enclosing it in a user-defined approach corridor. Guidance laws are therefore synthetized via the solution of an SDP optimisation problem in the general case and via a linear programming when considering standard cases like the V-bar or R-bar approaches.

Pour maintenir la tension dans des bornes admissibles, des régulations locales de puissance réactive (Q) en fonction de la tension (U) sont envisagées sur les réseaux de distribution. Ces travaux étudient l’impact de ces régulations sur la stabilité des réseaux de distribution accueillant de la production. Une étude empirique confirme le risque d’instabilité de la tension et souligne le lien avec les paramètres de la régulation. Pour aider les gestionnaires à les choisir, trois méthodes d’étude de la stabilité sont proposées. Tout d’abord, une méthode formelle fondée sur les notions d’abstraction discrète et de bisimulation est développée. Elle offre une grande précision au prix d’un effort de calcul important. Pour contournercette difficulté, un critère analytique portant sur le temps de réponse des régulations Q(U) est formulé. Ensuite, un critère valable dans tous les cas est proposé pour les codes de réseaux. Enfin, l’extension desméthodes à des cas plus complexes est discutée. / To maintain the voltage within specified limits, local control laws of distributed generators (DGs) reactive power (Q) with respect to their voltage (U) have been considered. This work studies the impact of Q(U) control laws on distribution feeders’voltage stability. An empirical study confirms the risk of voltage instability and highlights its dependence on control law parameters. To help distribution grid operators to choose these parameters, three methods assessing stability are formulated.First, a formal method based on discrete abstraction and bisimulation calculation is developed. The proposed approach yields precise results but with a high computational load. Then, to overcome this issue, an analytical criterion adapting Q(U) control laws response time with respect to grid parameters is formulated. Finally, a general criterion, valid in any cases, is established in order to be included in the grid codes. To conclude this work, extension to more complex cases is discussed.

Dans cette thèse, nous aborderons deux aspects fondamentaux qui se posent dans les systèmes de commande modernes du fait de l'interaction entre des processus en temps continu et des dispositifs numériques: la synthèse de lois de commande en présence de quantificateurs et l'estimation d'état en présence de mesures sporadiques. Une des caractéristiques principales de cette thèse consiste également à proposer des méthodes constructives pour résoudre les problèmes envisagés. Plus précisément, pour répondre à cette exigence, nous allons nous tourner vers une approche basée sur les inégalités matricielles linéaires (LMI). Dans la première partie de la thèse, nous proposons un ensemble d'outils constructifs basés sur une approche LMI, pour l'analyse et la conception de systèmes de commande quantifiés impliquant des modèles et des correcteurs linéaires. L'approche est basée sur l'utilisation des inclusions différentielles qui permet de modéliser finement le comportement de la boucle fermée et ainsi d'obtenir des résultats intéressants. Dans la seconde partie de la thèse, inspirés par certains schémas d'observation classiques présentés dans la littérature, nous proposons deux observateurs pour l'estimation de l'état d'un système linéaire en présence de mesures sporadiques, c'est-à-dire prenant en compte la nature discrète des mesures disponibles. De plus, en se basant sur une des deux solutions présentées, une architecture de commande basée observateur est proposée afin de stabiliser asymptotiquement un système linéaire en présence à la fois de mesures sporadiques et d'un accès intermittent à l'entrée de commande du système. / In this dissertation, two fundamental aspects arising in modern engineered control systems will be addressed:On the one hand, the presence of quantization in standard control loops. On the other hand, the state estimation in the presence of sporadic available measurements. These two aspects are addressed in two different parts. One of the main feature of this thesis consists of striving to derive computer-aided tools for the solution to the considered problems. Specifically, to meet this requirement, we revolve on a linear matrix inequalities (LMIs) approach. In the first part, we propose a set of LMI-based constructive Lyapunov-based tools for the analysis and the design of quantized control systems involving linear plants and linear controllers. The entire treatment revolves on the use of differential inclusions as modeling tools, and on stabilization of compact sets as a stability notion. In the second part of the thesis, inspired by some of the classical observation schemes presented in the literature of sampled-data observers, we propose two observers to exponentially estimate the state of a linear system in the presence of sporadic measurements. In addition, building upon one of the two observers, an observer-based controller architecture is proposed to asymptotically stabilize a linear plant in the presence of sporadic measurements and intermittent input access.