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.
Liste complète des métadonnées

Littérature citée [4 références]  Voir  Masquer  Télécharger

https://hal-mines-paristech.archives-ouvertes.fr/hal-01138327
Contributeur : Olivier Hermant <>
Soumis le : mercredi 1 avril 2015 - 16:43:06
Dernière modification le : lundi 12 novembre 2018 - 10:55:01
Document(s) archivé(s) le : jeudi 2 juillet 2015 - 15:26:31

Fichiers

lyafloat.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité - Partage selon les Conditions Initiales 4.0 International License

Identifiants

  • 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⟩

Partager

Métriques

Consultations de la notice

243

Téléchargements de fichiers

107