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

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.The reachable set of a dynamical system is of great interest when it comes to verification of safety properties. Such set is known to be a complex geometrical object (sometimes non-convex and/or unconnected even for simple cases) and its computation is challenging. This thesis proposes three methods to overapproximate the reachable set of cyber-physical systems. The first method, the "ellipsoidal method'', studies linear systems subjects to a disturbance bounded in norm 2 or norm infty. The second method, the "interval method'', studies non-linear IQC systems by means of interval sets. In the last method, the "cosimulation method'' studies a broader family of systems (an interconnection of dynamical systems) with an abstract interpretation approach.The "ellipsoidal method'' describes the computation of reachable sets for linear time-invariant systems with an unknown input bounded by Integral Quadratic Constraints (IQC) and/or Quadratic Constraints (QC), which models e.g. delay, rate limiter, energy bounds or sector inequalities. The reachable set is overapproximated with a family of time-varying conics. Each conic's parameter is the solution to a Differential Riccati Equation (DRE). Contrary to previous work in this field, this DRE involves a time-varying free parameter that can be chosen for different purposes. We can generate the conic of minimal volume at a given time or find a conic supported by the reachable set in given directions. Our approach unifies ellipsoidal methods (for L_infty constrained disturbances) and storage function methods (classically used for IQC systems).The "interval method'' describes the use a Runge-Kutta guaranteed integration scheme to overapproximate the reachable set of non-linear IQC systems. The integral constraint is used to define a contractor over the reachable tube. This contractor and a propagation step are successively applied on a prior given overapproximation of the reahcable tube until a fixed point is reached. We evaluated our algorithm with DynIbex library to simulate a delayed system, i.e., an infinite dimensional system that can be modeled as a linear time-invariant system subject to an integral quadratic constraint. Our approach is shown to be tractable and enables the use of interval arithmetic and guaranteed integration for a richer set of dynamical systems.Finally, the "cosimulation method'' merges the two previous methods into a unique one that can study a broader family of systems : an interconnection of system. Each system in the interconnection is considered as an operator in a signal space (continuous-/discrete-time) and the proposed method is formalized within the abstract interpretation framework. System's reachable tube is expressed as the solution of a fixed point equation. This reachable set is overapproximated in the abstract domain with time-varying sets (e.g. time-varying intervals or ellipsoidal sets) and computed by solving a least fixed point equation. We apply the cosimulation method to overapproximate the reachable tube of several non-linear systems subject to IQC-bounded disturbances