From Reals to Floating-Point Numbers: Automatic Preservation of Lyapunov Stability Proofs - Archive ouverte HAL Accéder directement au contenu
Communication Dans Un Congrès Année :

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

(1) , (1)
1
Olivier Hermant
Vivien Maisonneuve
  • Fonction : Auteur
  • PersonId : 773689
  • IdRef : 185718418

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.
Fichier principal
Vignette du fichier
lyafloat.pdf (251.71 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01138327 , version 1 (01-04-2015)

Licence

Paternité - Partage selon les Conditions Initiales - CC BY 4.0

Identifiants

  • HAL Id : hal-01138327 , version 1

Citer

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⟩
178 Consultations
78 Téléchargements

Partager

Gmail Facebook Twitter LinkedIn More