Preservation of Lyapunov-Theoretic Proofs: From Real to Floating-Point Numbers - Archive ouverte HAL Accéder directement au contenu
Rapport (Rapport De Recherche) Année : 2013

Preservation of Lyapunov-Theoretic Proofs: From Real to Floating-Point Numbers

(1)
1
Vivien Maisonneuve
  • Fonction : Auteur
  • PersonId : 942462

Résumé

In Feron presents how Lyapunov-theoretic proofs of stability can be migrated toward computerreadable and verifiable certificates of control software behavior by relying of Floyd’s and Hoare’s proof system.However, Feron’s proofs are addressed towards exact, real arithmetic and do not accurately represent the behavior of realistic programs run with machine arithmetic. We address the issue of errors resulting from the use of floating-point arithmetic: we present an approach to translate Feron’s proof invariants on real arithmetic to similar invariants on floating-point numbers and show how our methodology applies to prove stability, thus allowing to verify whether the stability invariant still holds when the controller is implemented.We study in details the open-loop system of Feron’s paper. We also use the same approach forFeron’s closed-loop system, but the constraints are too tights to show stability in this second case:more leeway should be introduced in the proof on real numbers, otherwise the resulting system might be unstable.
Fichier principal
Vignette du fichier
A-528-lyafloat.pdf (498.84 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01086727 , version 1 (24-11-2014)

Identifiants

  • HAL Id : hal-01086727 , version 1

Citer

Vivien Maisonneuve. Preservation of Lyapunov-Theoretic Proofs: From Real to Floating-Point Numbers. [Research Report] Mines ParisTech. 2013. ⟨hal-01086727⟩
107 Consultations
42 Téléchargements

Partager

Gmail Facebook Twitter LinkedIn More