Analyse statique de contrôleurs à base d'optimisation convexe

This manuscript presents a set of works targeting the formal analysis of controller software implementation using the tools of convex optimization.Les travaux présentés portent, d’une façon générale, sur la preuve automatique de propriétés de systèmes de contrôle-commande à l’aide d’optimisation convexe. Par exemple, pour montrer qu’un système ne va jamais se mettre dans un état indésirable, on va démontrer qu’une certaine propriété, dite invariant inductif, excluant les états indésirables, est vraie à toute étape de calcul par récurrence sur le nombre d’étapes. Ce sont des paramètres numériques de cette propriété qui sont obtenus par optimisation convexe. Les systèmes étudiés peuvent être présentéssoit comme des modèles de haut niveau, soit comme des logiciels ; dans ce dernier cas, leur utilisation de nombres en virgule flottante, par opposition à des réels, est prise en compte. Parmi les systèmes de contrôle-commande susceptibles d’être étudiés à l’aide des approches présentées dans le mémoire on trouve notamment ceux de l’avionique, où l’on exige non seulement un haut niveau de sûreté, mais aussi des arguments forts démontrant le bon fonctionnement du système