Les Systèmes Cyber Physiques (CPS) intègrent des composants programmables afin de contrôler un processus physique. Ils sont désormais largement répandus dans différentes industries comme l’énergie, l’aéronautique, l’automobile ou l’industrie chimique. Parmi les différents CPS existants, les systèmes SCADA (Supervisory Control And Data Acquisition) permettent le contrôle et la supervision des installations industrielles critiques. Leur dysfonctionnement peut engendrer des impacts néfastes sur l’installation et son environnement.Les systèmes SCADA ont d’abord été isolés et basés sur des composants et standards propriétaires. Afin de faciliter la supervision du processus industriel et réduire les coûts, ils intègrent de plus en plus les technologies de communication et de l’information (TIC). Ceci les rend plus complexes et les expose à des cyber-attaques qui exploitent les vulnérabilités existantes des TIC. Ces attaques peuvent modifier le fonctionnement du système et nuire à sa sûreté.On associe dans la suite la sûreté aux risques de nature accidentelle provenant du système, et la sécurité aux risques d’origine malveillante et en particulier les cyber-attaques. Dans ce contexte où les infrastructures industrielles sont contrôlées par les nouveaux systèmes SCADA, les risques et les exigences liés à la sûreté et à la sécurité convergent et peuvent avoir des interactions mutuelles. Une analyse de risque qui couvre à la fois la sûreté et la sécurité est indispensable pour l’identification de ces interactions ce qui conditionne l’optimalité de la gestion de risque.Dans cette thèse, on donne d’abord un état de l’art complet des approches qui traitent la sûreté et la sécurité des systèmes industriels et on souligne leur carences par rapport aux quatre critères suivants qu’on juge nécessaires pour une bonne approche basée sur les modèles : formelle, automatique, qualitative et quantitative, et robuste (i.e. intègre facilement dans le modèle des variations d’hypothèses sur le système).On propose ensuite une nouvelle approche orientée modèle d’analyse conjointe de la sûreté et de la sécurité : S-cube (SCADA Safety and Security modeling), qui satisfait les critères ci-dessus. Elle permet une modélisation formelle des CPS et génère l’analyse de risque qualitative et quantitative associée. Grâce à une modélisation graphique de l’architecture du système, S-cube permet de prendre en compte différentes hypothèses et de générer automatiquement les scenarios de risque liés à la sûreté et à la sécurité qui amènent à un évènement indésirable donné, avec une estimation de leurs probabilités.L’approche S-cube est basée sur une base de connaissance (BDC) qui décrit les composants typiques des architectures industrielles incluant les systèmes d’information, le contrôle et la supervision, et l’instrumentation. Cette BDC a été conçue sur la base d’une taxonomie d’attaques et modes de défaillances et un mécanisme de raisonnement hiérarchique. Elle a été mise en œuvre à l’aide du langage de modélisation Figaro et ses outils associés. Afin de construire le modèle du système, l’utilisateur saisit graphiquement l’architecture physique et fonctionnelle (logiciels et flux de données) du système. L’association entre la BDC et ce modèle produit un modèle d’états dynamiques : une chaîne de Markov à temps continu. Pour limiter l’explosion combinatoire, cette chaîne n’est pas construite mais peut être explorée de deux façons : recherche de séquences amenant à un évènement indésirable ou simulation de Monte Carlo, ce qui génère des résultats qualitatifs et quantitatifs.On illustre enfin l’approche S-cube sur un cas d’étude réaliste : un système de stockage d’énergie par pompage, et on montre sa capacité à générer une analyse holistique couvrant les risques liés à la sûreté et à la sécurité. Les résultats sont ensuite analysés afin d’identifier les interactions potentielles entre sûreté et sécurité et de donner des recommandations. / Cyber physical systems (CPS) denote systems that embed programmable components in order to control a physical process or infrastructure. CPS are henceforth widely used in different industries like energy, aeronautics, automotive, medical or chemical industry. Among the variety of existing CPS stand SCADA (Supervisory Control And Data Acquisition) systems that offer the necessary means to control and supervise critical infrastructures. Their failure or malfunction can engender adverse consequences on the system and its environment.SCADA systems used to be isolated and based on simple components and proprietary standards. They are nowadays increasingly integrating information and communication technologies (ICT) in order to facilitate supervision and control of the industrial process and to reduce exploitation costs. This trend induces more complexity in SCADA systems and exposes them to cyber-attacks that exploit vulnerabilities already existent in the ICT components. Such attacks can reach some critical components within the system and alter its functioning causing safety harms.We associate throughout this dissertation safety with accidental risks originating from the system and security with malicious risks with a focus on cyber-attacks. In this context of industrial systems supervised by new SCADA systems, safety and security requirements and risks converge and can have mutual interactions. A joint risk analysis covering both safety and security aspects would be necessary to identify these interactions and optimize the risk management.In this thesis, we give first a comprehensive survey of existing approaches considering both safety and security issues for industrial systems, and highlight their shortcomings according to the four following criteria that we believe essential for a good model-based approach: formal, automatic, qualitative and quantitative and robust (i.e. easily integrates changes on system into the model).Next, we propose a new model-based approach for a safety and security joint risk analysis: S-cube (SCADA Safety and Security modeling), that satisfies all the above criteria. The S-cube approach enables to formally model CPS and yields the associated qualitative and quantitative risk analysis. Thanks to graphical modeling, S-cube enables to input the system architecture and to easily consider different hypothesis about it. It enables next to automatically generate safety and security risk scenarios likely to happen on this architecture and that lead to a given undesirable event, with an estimation of their probabilities.The S-cube approach is based on a knowledge base that describes the typical components of industrial architectures encompassing information, process control and instrumentation levels. This knowledge base has been built upon a taxonomy of attacks and failure modes and a hierarchical top-down reasoning mechanism. It has been implemented using the Figaro modeling language and the associated tools. In order to build the model of a system, the user only has to describe graphically the physical and functional (in terms of software and data flows) architectures of the system. The association of the knowledge base and the system architecture produces a dynamic state based model: a Continuous Time Markov Chain. Because of the combinatorial explosion of the states, this CTMC cannot be exhaustively built, but it can be explored in two ways: by a search of sequences leading to an undesirable event, or by Monte Carlo simulation. This yields both qualitative and quantitative results.We finally illustrate the S-cube approach on a realistic case study: a pumped storage hydroelectric plant, in order to show its ability to yield a holistic analysis encompassing safety and security risks on such a system. We investigate the results obtained in order to identify potential safety and security interactions and give recommendations.

La gestion des suites chirurgicales joue un rôle central pour permettre aux hôpitaux d’offrir l’accès aux soins à des coûts raisonnables. L'informatisation et l'automatisation sont des évolutions conventionnelles pour améliorer l’efficacité. Toutefois, un soutien inadapté ne peut améliorer l'activité de gestion et peut nuire à son action. Notre hypothèse est que des fonctionnalités interactives, utilisables, flexibles et adaptée aux spécificités des activités locales peuvent créer un environnement de travail dans lequel le personnel médical est capable de réagir à des événements inattendus et de s’approprier la technologie. Nos contributions comprennent en une analyse de l'activité de l'équipe chirurgicale, basée sur des entretiens, observations, une revue de la littérature et une analogie avec l'aviation civile. Nous avons participé à la construction d'un modèle mathématique du flux chirurgical et d'une visualisation de ce modèle. Nous avons identifié les exigences et principes de conception nécessaires au développement, à l'intégration et à l'appropriation d'un outil pour soutenir la gestion du flux chirurgical. Nous avons conçu des interactions multi-utilisateurs sur une grande surface et développé un prototype de tableau blanc électronique, OnBoard, qui démontre l'intégration des spécifications et des défis techniques. OnBoard appartient à un système cyber-physique comprenant des capteurs dans les salles d'opération. Enfin, nous avons déployé et évalué OnBoard dans une suite chirurgicale. L'expérience de OnBoard suggère que la conception des interactions est primordiale pour offrir un environnement collaboratif efficace au personnel médical. / Surgical suite management plays a key role in the endeavor of hospitals: patients’ health at sustainable cost. Computerization and automation of processes are conventional solutions to support resource management and efficiency. However, unsuitable support might not improve the management activity, and can even be detrimental to it. Our hypothesis is that usable and flexible interactivity tuned to local particularities can create a working environment in which the medical staff can cope with unexpected surgery events and appropriate the technology. Our contributions comprise an analysis of the activity of the surgical team, based on interviews, observations, review of the literature and an analogy with civil aviation. We participated in the construction of a mathematical model of the surgical workflow and a visualization of the mathematical model. We conducted an experimentation to identify bottlenecks of workflow inefficiencies and delays. We identified scenarios, requirements and design principles necessary to the development, integration and acceptation of a tool to support surgical workflow activities. We designed multi-users interactions on a large surface and made a prototype of electronic whiteboard, OnBoard, for the surgical suite which demonstrates the integration of the specifications and technical challenges. OnBoard belongs to a larger cyber physical system including activity sensors in every operating room of the surgical suite. Finally, we deployed the prototype in a surgical suite and evaluated it. The OnBoard experience suggests that the design of interactions is paramount to provide the medical staff an efficient collaborative environment.

Les systèmes cyber-physiques mélangent des comportements physiques continus, tel la vitesse d'un véhicule, et des comportement discrets, tel que le régulateur de vitesse d'un véhicule. Ils sont désormais omniprésents dans notre société. Un grand nombre de ces systèmes sont dits critiques, i.e. une mauvaise conception entraînant un comportement non prévu, un bug, peut mettre en danger des êtres humains. Il est nécessaire de développer des méthodes pour garantir le bon fonctionnement de tels systèmes. Les méthodes formelles regroupent des procédés mathématiques pour garantir qu'un système se comporte comme attendu, par exemple que le régulateur de vitesse n'autorise pas de dépasser la vitesse maximale autorisée. De récents travaux ont permis des progrès significatifs dans ce domaine, mais l'approche adoptée est encore monolithique, i.e. que le système est modélisé d'un seul tenant et est ensuite soumis à la preuve. Notre problématique est comment modéliser efficacement des systèmes cyber-physiques dont la complexité réside dans une répétition de morceaux élémentaires. Et une fois que l'on a obtenu une modélisation, comment garantir le bon fonctionnement de tels systèmes. Notre approche consiste à modéliser le système de manière compositionnelle. Plutôt que de vouloir le modéliser d'un seul tenant, il faut le faire morceaux par morceaux, appelés composants. Chaque composant correspond à un sous-système du système final qu'il est simple de modéliser. On obtient le système complet en assemblant les composants ensembles. Ainsi une usine de traitement des eaux est obtenue en assemblant différentes cuves. L'intérêt de cette méthode est qu'elle correspond à l'approche des ingénieurs dans l'industrie : considérer des éléments séparés que l'on compose ensuite. Mais cette approche seule ne résout pas le problème de la preuve de bon fonctionnement du système. Il faut aussi rendre la preuve compositionnelle. Pour cela, on associe à chaque composant des propriétés sur ses entrées et sortie, et on prouve qu'elles sont respectées. Cette preuve peut être effectué par un expert, mais aussi par un ordinateur si les composants sont de tailles raisonnables. Il faut ensuite nous assurer que lors de l'assemblage des composants, les propriétés continuent à être respectées. Ainsi, la charge de la preuve est reportée sur les composants élémentaires, l'assurance du respect des propriétés désirées est conservée lors des étapes de composition. On peut alors obtenir une preuve du bon fonctionnement de systèmes industriels avec un coût de preuve réduit. Notre contribution majeure est de proposer une telle approche compositionnelle à la fois pour modéliser des systèmes cyber-physiques, mais aussi pour prouver qu'ils respectent les propriétés voulues. Ainsi, à chaque étape de la conception, on s'assure que les propriétés sont conservées, si possible à l'aide d'un ordinateur. Le système résultant est correct par construction. De ce résultat, nous avons proposé plusieurs outils pour aider à la conception de systèmes cyber-physiques de manière modulaire. On peut raisonner sur les propriétés temporelles de tels systèmes, par exemple est-ce que le temps de réaction d'un contrôleur est suffisamment court pour garantir le bon fonctionnement. On peut aussi raisonner sur des systèmes où un mode nominal cohabite avec un mode d'urgence. / Cyber-physical systems mix continuous physical behaviors, e.g. the velocity of a vehicle, and discrete behaviors, e.g. the cruise-controller of the vehicle. They are pervasive in our society. Numerous of such systems are safety-critical, i.e. a design error which leads to an unexpected behavior can harm humans. It is mandatory to develop methods to ensure the correct functioning of such systems. Formal methods is a set of mathematical methods that are used to guarantee that a system behaves as expected, e.g. that the cruise-controller does not allow the vehicle to exceed the speed limit. Recent works have allowed significant progress in the domain of the verification of cyber-physical systems, but the approach is still monolithic. The system under consideration is modeled in one block. Our problematic is how to efficiently model cyber-physical systems where the complexity lies in a repetition of elementary blocks. And once this modeling done, how guaranteeing the correct functioning of such systems. Our approach is to model the system in a compositional manner. Rather than modeling it in one block, we model it pieces by pieces, called components. Each component correspond to a subsystem of the final system and are easier to model due to their reasonable size. We obtain the complete system by assembling the different components. A water-plant will thus be obtained by the composition of several water-tanks. The main advantage of this method is that it corresponds to the work-flow in the industry : consider each elements separately and compose them later. But this approach does not solve the problem of the proof of correct functioning of the system. We have to make the proof compositional too. To achieve it, we associate to each component properties on its inputs and outputs, then prove that they are satisfied. This step can be done by a domain expert, but also by a computer program if the component is of a reasonable size. We have then to ensure that the properties are preserved through the composition. Thus, the proof effort is reported to elementary components. It is possible to obtain a proof of the correct functioning of industrial systems with a reduced proof effort. Our main contribution is the development of such approach in Differential Dynamic Logic. We are able to modularly model cyber-physical systems, but also prove their correct functioning. Then, at each stage of the design, we can verify that the desired properties are still guaranteed. The resulting system is correct-by-construction. From this result, we have developed several tools to help for the modular reasoning on cyber-physical systems. We have proposed a methodology to reason on temporal properties, e.g. if the execution period of a controller is small enough to effectively regulate the continuous behavior. We have also showed how we can reason on functioning modes in our framework.

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.

Les dernières années ont vu le développement de recherches portant sur l'interaction physique entre les robots aériens et leur environnement, accompagné de l'apparition de nombreux nouveaux systèmes mécaniques et approches de régulation. La communauté centrée autour de la robotique aérienne observe actuellement un déplacement de paradigmes des approches classiques de guidage, de navigation et de régulation vers des tâches moins triviales, telle le développement de l'interaction physique entre robots aériens et leur environnement. Ceci correspond à une extension des tâches dites de manipulation, du sol vers les airs. Cette thèse contribue au domaine de la manipulation aérienne en proposant un nouveau concept appelé MAGMaS, pour " Multiple Aerial Ground Manipulator System ". Les motivations qui ont conduites à l'association de manipulateurs terrestres et aériens pour effectuer des tâches de manipulation coopérative, résident dans une volonté d'exploiter leurs particularités respectives. Les manipulateurs terrestres apportant leur importante force et les manipulateurs aériens apportant leur vaste espace de travail. La première contribution de cette thèse présente une modélisation rigoureuse des MAGMaS. Les propriétés du système ainsi que ses possibles extensions sont discutées. Les méthodes de planning, d'estimation et de régulation nécessaire à l'exploitation des MAGMaS pour des tâches de manipulation collaborative sont dérivées. Ce travail propose d'exploiter les redondances des MAGMaS grâce à un algorithme optimal d'allocation de forces entre les manipulateurs. De plus, une méthode générale d'estimation de forces pour robots aériens est introduite. Toutes les techniques et les algorithmes présentés dans cette thèse sont intégrés dans une architecture globale, utilisée à la fois pour la simulation et la validation expérimentale. Cette architecture est en outre augmentée par l'addition d'une structure de télé-présence, afin de permettre l'opération à distances des MAGMaS. L'architecture générale est validée par une démonstration de levage de barre, qui est une application représentative des potentiels usages des MAGMaS. Une autre contribution relative au développement des MAGMaS consiste en une étude exploratoire de la flexibilité dans les objets manipulés par un MAGMaS. Un modèle du phénomène vibratoire est dérivé afin de mettre en exergue ses propriétés en termes de contrôle. La dernière contribution de cette thèse consiste en une étude exploratoire sur l'usage des actionneurs à raideur variable dans les robots aériens, dotant ces systèmes d'une compliance mécanique intrinsèque et de capacité de stockage d'énergie. Les fondements théoriques sont associés à la synthèse d'un contrôleur non-linéaire. L'approche proposée est validée par le biais d'expériences reposant sur l'intégration d'un actionneur à raideur variable léger sur un robot aérien. / In recent years, the subject of physical interaction for aerial robots has been a popular research area with many new mechanical designs and control approaches being proposed. The aerial robotics community is currently observing a paradigm shift from classic guidance, navigation, and control tasks towards more unusual tasks, for example requesting aerial robots to physically interact with the environment, thus extending the manipulation task from the ground into the air. This thesis contributes to the field of aerial manipulation by proposing a novel concept known has Multiple Aerial-Ground Manipulator System or MAGMaS, including what appears to be the first experimental demonstration of a MAGMaS and opening a new route of research. The motivation behind associating ground and aerial robots for cooperative manipulation is to leverage their respective particularities, ground robots bring strength while aerial robots widen the workspace of the system. The first contribution of this work introduces a meticulous system model for MAGMaS. The system model's properties and potential extensions are discussed in this work. The planning, estimation and control methods which are necessary to exploit MAGMaS in a cooperative manipulation tasks are derived. This works proposes an optimal control allocation scheme to exploit the MAGMaS redundancies and a general model-based force estimation method is presented. All of the proposed techniques reported in this thesis are integrated in a global architecture used for simulations and experimental validation. This architecture is extended by the addition of a tele-presence framework to allow remote operations of MAGMaS. The global architecture is validated by robust demonstrations of bar lifting, an application that gives an outlook of the prospective use of the proposed concept of MAGMaS. Another contribution in the development of MAGMaS consists of an exploratory study on the flexibility of manipulated loads. A vibration model is derived and exploited to showcase vibration properties in terms of control. The last contribution of this thesis consists of an exploratory study on the use of elastic joints in aerial robots, endowing these systems with mechanical compliance and energy storage capabilities. Theoretical groundings are associated with a nonlinear controller synthesis. The proposed approach is validated by experimental work which relies on the integration of a lightweight variable stiffness actuator on an aerial robot.

Cette thèse porte sur le développement d'approches compositionnelles et efficaces de synthèse de contrôleurs pour les systèmes cyber-physiques (CPS). En effet, alors que les techniques de conception des CPS basées sur des modèles ont fait l'objet de nombreuses études au cours de la dernière décennie, leur scalabilité reste problématique. Dans cette thèse, nous contribuons à rendre de telles approches plus évolutives.La première partie est axée sur les approches compositionnelles. Un cadre général pour le raisonnement compositionnel en utilisant des contrats d’hypothèse-garantie est proposé. Ce cadre est ensuite combiné avec des techniques de contrôle symbolique et appliqué à un problème de synthèse de contrôleur pour des systèmes échantillonnés, distribués et multipériodiques, où l'approche symbolique est utilisé pour synthétiser un contrôleur imposant un contrat donné. Ensuite, une nouvelle approche de calcul compositionnel des abstractions symboliques est proposée, basée sur la notion de composition approchée et permettant de traiter des abstractions hétérogènes.La deuxième partie de la thèse porte sur des techniques efficaces d'abstraction et de synthèse de contrôleurs. Deux nouvelles techniques de calcul d’abstractions sont proposées pour les systèmes à commutation incrémentalement stables. La première approche est basée sur l'échantillonnage multi-niveaux où nous avons établi l'existence d'un paramètre optimal d'échantillonnage qui aboutit à un modèle symbolique avec un nombre minimal de transitions. La deuxième approche est basée sur un échantillonnage événementiel, où la durée des transitions dans le modèle symbolique est déterminée par un mécanisme déclencheur, ce qui permet de réduire le conservatisme par rapport au cas périodique. La combinaison avec des techniques de synthèse de contrôleurs paresseux est proposée permettant la synthèse à un coût de calcul réduit. Enfin, une nouvelle approche de synthèse paresseuse a été développée pour les systèmes de transition monotones et les spécifications de sécurité dirigées. Plusieurs études de cas sont considérées dans cette thèse, telles que la régulation de la température dans les bâtiments, le contrôle des convertisseurs de puissance, le pilotage des véhicules et le contrôle de la tension dans les micro-réseaux DC. / This thesis focus on the development of compositional and efficient controller synthesis approaches for cyber-physical systems (CPS). Indeed, while model-based techniques for CPS design have been the subject of a large amount of research in the last decade, scalability of these techniques remains an issue. In his thesis, we contribute to make such approaches more scalable.The focus of the first part is on compositional approaches. A general framework for compositional reasoning using assume-guarantee contracts is proposed. This framework is then combined with symbolic control techniques and applied to a controller synthesis problem for multiperiodic distributed sampled-data systems, where symbolic approaches have been used to synthesize controllers enforcing a given assume-guarantee contract. Then, a new approach to the compositional computation of symbolic abstractions is proposed based on the notion of approximate composition, allowing to deal with heterogeneous abstractions and arbitrary interconnections.The second part is about efficient abstraction and controller synthesis techniques. Two new abstractions schemes have been developed for incrementally stable switched systems. The first approach is based on multirate sampling where we established the existence of an optimal multirate sampling parameter that results in a symbolic model with a minimal number of transitions. The second approach is based on event-based sampling, where the duration of transitions in the symbolic model is determined by some triggering mechanism, which makes it possible to reduce the conservatism with respect to the periodic case. Combination with lazy controller synthesis techniques has been proposed allowing the synthesis at a reduced computational cost. Finally, a new lazy approach has been develop for monotone transition systems and directed safety specifications. Several case studies have been considered in this thesis such as temperature regulation in buildings, control of power converters, vehicle platooning and voltage control in DC micro-grids.

L'électronique a connu une évolution incontestable ces dernières années. Les progrès réalisés, notamment dans l'électronique numérique et l'intégration des circuits, ont abouti à des systèmes plus performants, miniatures et à faible consommation énergétique. Les évolutions technologiques, alliant les avancées de l'informatique et des technologies numériques et leur intégration de plus en plus poussée au sein d'objets multiples, ont permis le développement d'un nouveau paradigme de systèmes qualifiés de systèmes cyber-physiques. Ces systèmes sont massivement déployés de nos jours grâce à l'expansion des applications liées à l'Internet Des Objets (IDO). Les systèmes cyber-physiques s'appuient, entre autre, sur le déploiement massif de capteurs communicants sans fil autonomes, ceux-ci présentent plusieurs avantages : * Flexibilité dans le choix de l'emplacement. Ils permettent l'accès à des zones dangereuses ou difficiles d'accès. * Affranchissement des câbles qui présentent un poids, un encombrement et un coût supplémentaire. * Elimination des problèmes relatifs aux câbles (usure, étanchéité...) * Facilité de déploiement de réseaux de capteurs Cependant, ces capteurs sans fils nécessitent une autonomie énergétique afin de fonctionner. Les techniques conventionnelles telles que les batteries ou les piles, n'assurent le fonctionnement des capteurs que pour une durée limitée et nécessitent un changement périodique. Ceci présente un obstacle dans le cas où les capteurs sans fils sont placés dans un endroit où l'accès est impossible. Il est donc nécessaire de trouver un autre moyen d'approvisionner l'énergie de façon permanente à ces réseaux de capteurs sans fil. L'intégration et la miniaturisation des systèmes électroniques ont permis la réalisation de systèmes à faible consommation, ce qui a fait apparaître d'autres techniques en termes d'apports énergétiques. Parmi ces possibilités se trouvent la récupération d'énergie électromagnétique et le transfert d'énergie sans fil (TESF). En effet, l'énergie électromagnétique est de nos jours, omniprésente sur notre planète, l'utiliser donc comme source d'énergie pour les systèmes électroniques semble être une idée plausible et réalisable. Cette thèse s'inscrit dans ce cadre, elle a pour objectif la conception et la fabrication de systèmes de récupération d'énergie électromagnétique pour l'alimentation de réseaux de capteurs sans fil. Le circuit de récupération d'énergie électromagnétique est appelé " Rectenna ", ce mot est l'association de deux entités qui sont " antenne " et " rectifier " qui désigne en anglais le " redresseur ". L'antenne permet de récupérer l'énergie électromagnétique ambiante et le redresseur la convertit en un signal continu (DC) qui servira par la suite à alimenter les capteurs sans fil. Dans ce manuscrit, plusieurs rectennas seront présentées, pour des fréquences allant des bandes GSM 868MHz, 915MHz, passant par l'UMTS à 2GHZ et WIFI à 2,45GHz, et allant jusqu'aux bandes Ku et Ka. / The electronic domain has known a significant expansion the last decades, all the advancements made has led to the development of miniature and efficient electronic devices used in many applications such as cyber physical systems. These systems use low-power wireless sensors for: detection, monitoring and so on. The use of wireless sensors has many advantages: * The flexibility of their location, they allow the access to hazardous areas. * The realization of lighter system, less expensive and less cumbersome. * The elimination of all the problems associated to the cables (erosion, impermeability...) * The deployment of sensor arrays. Therefore, these wireless sensors need to be supplied somehow with energy to be able to function properly. The classic ways of supplying energy such as batteries have some drawbacks, they are limited in energy and must be replaced periodically, and this is not conceivable for applications where the wireless sensor is placed in hazardous places or in places where the access is impossible. So, it is necessary to find another way to permanently provide energy to these wireless sensors. The integration and miniaturization of the electronic devices has led to low power consumption systems, which opens a way to another techniques in terms of providing energy. Amongst the possibilities, we can find the Wireless Power Transfer (WPT) and Energy Harvesting (EH). In fact, the electromagnetic energy is nowadays highly available in our planet thanks to all the applications that use wireless systems. We can take advantage of this massive available quantity of energy and use it to power-up the low power wireless sensors. This thesis is incorporated within the framework of WPT and EH. Its objective is the conception and realization of electromagnetic energy harvesters called "Rectenna" in order to supply energy to low power wireless sensors. The term "rectenna" is the combination of two words: Antenna and Rectifier. The Antenna is the module that captures the electromagnetic ambient energy and converts it to a RF signal, the rectifier is the RF circuit that converts this RF signal into a continuous (DC) signal that is used to supply the wireless sensors. In this manuscript, several rectennas will be presented, for different frequencies going from the GSM frequencies (868 MHz, 915 MHz) to the Ku/Ka bands.

Les systèmes de contrôle-commande industriels (Industrial Control System, ICS) sont des infrastructures constituées par un ensemble de calculateurs industriels reliés en réseau et permettant de contrôler un système physique. Ils assurent le pilotage de réseaux électriques (Smart Grid), de systèmes de production, de transports, de santé ou encore de systèmes d’armes. Pensés avant tout pour assurer productivité et respect de la mission dans un environnement non malveillant, les ICS sont, depuis le 21ème siècle, de plus en plus vulnérables aux attaques (Stuxnet, Industroyer, Triton, …) notamment avec l’arrivée de l’industrie 4.0. De nombreuses études ont contribué à sécuriser les ICS avec des approches issues du domaine de la sécurité (cryptographie, IDS, etc…) mais qui ne tiennent pas compte du comportement du système physique et donc des conséquences de l’acte de malveillance en lui-même. Ainsi, une sécurisation se limitant exclusivement à l’analyse des informations qui transitent sur un réseau industriel n’est pas suffisante. Notre approche amène un changement de paradigme dans les mécanismes de détection en y intégrant la modélisation du comportement du système cyber-physique.Cette thèse propose des mécanismes de détection d’attaques en se positionnant au plus proche de la physique. Ils analysent les données échangées entre le système de contrôle-commande et le système physique, et filtrent les échanges au travers de modèles déterministes qui représentent le comportement du système physique soumis à des lois de commande. A cet effet, une méthodologie de conception a été proposée dans laquelle l’ensemble des ordres est identifié afin de détecter les attaques brutales. Pour faire face aux autres attaques, en particulier celles plus sournoises, comme les attaques par séquences, nous proposons une stratégie de détection complémentaire permettant d’estimer l’occurrence d’une attaque avant que ses conséquences ne soient destructives. A cet effet, nous avons développé des concepts de distance d’un état caractérisé comme critique auquel nous avons adjoint un second mécanisme dit de trajectoire dans le temps permettant de caractériser une intention de nuire.L’approche proposée hybride ainsi deux techniques orientées sécurité (sonde IDS) et sûreté (approche filtre) pour proposer une stratégie de détection basée sur quatre mécanismes lié :• A la détection de contexte : basé sur l’état courant de l’ICS, un ordre émis par l’API peut être bloqué s’il conduit vers un état critique (attaque brutale).• Aux contraintes combinatoires (attaque par séquences) : vérifiées par les concepts de distance et de trajectoire (évolution de la distance).• Aux contraintes temporelles (attaque temporelle) : vérifiées par des fenêtres temporelles sur l’apparition d’évènements et d’indicateurs surveillant la durée moyenne d’exécution.• Aux sur-sollicitations basées sur un indicateur surveillant les commandes envoyées afin de prévenir un vieillissement prématuré (attaque sur les équipements).L’approche proposée a été appliquée sur différents exemples de simulation et sur une plateforme industrielle réelle où la stratégie de détection a montré son efficacité face à différents profils d’attaquant. / Industrial Control Systems (ICSs) are infrastructures composed by several industrial devices connected to a network and used to control a physical system. They control electrical power grid (Smart Grid), production systems (e.g. chemical and manufacturing industries), transport (e.g. trains, aircrafts and autonomous vehicles), health and weapon systems. Designed to ensure productivity and respect safety in a non-malicious environment, the ICSs are, since the 21st century, increasingly vulnerable to attacks (e.g. Stuxnet, Industroyer, Triton) especially with the emergence of the industry 4.0. Several studies contributed to secure the ICS with approaches from the security field (e.g. cryptography, IDS) which do not take into account the behavior of the physical system and therefore the consequences of the malicious act. Thus, a security approach limited exclusively to the analysis of information exchanged by industrial network is not sufficient. Our approach creates a paradigm shift in detection mechanisms by integrating the behavioral modeling of the cyber-physical system.This thesis proposes detection mechanisms of attacks by locating detection closer to physical system. They analyze the data exchanged between the control system and the physical system, and filter the exchanges through deterministic models that represent the behavior of the physical system controlled by control laws. For this purpose, a design methodology has been proposed in which all actions are identified in order to instantly detect brutal attacks. To deal with other attacks, especially the more sneaky, such as sequential attacks, we propose a complementary detection strategy to estimate the occurrence of an attack before its consequences are destructive. To this end, we have developed the concepts of distance of a state identified as critical to which we have added a second mechanism called trajectory which leads to a temporal notion that characterize an intention to harm.As part of this thesis, the proposed approach combines two techniques oriented security (IDS probe) and safety (filter approach) to propose a detection strategy based on four mechanisms related to:• Context detection: based on the current state of the system, an order sent by the PLC can be blocked by the control filter if it leads to a critical state (brutal attack).• Combinatorial constraints (sequential attack): verified by the concepts of distance (risk indicator for the current state) and trajectory (indicator of the intention to harm by studying the evolution of the distance on a sequence).• Temporal constraints (temporal attack): verified by time windows on the appearance of events and an indicator monitoring the average duration of execution.• Over-solicitation monitoring mechanism: based on an indicator monitoring orders sent to the actuators to prevent premature ageing of the production equipment (attack on the equipment).The proposed approach has been applied to various simulation examples and an industrial platform where the detection strategy has shown its effectiveness against different scenarios corresponding to attacker profiles.

De nos jours, la validation des unités de contrôle électronique ECU se fonde généralement sur la simulationHardware-In-the-Loop où les systèmes physiques qui manquent sont modélisés à l’aide deséquations différentielles hybrides. La complexité croissante de ce type de modèles rend le compromisentre le temps de calcul et la précision de la simulation difficile à satisfaire. Cette thèse étudie et proposedes méthodes d’analyse et d’expérimentation destinées à la co-simulation temps-réel ferme de modèlesdynamiques hybrides. Elle vise notamment à définir des solutions afin d’exploiter plus efficacement leparallélisme fourni par les architectures multi-coeurs en utilisant de nouvelles méthodes et paradigmesde l’allocation des ressources. La première phase de la thèse a étudié la possibilité d’utiliser des méthodesd’intégration numérique permettant d’adapter l’ordre comme la taille du pas de temps ainsi quede détecter les événements et ceci dans le contexte de la co-simulation modulaire avec des contraintestemps-réel faiblement dures. De plus, l’ordre d’exécution des différents modèles a été étudié afin dedémontrer l’influence du respect des dépendances de données entre les modèles couplés sur les résultatsde la simulation. Nous avons proposé pour cet objectif, une nouvelle méthode de co-simulationqui permet le parallélisme complet entre les modèles impliquant une accélération supra-linéaire sanspour autant ajouter des erreurs liées à l’ordre d’exécution. Enfin, les erreurs de retard causées par lataille de pas de communication entre les modèles ont été améliorées grâce à une nouvelle méthoded’extrapolation par contexte des signaux d’entrée. Toutes les approches proposées visent de manièreconstructive à améliorer la vitesse de simulation afin de respecter les contraintes temps-réel, tout engardant la qualité et la précision des résultats de simulation sous contrôle. Ces méthodes ont été validéespar plusieurs essais et expériences sur un modèle de moteur à combustion interne et intégrées àun prototype du logiciel xMOD. / Nowadays the validation of Electronic Control Units ECUs generally relies on Hardware-in-The-Loopsimulation where the lacking physical systems are modeled using hybrid differential equations. Theincreasing complexity of this kind of models makes the trade-off between time efficiency and the simulationaccuracy hard to satisfy. This thesis investigates and proposes some analytical and experimentalmethods towards weakly-hard real-time co-simulation of hybrid dynamical models. It seeks in particularto define solutions in order to exploit more efficiently the parallelism provided by multi-core architecturesusing new methods and paradigms of resource allocation. The first phase of the thesis studied the possibilityof using step-size and order control numerical integration methods with events detection in thecontext of real-time modular co-simulation when the time constraints are considered weakly-hard. Moreover,the execution order of the different models was studied to show the influence of keeping or not thedata dependencies between coupled models on the simulation results. We proposed for this aim a newmethod of co-simulation that allows the full parallelism between models implying supra-linear speed-upswithout adding errors related to their execution order. Finally, the delay errors due to the communicationstep-size between the models were improved thanks to a proposed context-based inputs extrapolation.All proposed approaches target constructively to enhance the simulation speed for the compliance toreal-time constraints while keeping the quality and accuracy of simulation results under control and theyare validated through several test and experiments on an internal combustion engine model and integratedto a prototype version of the xMOD software.