Modélisation et simulation qualitative de systèmes hybrides

Hybrid systems are at the core of cyber-physical systems. Such systems represent the interaction between continuous physical processes generally modelling the environment with discrete decisions from control electronic signaling. The verification of these systems is crucial to ensure safety at the modeling stage. The application of hybrid systems is present in many fields such as transportation, biology and avionics. The thesis studies principals from the qualitative reasoning domain and applies them to the verification of hybrid systems. The accomplished work elaborates methods to abstract a hybrid system using qualitative principles. These methods consist in discretizing the state space to a finite number of states while conserving qualitative characteristics. The computed abstraction allows to prove properties at the level of the concrete hybrid system and presents a representation of the global behavior of the system. A tool developed in C++ computes the abstraction of a given hybrid system. An evaluation of its performance is performed. We are also interested in a particular property called diagnosability. The system is said to be diagnosable when it is capable to identify modeled faults using limited specified observations. A method that uses the computed abstraction to verify diagnosability of a given hybrid system is proposed.Les systèmes hybrides sont au cœur des systèmes cyber-physiques. De tels systèmes représentent l’interaction de processus physiques continus modélisant généralement l'environnement avec des décisions discrètes issues d'un système de contrôle commande électronique. La vérification de ces systèmes est cruciale pour assurer leur sûreté dès la phase de modélisation. Les recherches sur les systèmes hybrides ont de nombreux domaines d’application, notamment le transport, l’aéronautique et la biologie. La thèse étudie des principes du raisonnement qualitatif et les applique à la vérification des systèmes hybrides. Le travail consiste à élaborer une méthode pour abstraire le système hybride en utilisant des principes qualitatifs. On recourt à une discrétisation finie de l'espace d'état tout en conservant des caractéristiques qualitatives du système. L'abstraction calculée permet de prouver des propriétés au niveau du système hybride concret et fournit une représentation du comportement global du système. Un outil développé en C++ permet de calculer l'abstraction d'un système hybride donné. Une évaluation de ses performances est établie. On s'intéresse particulièrement à une propriété de sûreté des systèmes appelée diagnosticabilité. Un modèle de système est dit diagnosticable s'il permet d'identifier sans ambiguïté la survenue de toute faute modélisée à partir des seules observations disponibles du système jusqu’à un certain délai après l’occurrence de la faute. Une méthode qui consiste à utiliser l'abstraction établie précédemment pour vérifier la diagnosticabilité d'un système hybride est proposée