en fr

From Reals to Floating-Point Numbers: Automatic Preservation of Lyapunov Stability Proofs

Des réels aux flottants : préservation automatique de preuves de stabilité de Lyapunov

Résumé : Les programmes contrôle-commande doivent assurer la stabilité d'un syst eme dynamique autour d'un point d'´ equilibre. De tels programmes sont généralement issus d'une modélisation du syst eme, en partie intégrée au programme, qui calcule alors a chaque cycle la commande adéquatè a envoyer au syst eme. Les concepteurs de tels syst emes s'appuient sur la théorie de Lyapunov pour déterminer les param etres internes nécessaires a la stabilité. Il s'agit donc d'un cas rare, o` u l'on dispose en amont d'une preuve que le syst eme respecte la propriété voulue. Nous nous intéressons auprobì eme du transfert de ces preuves de la modélisation vers l' implémentation, et plusparticulì erement auprobì eme du passage des nombres réels , utilisés pour la modélisation , aux nombres flottants, qui sont utilisés dans l'implantation du programme sur micro-contrôleur. Pour cela, nous introduisons l'outil LyaFloat, qui permet de vérifier a quelles conditions de précision une preuve de stabilité, donnée en tant qu'annotation dans une logique de Hoare, est préservée ou non lors du passage aux flottants.