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

Abstract : In a paper, Feron presents how Lyapunov-theoretic proofs of stability can be migrated toward computer-readable and verifiable certificates of control software behavior by relying of Floyd's and Hoare's proof system. However, Lyapunov-theoretic 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 preserving those proofs in presence of rounding errors resulting from the use of floating-point arithmetic: we present an automatic tool, based on a theoretical framework the soundness of which is proved in Coq, that translates Feron's proof invariants on real arithmetic to similar invariants on floating-point numbers, and preserves the proof structure. We show how our methodology allows to verify whether stability invariants still hold for the concrete implementation of the controller. We study in details the application of our tool to the open-loop system of Feron's paper and show that stability is preserved out of the box. We also translate Feron's proof for the closed-loop system, and discuss the conditions under which the system remains stable.
Liste complète des métadonnées

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

https://hal-mines-paristech.archives-ouvertes.fr/hal-01086732
Contributeur : Claire Medrala <>
Soumis le : lundi 24 novembre 2014 - 17:13:45
Dernière modification le : lundi 12 novembre 2018 - 10:56:29
Document(s) archivé(s) le : mercredi 25 février 2015 - 11:30:31

Fichier

A-556.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01086732, version 1

Citation

Vivien Maisonneuve, Olivier Hermant, François Irigoin. Preservation of Lyapunov-Theoretic Proofs: From Real to Floating-Point Arithmetic. [Research Report] Mines ParisTech. 2014. ⟨hal-01086732⟩

Partager

Métriques

Consultations de la notice

322

Téléchargements de fichiers

138