Formalisation en Coq des algorithmes de filtre numérique calculés en précision finie ; Coq formalization of digital filter algorithms computed using finite precision arithmetic
Titel:
Formalisation en Coq des algorithmes de filtre numérique calculés en précision finie ; Coq formalization of digital filter algorithms computed using finite precision arithmetic
Anmerkungen:
Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
Beschreibung:
Les filtres numériques sont utilisés dans de nombreux domaines, des télécommunications à l'aérospatiale. En pratique, ces filtres sont calculés sur machine en précision finie (virgule flottante ou virgule fixe). Les erreurs d'arrondi résultantes peuvent être particulièrement problématiques dans les systèmes embarqués. En effet, de fortes contraintes énergétiques et spatiales peuvent amener à privilégier l'efficacité des calculs, souvent au détriment de leur précision. De plus, les algorithmes de filtres enchaînent de nombreux calculs, au cours desquels les erreurs d'arrondi se propagent et risquent de s'accumuler. Comme certains domaines d'application sont critiques, j'analyse les erreurs d'arrondi dans les algorithmes de filtre en utilisant l'assistant de preuve Coq. Il s'agit d'un logiciel qui garantit formellement que cette analyse est correcte. Un premier objectif est d'obtenir des bornes certifiées sur la différence entre les valeurs produites par un filtre implémenté (calculé en précision finie) et par le filtre modèle initial (défini par des calculs théoriques exacts). Un second objectif est de garantir l'absence de comportement catastrophique comme un dépassement de capacité supérieur imprévu. Je définis en Coq les filtres numériques linéaires invariants dans le temps (LTI), considérés dans le domaine temporel. Je formalise une forme universelle appelée la SIF, à laquelle on peut ramener n'importe quel algorithme de filtre LTI sans modifier ses propriétés numériques. Je prouve ensuite le théorème des filtres d'erreurs et le théorème du Worst-Case Peak Gain, qui sont deux théorèmes essentiels à l'analyse numérique d'un filtre sous forme de SIF. Par ailleurs, cette analyse dépend aussi de l'algorithme de somme de produits utilisé dans l'implémentation. Je formalise donc plusieurs algorithmes de somme de produits offrant différents compromis entre précision du résultat et vitesse de calcul, dont un algorithme original correctement arrondi au plus proche. Je définis également en Coq les dépassements de ...