A set-based cosimulation method to overapproximate the reachable set of an interconnection of dynamical systems

Cosimulation ensembliste d'une interconnexion de systèmes L'ensemble d'atteignabilité d'un système embarqué est central dans la vérification de propriété de sureté. Cet ensemble géométrique est en général complexe à décrire (il peut être non convexe et/ou non connecté même dans des cas simples) et complexe à calculer. Cette thèse propose trois méthodes pour surapproximer cet ensemble. La première méthode, la "méthode ellipsoïdale'', surapproxime avec des coniques l'ensemble d'atteignabilité d'un système linéaire sujet à des perturbations bornées par des inégalités en norme 2 ou en norme inf. La seconde méthode, la "méthode des intervalles'', surapproxime avec des intervales l'ensemble d'atteignabilité d'un système non linéaire sujet à des perturbations bornées par une inégalité de norme 2. La dernière méthode, la "méthode de cosimulation'', formalise par une approche interprétation abstraite la surapproximation de l'ensemble d'atteignabilité d'une interconnexion de systèmes.La "méthode ellipsoidale'' s'intéresse à des systèmes linéaires variant dans le temps sujet à des perturbations bornées par des inégalités norme 2 (Contrainte Intgrale Quadratique -IQC-) ou norme inf (Contrainte Quadratique -QC-). Ces modèles permettent de modéliser des systèmes à délais, des systèmes soumis à des perturbations de croissance bornée (rate-limiters systems), the contraintes énergétiques, ou des inégalités sectorielles. L'ensemble d'atteignabilité est surapproximé avec des coniques variant dans le temps. Le coefficient de ces coniques est solution d'une Équation Différentielle de Riccati (DRE). Contrairement aux travaux existants, cette DRE est dépendante d'un paramètre (libre) variant dans le temps. Chaque choix de paramètres génère une surapproximation différente. Ce paramètre peut-être choisit pour satisfaire différents critères : par exemple, pour obtenir la surapproximation de volume minimal, ou bien pour obtenir une surapproximation qui "touche'' l'ensemble d'atteignabilité.La "méthode des intervalles'' applique une méthode d'intégration guaranties basée sur l'arithmétique des intervalles à la surapproximation de l'ensemble d'atteignabilité d'un système IQC non-linéaire.La contrainte intégrale est utilisée pour définir un contracteur. Le contracteur et l'opérateur de propagation (qui propage un ensemble d'états le long du flux du système) sont successivement appliqué sur une surapproximation (a priori) du reachable tube jusqu'à ce qu'un point fixe soit atteint. L'algorithme a été intégré dans le framework DynIbex pour simuler des systèmes de dimension infinie (système à délais).Enfin, la "méthode de cosimulation'' associe les deux méthodes précédentes dans une approche générique permettant ainsi l'analyse d'une classe plus large de systèmes : une interconnexion de systèmes. Chaque système dans l'interconnexion est considéré comme un opérateur sur un espace de signals (en temps continu ou discret) et l'interconnexion de systèmes est exprimée à l'aide de compositions et des point-fixes de ces opérateurs. Le formalisme de l'interprétation abstraite est ensuite utilisé pour représenter des abstractions correctes de ces signaux. Nous détaillons plusieurs domaines abstraits permettant de représenter des ensembles de trajectoires et les appliquons à des exemples-jouets.