Analyse statique de systèmes de contrôle commande : synthèse d'invariants non linéaires (Static Analysis of Control Command Systems : Synthesizing non Linear Invariants) Roux, Pierre 2013-12-18 Institut Supérieur de l'Aéronautique et de l'Espace

Directeur(s) de thèse:  Wiels, Virginie; Garoche, Pierre-Loïc Laboratoire :  Département Traitement de l’Information et Modélisation -DTIM (depuis 1997) Ecole doctorale :  Mathématiques, Informatique et Télécommunications de Toulouse -MITT Classification : Informatique

Accès :  Texte intégral Mots-clés : Interprétation abstraite, Systèmes de contrôle-commande, Invariants quadratiques, Itération sur les stratégies, Ellipsoïdes, Programmation semi-définie Résumé : Les systèmes critiques comme les commandes de vol peuvent entraîner des désastres en cas de dysfonctionnement. D'où l'intérêt porté à la fois par le monde industriel et académique aux méthodes de preuve formelle capable d'apporter, plus ou moins automatiquement, une preuve mathématique de correction. Parmi elles, cette thèse s'intéresse particulièrement à l'interprétation abstraite, une méthode efficace pour générer automatiquement des preuves de propriétés numériques qui sont essentielles dans notre contexte. Il est bien connu des automaticiens que les contrôleurs linéaires sont stables si et seulement si ils admettent un invariant quadratique (un ellipsoïde, d'un point de vue géométrique). Ils les appellent fonction de Lyapunov quadratique et une première partie propose d'en calculer automatiquement pour des contrôleurs donnés comme paire de matrices. Ceci est réalisé en utilisant des outils de programmation semi-définie. Les aspects virgule flottante sont pris en compte, que ce soit dans les calculs effectués par le programme analysé ou dans les outils utilisés pour l'analyse. Toutefois, le véritable but est d'analyser des programmes implémentant des contrôleurs (et non des paires de matrices), incluant éventuellement des réinitialisation ou des saturations, donc non purement linéaires. L'itération sur les stratégies est une technique d'analyse statique récemment développée et bien adaptée à nos besoins. Toutefois, elle ne se marrie pas facilement avec les techniques classiques d'interprétation abstraite. La partie suivante propose une interface entre les deux mondes. Enfin, la dernière partie est un travail plus préliminaire sur l'usage de l'optimisation globale sur des polynômes basée sur les polynômes de Bernstein pour calculer des invariants polynomiaux sur des programmes polynomiaux. Résumé (anglais) : Critical Systems such as flight commands may have disastrous results in case of failure. Hence the interest of both the industrial and the academic communities in formal methods able to more or less automatically deliver mathematical proof of correctness. Among them, this thesis will particularly focus on abstract interpretation, an efficient method to automatically generate proofs of numerical properties which are essential in our context. It is well known from control theorists that linear controllers are stable if and only if they admit a quadratic invariant (geometrically speaking, an ellipsoid). They call these invariants quadratic Lyapunov functions and a first part offers to automatically compute such invariants for controllers given as a pair of matrices. This is done using semi-definite programming optimization tools. It is worth noting that floating point aspects are taken care of, whether they affect computations performed by the analyzed program or by the tools used for the analysis. However, the actual goal is to analyze programs implementing controllers (and not pairs of matrices), potentially including resets or saturations, hence not purely linears. The policy iteration technique is a recently developed static analysis techniques well suited to that purpose. However, it does not marry very easily with the classic abstract interpretation paradigm. The next part tries to offer a nice interface between the two worlds. Finally, the last part is a more prospective work on the use of polynomial global optimization based on Bernstein polynomials to compute polynomial invariants on polynomials systems. Langue : Anglais

Exporter au format XML