Accéder directement au contenu Accéder directement à la navigation
Rapport

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

Abstract : In 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. 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 for Feron'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.
Liste complète des métadonnées

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

https://hal-mines-paristech.archives-ouvertes.fr/hal-00838010
Contributeur : Claire Medrala <>
Soumis le : lundi 24 juin 2013 - 15:37:29
Dernière modification le : jeudi 24 septembre 2020 - 16:36:01
Archivage à long terme le : : mercredi 5 avril 2017 - 03:41:39

Fichier

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

Identifiants

  • HAL Id : hal-00838010, version 1

Citation

Vivien Maisonneuve. Preservation of Lyapunov-Theoretic Proofs: From Real to loating-Point Numbers. 2013. ⟨hal-00838010⟩

Partager

Métriques

Consultations de la notice

368

Téléchargements de fichiers

118