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.
https://hal-mines-paristech.archives-ouvertes.fr/hal-01138327 Contributor : Olivier HermantConnect in order to contact the contributor Submitted on : Wednesday, April 1, 2015 - 4:43:06 PM Last modification on : Wednesday, November 17, 2021 - 12:31:47 PM Long-term archiving on: : Thursday, July 2, 2015 - 3:26:31 PM
Olivier Hermant, Vivien Maisonneuve. Des réels aux flottants : préservation automatique de preuves de stabilité de Lyapunov. AFADL, Pascale Le Gall; Frederic Dadeau, Jun 2015, Bordeaux, France. pp.51-56. ⟨hal-01138327⟩