Génération de codes et d'annotations prouvables d'algorithmes de points intérieurs à destination de systèmes embarqués critiques

The objective of this thesis is to contribute to the formal verification of such systems. We will focus in particular on the certification of the compilation of the model to the code. In particular, through the annotation generation at the core of the code from the properties of the model. In the case of synchronous languages, the transition from a synchronous paradigm to a imperative paradigm will be a fundamental step. As regards the properties properly they may be of several forms, mainly logical, whole or real, requiring each of the different methods of proof. It will be necessary to generate these properties at the level of code, but then to ensure that they are provable (on condition that it was at the model level). To do this we can start from an existing compiler and complete it with a module of annotation generation. The target being a priori the C, one can use the language ACSL to write the annotations and then Frama-C to check them.L’aéronautique a vu émerger ces dernières années l’utilisation d’optimisation convexe au sein de ses systèmes critiques. Les avantages apportés par l’optimisation peuvent aller de la réduction de la consommation de fioul à de nouvelles techniques de contrôle. Par exemple, l’atterrissage de fusée comme pratiqué par SpaceX se base sur la résolution en ligne de problème d’optimisation convexe grâce à des algorithmes de point intérieur. Toutefois, ceux-ci sont couteux en temps de calcul, mais la puissance grandissante des systèmes informatiques permet, désormais, leur utilisation en ligne. De plus, afin de réduire les temps de calcul au maximum, les industriels choisissent de développer des implémentations spécifiques aux problèmes à résoudre. L’optimisation reste cependant aujourd’hui limitée à des calculs secondaires, ou à des systèmes peu critiques. Pour généraliser leur utilisation, au sein de systèmes grand public, les industriels devront pouvoir certifier les implémentations de ces algorithmes. Cela consiste à vérifier :1. l’absence d’erreur à l’exécution,2. qu’elles répondent en temps fini, idéalement borné,3. la correction de la solution retournée.Dans le cas de l’optimisation, ce dernier point correspond à vérifier que la solution respecte les contraintes et est optimale. Ce travail a consisté à développer des outils et des méthodes qui permettent de certifier formellement un code généré d’algorithme de point intérieur. Pour cela, nous avons utilisé des méthodes et outils issus de la vérification formelle de programmes afin de générer un code embarquable, mais aussi prouvable à partir de la donnée d’un problème d’optimisation convexe.Les principales contributions apportées par ce manuscrit sont :1. La création d’un langage, pySil, qui permet d’exprimer simplement des algorithmes numériques matriciels, ainsi que leurs spécifications.2. L’écriture, en pySil, d’un algorithme de point intérieur.3. Le développement d’un compilateur de pySil vers le langage C/ACSL afin d’obtenir un code à la fois exécutable en ligne, mais aussi prouvable par Frama-C.4. L’enrichissement de la spécification de l’algorithme écrit en pySil afin que Frama-C puisse prouver la correction de sa compilation en C/ACSL. L’approche a pu être évaluée sur des exemples, en particulier de commande prédictive.D’autre part, nous avons mené ce travail avec le souci d’expliciter clairement et réduire au maximum les logiciels et hypothèses sur lesquels repose la preuve de correction