Cette thèse est consacrée à l'analyse algorithmique des systèmes hybrides. Nous examinons plusieurs problèmes liés à l'étude et au controle des systèmes hybrides linéaires par morceaux. Dans une première partie, nous présentons les notions de base de la théorie. Nous illustrons notre propos grace à de nombreux exemples. La deuxième partie est dédiée au calcul algorithmique des exécutions acceptées par un système hybride. Une méthode de détection des événements (changement de valeur de la variable discrète du système) est proposée. Le cas des exécutions périodiques est également examiné. Dans la troisième partie, nous abordons le problème du calcul de l'ensemble atteignable des systèmes hybrides. Nous apportons un soin particulier aux systèmes où les dynamiques continues sont connues de manière incertaine. Dans la quatrième partie, nous nous intéressons au controle des systèmes hybrides. Nous construisons une analyse multirésolution de l'espace des entrées d'un système linéaire et calculons une base d'ondelettes associée. Les propriétés de cette base se révèlent intéressantes pour la synthèse de signaux d'entrée d'un système hybride. Dans la dernière partie nous montrons que les techniques développées pour les systèmes hybrides linéaires par morceaux peuvent etre utilisées pour analyser des systèmes dynamiques non-linéaires.

Actuellement la nécessité des systèmes d'alimentation d'énergie, capables d'assurer un fonctionnement stable dans des domaines de fonctionnement assez larges avec des bonnes performances dynamiques (rapidité du système, variations limitées de la tension de sortie en réponse aux perturbations de charge ou de tension d'alimentation), devient de plus en plus importante. De ce fait, cette thèse est orientée sur la commande des convertisseurs de puissance DC-DC représentés par des modèles hybrides.En tenant compte de la structure variable de ces systèmes à commutation, un modèle hybride permet de décrire plus précisément le comportement dynamique d'un convertisseur dans son domaine de fonctionnement. Dans cette optique, l'approximation PWA est utilisée afin de modéliser les convertisseurs DC-DC. A partir des modèles hybrides développés, on s'est intéressé à la stabilisation des convertisseurs au moyen des correcteurs à gains commutés élaborés sur la base de fonctions de Lyapunov PWQ, et à l'implantation d'une commande prédictive explicite, en considérant des contraintes sur l'entrée de commande. La méthode de modélisation et les stratégies de commande proposées ont été appliquées sur deux topologies : un convertisseur buck, afin de mieux maîtriser le réglage des correcteurs et un convertisseur flyback avec filtre d'entrée. Cette dernière topologie nous a permis de répondre aux difficultés du point de vue de la commande (comportement à déphasage non-minimal) rencontrées dans la majorité des convertisseurs DC-DC. Les performances des commandes élaborées ont été validées en simulation sur les topologies considérées et expérimentalement sur une maquette du convertisseur buck.

Dans cette thèse nous développons des structures de supervision permettant de définir des consignes optimales pour des actionneurs thermiques, ainsi que des stratégies de commande appropriées pour le pilotage d'une pompe à chaleur (PAC). Pour répondre à ces objectifs, plusieurs étapes ont été réalisées :- Modélisation orientée commande d'une PAC réversible, des thermistances, et de l'environnement permettant de les lier à l'intérieur de l'habitacle. Des modèles physiques ont été définis et intégrés dans une plateforme du type Model-in-the-Loop pour permettre a posteriori la validation des stratégies de commande et d'optimisation. - Commande d'une PAC. La linéarisation du modèle de PAC autour de certains points de fonctionnement a permis le développement de la commande de l'actionneur principal. La structure de commande proposée permet de prendre en compte, en boucle fermée, des contraintes d'état et d'entrée du système. Les performances de cette structure ont été analysées en considérant successivement des régulateurs principaux de type PI et Hinf. Enfin, des algorithmes réalisant le pilotage d'un actionneur secondaire du système ont été également proposés. - Optimisation des actionneurs thermiques. L'utilisation combinée de thermistances et de la PAC présente des avantages en termes de réduction de la consommation énergétique et/ou du maintien de la puissance thermique demandée dans des conditions aux limites de fonctionnement. Le problème d'optimisation a été résolu en deux temps : des solutions hors-ligne ont été obtenues par résolution d'un problème mixte en nombre entier avec modèle prédictif, puis utilisées pour déduire des stratégies embarquables sur le véhicule.

La complexité inhérente à la coordination des mouvements d'un groupe de robots mobiles est traitée en investiguant plus avant les potentialités des architectures de contrôle comportementales dont le but est de briser la complexité des tâches à exécuter. En effet, les robots mobiles peuvent évoluer dans des environnements très complexes et nécessite de surcroît une coopération précise et sécurisée des véhicules pouvant rapidement devenir inextricable. Ainsi, pour maîtriser cette complexité, le contrôleur dédié à la réalisation de la tâche est décomposé en un ensemble de comportements/contrôleurs élémentaires (évitement d'obstacles et de collision entre les robots, attraction vers une cible, etc.) qui lient les informations capteurs (provenant de caméras, des capteurs locaux du robot, etc.) aux actionneurs des différentes entités robotiques. La tâche considérée est la navigation en formation en présence d'obstacles (statiques et dynamiques). La spécificité de l'approche théorique consiste à allier les avantages des architectures de contrôle comportementales à la méthode de la structure virtuelle où le groupe de robots mobiles suit un corps virtuel avec une dynamique (vitesse, direction) donnée. Ainsi, l'activation d'un comportement élémentaire en faveur d'un autre se fait en respectant les contraintes structurelles des robots (e.g. vitesses et accélérations maximales, etc.) en vue d'assurer le maximum de précision et de sécurité des mouvements coordonnés entre les différentes entités mobiles. La coopération consiste à se partager les places dans la structure virtuelle de manière distribuée et de façon à atteindre plus rapidement la formation désirée. Pour garantir les critères de performances visés par l'architecture de contrôle, les systèmes hybrides qui permettent de commander des systèmes continus en présence d'évènements discrets sont exploités. En effet, ces contrôleurs (partie discrète) permettent de coordonner l'activité des différents comportements (partie continue) disponibles au niveau de l'architecture, tout en offrant une analyse automaticienne rigoureuse de la stabilité de celle-ci au sens de Lyapunov. Chaque contribution est illustrée par des résultats de simulation. Le dernier chapitre est dédié à l'implémentation de l'architecture de contrôle proposée sur un groupe de robots mobiles Khepera III.

Ce travail de thèse s'inscrit dans la recherche des solutions économiquementviables pour des réseaux personnels à hauts débits (plusieurs Gbps à plusieursdizaines de Gbps) opérationnels en bande millimétrique autour de 60 GHz. Aucas où ces réseaux servent un nombre élevé d'utilisateurs, ils comprendront unemultitude d'antennes afin d'assurer l'accès sans fil rapide. Afin de réduire aumaximum le coût d'un module d'antenne, les réseaux doivent fournir un signalanalogue à des porteuses millimetriques. Une solution prometteuse pour les systèmesde distribution qui correspond à ces besoins sont des structures à fibreoptique, laquelle permet une transmission à faibles pertes et à haute bande passante.On parle de l'approche "radio-sur-fibre" (en anglais, radio-over-fiber). Laproblématique est de pouvoir générer et moduler un signal aux fréquences millimétriqueslors de la transmission optique - et ce avec des composant bas coûts.La technique utilisée dans le cadre de cette thèse est l'emploi des diodes laser àverrouillage de modes. Ces derniers vont pouvoir générer des hautes fréquencestout en ne nécessitant qu'une alimentation continue, et ils peuvent être modulésde manière directe ou externe. Les lasers à semi-conducteurs employés ici sontd'une génération encore à l'état d'étude puisqu'il s'agit des lasers à boites (ouîlots) quantiques. Ces lasers ont montrés de très bonnes capacités à générer dessignaux électriques aux fréquences autour de 60 GHz, bien qu'ayant encore, pourl'instant, à une stabilité de fréquence (ou de phase) limitée. Dans le cadre des systèmesde communication opto/micro-ondes, peu de travaux approfondis ont étémenés sur ces structures.Au cours de cette thèse, plusieurs études ont été effectuées. La première portesur les propriétés générales d'un système construit à partir de ce type de laser(puissances disponibles, figure de bruit, linéarité etc.). Une deuxième étude aété consacrée aux effets de la propagation des signaux dans les systèmes baséssur les lasers à verrouillage de modes, notamment de la dispersion chromatiquelaquelle a un effet considérable sur les distances de transmission. Les deux étudesmettent en avant l'importance d'une limitation du nombre de modes générés parla diode laser afin d'optimiser non seulement le gain du lien et la puissance RFrécupérée, mais aussi la figure de bruit du système. Lors d'une troisième étude, lastabilité en fréquence/phase s'est révélée critique, car le bruit de fréquence/phaselimite la qualité de la transmission en introduisant un plancher d'erreur mêmepour des rapports signal-a-bruit très élevés. Des différentes générations de lasersà boites (îlots) quantiques et à verrouillage de modes ont été testées. Le problèmedu bruit de fréquence et de phase persiste et ne peut pas être résolu en utilisantles techniques classiques comme les boucles à verrouillage de phase conventionnelles.Une solution pour ce problème a été développée pour les systèmes detransmission; elle permet simultanément un ajustement de fréquence supérieure(précision de quelques Hz à quelques kHz) à celle donnée par le processus de fabricationdes diodes lasers (précision de quelques GHz), ainsi qu'une stabilisationde fréquence et de phase.

Le secteur du bâtiment est un consommateur énergétique majeur, par conséquent, un cadre d’actions a été décidé au niveau international dans le but de limiter son impact. Afin de mettre en œuvre ces mesures, il est nécessaire d’avoir à disposition des modèles offrants une description fiable du comportement thermique des bâtiments. A cet effet, cette thèse propose l’application d’une nouvelle technique guidée par les données pour la modélisation thermique des bâtiments en se basant sur l’approche des systèmes hybrides, caractérisés par des dynamiques continues et événementielles. Ce choix est motivé par le fait qu’un bâtiment est un système complexe caractérisé par des phénomènes non-linéaires et l’apparition de différents événements. On utilise les modèles affines par morceaux ou PWARX pour l’identification de systèmes hybrides. C’est une collection de sous-modèles affines représentant chacun une configuration caractérisée par une dynamique particulière. Le manuscrit commence par un état de l’art sur les principales techniques de modélisation thermique des bâtiments. Ensuite, le choix d’une approche hybride est motivé par une interprétation mathématique basée sur les équations d’un circuit thermique. Ceci est suivi par une brève présentation des modèles hybrides et une description détaillée de la méthodologie utilisée. On montre ensuite comment utiliser la technique SVM pour classifier les nouvelles données. Enfin, l’intégration des modèles PWARX dans une boucle de contrôle hybride afin d’estimer le gain en performance énergétique d’un bâtiment après rénovation est présentée. La méthodologie est validée en utilisant des données issues de cas d’études variés. / The building sector is a major energy consumer, therefore, a framework of actions has been decided on by countries worldwide to limit its impact. For implementing such actions, the availability of models providing an accurate description of the thermal behavior of buildings is essential. For this purpose, this thesis proposes the application of a new data-driven technique for modeling the thermal behavior of buildings based on a hybrid system approach. Hybrid systems exhibit both continuous and discrete dynamics. This choice is motivated by the fact that a building is a complex system characterized by nonlinear phenomena and the occurrence of different events. We use a PieceWise AutoRegressive eXogeneous inputs (PWARX) model for the identification of hybrid systems. It is a collection of sub-models where each sub-model is an ARX equation representing a certain configuration in the building characterized by its own dynamics. This thesis starts with a state-of-the-art on building thermal modeling. Then, the choice of a hybrid system approach is motivated by a mathematical interpretation based on the equations derived from an RC thermal circuit of a building zone. This is followed by a brief background about hybrid system identification and a detailed description of the PWARX methodology. For the prediction phase, it is shown how to use the Support Vector Machine (SVM) technique to classify new data to the right sub-model. Then, it is shown how to integrate these models in a hybrid control loop to estimate the gain in the energy performance for a building after insulation work. The performance of the proposed technique is validated using data collected from various test cases.

Il s'agit d'une étude menée sur les systèmes cyber-physiques sur trois aspects principaux: la vérification de la stabilité, l'ordonnancement et la synthèse des paramètres. Les systèmes de contrôle embarqués (ECS) agissant dans le cadre de contrats temporels sont la classe considérée de systèmes cyber-physiques dans la thèse. ECS fait référence à des intégrations d'un dispositif informatique avec le système physique. En ce qui concerne les contrats temporels, ils sont des contraintes de temps sur les instants où se produisent certains événements tels que l'échantillonnage, l'actionnement et le calcul. Ces contrats sont utilisés pour modéliser les problèmes qui se posent dans les systèmes de contrôle modernes: incertitudes sur les retards d'actionnement, les périodes d'échantillonnage incertaines et l'interaction de plusieurs systèmes physiques avec des ressources informatiques partagées (CPUs). Maintenant, compte tenu d'un ECS et d'un contrat temporel, nous reformulons le système de manière impulsionnelle et vérifions la stabilité du système, sous toutes les incertitudes bornées et données par le contrat, en utilisant des techniques d'approximation convexe et de nouveaux résultats généralisés pour le problème sur une classe de systèmes modélisés dans le cadre des inclusions différentielles. Deuxièmement, compte tenu d'un ensemble de contrôleurs implémentés sur une plate-forme de calcul commune (CPUs), dont chacun est soumis à un contrat de synchronisation, et à son meilleur et son plus mauvais cas d'exécution dans chaque CPU, nous synthétisons une politique d’ordonnancement dynamique qui garantit que chaque contrat temporel est satisfait et que chacun des CPU partagés est attribué à au plus un contrôleur à tout moment. L'approche est basée sur une reformulation qui nous permet d'écrire le problème d’ordonnancement comme un jeu temporelle avec spécification de sureté. Ensuite, en utilisant l'outil UPPAAL-TIGA, une solution au jeu fournit une politique d’ordonnancement appropriée. En outre, nous fournissons une nouvelle condition nécessaire et suffisante pour l’ordonnancement des tâches de contrôle en fonction d’un jeu temporisé simplifiés. Enfin, nous résolvons un problème de synthèse de paramètres qui consiste à synthétiser une sous-approximation de l'ensemble des contrats de synchronisation qui garantissent en même temps l’ordonnancement et la stabilité des contrôleurs intégrés. La synthèse est basée sur un nouveau paramétrage du contrat temporel pour les rendre monotones, puis sur un échantillonnage à plusieurs reprises de l'espace des paramètres jusqu'à atteindre une précision d'approximation prédéfinie. / This is a study conducted on cyber-physical systems on three main aspects: stability verification, scheduling, and parameter synthesis. Embedded control systems (ECS) acting under timing contracts are the considered class of cyber-physical systems in the thesis. ECS refers to integrations of a computing device with the physical system. As for timing contracts they are time constraints on the instants where some events happen such as sampling, actuation, and computation. These contracts are used to model issues that arise in modern embedded control systems: uncertain sampling to actuation delays, uncertain sampling periods, and interaction of several physical systems with shared computational resources (CPUs). Now given an ECS and a timing contract we reformulate the system into an impulsive one and verifies stability of the system, under all possible bounded uncertainties given by the contract, using safe convex approximation techniques and new generalized results for the problem on a class of systems modeled in the framework of difference inclusions. Second given a set of controllers implemented on a common computational platform (CPUs), each of which is subject to a timing contract, and best and worst case execution times on each CPU, we synthesize a dynamic scheduling policy, which guarantees that each timing contract is satisfied and that each of the shared CPUs are allocated to at most one embedded controller at any time. The approach is based on a timed game formulation that allows us to write the scheduling problem as a timed safety game. Then using the tool UPPAAL-TIGA, a solution to the safety game provides a suitable scheduling policy. In addition, we provide a novel necessary and sufficient condition for schedulability of the control tasks based on a simplified timed game automaton. Last, we solve a parameter synthesis problem which consists of synthesizing an under-approximation of the set of timing contracts that guarantee at the same time the schedulability and stability of the embedded controllers. The synthesis is based on a re-parameterization of the timing contract to make them monotonic, and then on a repeatedly sampling of the parameter space until reaching a predefined precision of approximation.

Cette étude s’inscrit dans le domaine de la gestion de santé des systèmes, qui vise à développer des outils d’aide à la maintenance, mais également à améliorer les prises de décision en autonomie des systèmes en cas de pannes. Dans ce cadre, des techniques de diagnostic déterminent si et pourquoi le système est en panne, alors que des techniques de pronostic déterminent quand les pannes vont survenir et leurs conséquences. Si elles semblent être corrélées, elles sont généralement étudiées séparément, car les échelles de temps manipulées par les deux processus sont très différentes.Ces travaux ont pour objectif de développer un outil intégrant les méthodes de diagnostic et de pronostic pour la surveillance des système hybrides, dont les dynamiques sont à la fois continues et discrètes. La méthodologie proposée, basée sur les réseaux de Petri hybrides particulaires, est appliquée sur un rover planétaire pour démontrer son utilisabilité en cas réel à travers la gestion des incertitudes liées au système et aux données / This study takes place in the field of system health management, which aims at developing maintenance aid tools, but also at improving the systems autonomous decision-making in case of failures. In this context, diagnostic techniques determine whether and why the system is down, while prognostic techniques determine when failures will occur and their consequences. If they seem to be correlated, they are usually studied separately because the time scales manipulated by the two processes are very different. This work aims at developing a tool that integrates both diagnosis and prognosis methods for the monitoring of hybrid systems, whose dynamics are both continuous and discrete. The proposed methodology, based on hybrid particle Petri nets, is applied to a planetary rover to demonstrate its usability in real cases through the management of knowledge-based and data-based uncertainty

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. / In this thesis, we presented our contributions to the formal analysis of dynamical systems. We focused on the problem of efficiently computing an accurate approximation of the reachable sets under nonlinear dynamics given by differential equations. Our aim was also to design scalable methods which can handle large systems. The first contribution of this thesis concerns the dynamic hybridization technique for a large class of nonlinear systems. We focused on the hybridization domain construction such that the linear interpolation realized in this domain ensures a desired error between the original system trajectories and those computed with the approximated system. We propose a construction method which tends to maximize the domain volume which reduce the number of creation of new domains during the analysis. The second research direction that we followed concerns a subclass of nonlinear dynamical systems which are the polynomial systems. Our results for the reachability analysis of these systems are based on the Bernstein expansion properties. We approximate an initial reachability computation (which requires solving polynomial optimization problems) with an accurate over-approximation (which requires solving linear optimization problems). The last theoretical contribution concerns the reachability analysis of linear systems with polyhedral input which often result from approximation of nonlinear systems. We proposed a technique to refine

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. / This thesis studies the automatic verification of safety properties of logico-numerical discrete and hybrid systems. These systems have Boolean and numerical variables and exhibit discrete and continuous behavior. Our approach is based on static analysis using abstract interpretation. We address the following issues: Numerical abstract interpretation methods require the enumeration of the Boolean states, and hence, they suffer from the state space explosion problem. Moreover, there is a precision loss due to widening operators used to guarantee termination of the analysis. Furthermore, we want to make abstract interpretation-based analysis methods accessible to simulation languages for hybrid systems. In this thesis, we first generalize abstract acceleration, a method that improves the precision of the inferred numerical invariants. Then, we show how to extend abstract acceleration and max-strategy iteration to logico-numerical programs while improving the trade-off between efficiency and precision. Concerning hybrid systems, we translate the Zelus hybrid synchronous programming language to logico-numerical hybrid automata and extend logico-numerical analysis methods to hybrid systems. Finally, we implemented the proposed methods in ReaVer, a REActive System VERification tool, and provide experimental results. Concluding, this thesis proposes a unified approach to the verification of discrete and hybrid logico-numerical systems based on abstract interpretation, which is capable of integrating sophisticated numerical abstract interpretation methods while successfully trading precision for efficiency.