Un Système Contrôlé en Réseau (SCR en français, NCS (Networked Control System) en anglais) est un système de contrôle/commande distribué dans lequel les informations sont échangées en temps réel via un réseau reliant capteurs, actionneurs, contrôleurs, …) Ces SCR sont présents dans de nombreuses applications industrielles tels que les systèmes de production, les systèmes contrôlés à distance, les véhicules autonomes, la téléopération, …. Les principaux avantages de ces systèmes sont la flexibilité de leur architecture et la réduction des coûts d'installation et de maintenance, le principal inconvénient est les effets dus au réseau tels que les retards de transmission, qui influencent les performances et la stabilité de la boucle de régulation, ces systèmes sont également vulnérables aux cyber – attaques.Cette thèse apporte quelques contributions sur la détection des cyber attaques ainsi que le développement d'un contrôleur capable de traiter les effets des retards temporels.Pour atteindre cet objectif, la méthode proposée est d'adapter une commande sans modèle et d'améliorer son utilisation dans les Systèmes Contrôlés en Réseau. L'idée principale est basée sur le bénéfice mutuel d'un prédicteur de Smith et du modèle de base de la commande sans modèle. Ensuite, la structure intelligente de la commande sans modèle est appliquée avec une commande prédictive généralisée (GPC Generalized Predictive Control) de manière à obtenir une commande prédictive généralisée intelligente, qui est une amélioration du contrôleur généralisé standard. Ce contrôleur est conçu selon deux méthodes différentes pour détecter les cyber attaques.Parallèlement, un nouveau mécanisme de sécurité basé sur une réponse trompeuse pour les cyber attaques dans les Systèmes Contrôlés en Réseau est proposé. Le mécanisme proposé peut permettre d'arrêter une cyber-attaque en apportant une dernière ligne de défense lorsque l'attaquant a un accès à l'installation distante.Enfin, deux détecteurs d'attaque de piratage de commande sont introduits. L'objectif est de pouvoir détecter une attaque tel que le cas Stuxnet où le contrôleur a été détourné par reprogrammation. L'avantage des détecteurs proposés est qu'il ne nécessite pas d'avoir a priori un modèle mathématique du contrôleur. / A networked control system (NCS) is a control system in which the control loop is closed over a real-time network. NCSs are used in many industrial applications, and also in applications such as remote control, unmanned aerial vehicles or surgical teleoperation, ... The major advantages of NCS are a flexible architecture and a reduction of installation and maintenance costs, the main disadvantage of NCS is the network effects, such as time-delays, that influence the performance and stability of the control loop. These systems are also vulnerable to cyber attacks.This thesis makes some contributions regarding the detection of cyber-physical attacks as well as the development of a controller which capable of dealing with the other the bad effects of the network like time-delays.To achieve this goal, the proposed approach is to adapt model-free controller and to improve its use in NCS. The main idea is based on mutual benefit between Smith predictor and the basic model-free controller. Then, the intelligent structure of model-free control is applied along with Generalized Predictive Controller (GPC) to achieve the Intelligent Generalized Predictive Controller (IGPC) as an enhancement for the standard GPC. The IGPC is designed along with two different methods for cyber-attack detection.Moreover, a new security mechanism based on the deception for the cyber-physical attacks in NCS is proposed, this mechanism can allow to stop the cyber-attacks by providing the last line of defense when the attacker has an access to the remote plant.Finally, two detectors for controller hijacking attack are introduced. The objective is to be able to detect an attack such as the Stuxnet case where the controller has been reprogrammed and hijacked. The advantage of these proposed detectors is that there is not necessary to have a priori mathematical model of the controller.

La vérification à l'exécution est une technique prometteuse pour améliorer la sûreté des systèmes complexes. Ces systèmes peuvent être instrumentés afin qu'ils produisent des traces d'exécution permettant d'observer leur utilisation dans des conditions réelles. Un défi important est de fournir aux ingénieurs logiciel un langage formel simple adapté à l'expression des exigences les plus importantes. Dans cette thèse, nous nous intéressons à la vérification de dispositifs médicaux. Nous avons effectué l'analyse approfondie d'un dispositif médical utilisé mondialement afin d'identifier les exigences les plus importantes, ainsi que la nature précise des traces d'exécution qu'il produit. À partir de cette analyse, nous proposons ParTraP, un langage défini formellement et dédié à la spécification de propriétés sur des traces finies. Il a été conçu pour être accessible à des ingénieurs logiciels non qualifiés en méthodes formelles grâce à sa simplicité et son style déclaratif. Le langage étend les patrons de spécification initialement proposé par Dwyer et. al. avec des opérateurs paramétriques et temps-réel, des portées emboîtable, et des quantificateurs de premier ordre. Nous proposons également une technique de mesure de couverture pour ParTraP, et que le niveau de couverture d'une propriété temporelle permet de mieux la comprendre, ainsi que le jeu de traces sur lequel elle est évaluée. Finalement, nous décrivons l'implémentation d'un environnement de développement intégré pour ParTraP, qui est disponible sous une licence libre. / Runtime verification is a promising technique to improve the safety of complex systems. These systems can be instrumented to produce execution traces enabling us to observe their usage in the field. A significant challenge is to provide software engineers with a simple formal language adapted to the expression of their most important requirements. In this thesis, we focus on the verification of medical devices. We performed a thorough analysis of a worldwide-used medical device in order to identify those requirements, as well as the precise nature of its execution traces. In the light of this study, we propose ParTraP, a formally defined language dedicated to property specification for finite traces. It is designed to be accessible to software engineers with no training in formal methods thanks to its simplicity and declarative style. The language extends the specification patterns originally proposed by Dwyer et al. with parametrized constructs, nested scopes, real-time and first-order quantification. We also propose a coverage measurement technique for ParTraP, and we show that coverage information provides insights on a corpus of traces as well as a deeper understanding of temporal properties. Finally, we describe the implementation of an Integrated Development Environment for ParTraP, which is available under a free and open-source license.