Vérification et synthèse des systèmes hybrides

Les systèmes hybrides sont des systèmes qui combinent des dynamiques discrètes et continues. Cette thèse propose des techniques algorithmiques de vérification et de synthèse pour ces systèmes Le manque de méthodes pour calculer les ensembles atteignables des dynamiques continues est l'obstacle principal vers une méthodologie algorithmique de vérification. Nous développons deux techniques d'atteignabilité approximatives pour les systèmes continus basées sur une méthode efficace pour représenter des ensembles et une combinaison des techniques de la simulation, de la géométrie algorithmique, de l'optimisation, et de la commande optimale. La première technique d'atteignabilité est spécialisée pour les systèmes linéaires et étendue aux systèmes avec entrée incertaine, et la seconde peut être appliquée aux systèmes non-linéaires. En appliquant ces techniques nous développons un algorithme de vérification des propriétés de sûreté pour une large classe des systèmes hybrides avec des dynamiques continues arbitraires et des dynamiques discrètes assez générales. Nous étudions ensuite le problème de la synthèse de contrôleurs de sûreté pour les systèmes hybrides. Nous présentons un algorithme de synthèse des contrôleurs par commutation basé sur le calcul de l'ensemble d'invariance maximal et les techniques d'analyse d'atteignabilité. Nous avons implanté les algorithmes développés dans un outil appelé "d/dt", qui permet la vérification et la synthèse automatique pour les systèmes hybrides avec des inclusions différentielles linéaires. En dehors de nombreux exemples académiques, nous avons appliqué avec succès l'outil pour analyser quelques systèmes pratiquesGRENOBLE1-BU Sciences (384212103) / SudocGRENOBLE-MI2S (384212302) / SudocSudocFranceF