Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata

Cited literature [4 references]  Display  Hide  Download

https://hal-mines-paristech.archives-ouvertes.fr/hal-01138327
Contributor : Olivier Hermant <>
Submitted on : Wednesday, April 1, 2015 - 4:43:06 PM
Last modification on : Thursday, September 24, 2020 - 4:36:02 PM
Long-term archiving on: : Thursday, July 2, 2015 - 3:26:31 PM

Files

lyafloat.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution - ShareAlike 4.0 International License

Identifiers

  • HAL Id : hal-01138327, version 1

Citation

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⟩

Share

Metrics

Record views

293

Files downloads

122