Skip to Main content Skip to Navigation
Conference papers

Formalisation en Coq d'algorithmes de filtres numériques

Résumé : Les algorithmes de filtres numériques sont un outil essentiel du traitement du signal et du contrôle-commande. Ils sont utilisés dans de nombreux domaines comme les télécommunications, l'automobile, la robotique, l'aéronautique etc. Comme certains de ces domaines sont critiques , nous souhaitons garantir formellement qu'ils se comportent bien numériquement malgré les erreurs d'arrondi inhérentes à leur implémen-tation en précision finie. Or il existe de nombreux algorithmes pour calculer un filtre numérique, que l'on appelle réalisations. En précision finie, des réalisations légèrement différentes, par exemple où seulement l'ordre des calculs est modifié, peuvent donner des résultats différents. La SIF (Specialized Implicit Form) est un formalisme très général, qui peut représenter toutes les réalisations en détaillant jusqu'à l'ordre des calculs. Cet article étend la formalisation en Coq des filtres numériques présentée dans [1] : il y ajoute la définition de la SIF, les traductions des réalisations de cette formalisation vers la SIF, et le théorème du filtre d'erreur associé à une SIF, qui décrit la propagation des erreurs de calcul au fil des itérations dans l'algorithme correspondant.
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/hal-01929531
Contributor : Diane Gallois-Wong <>
Submitted on : Tuesday, December 11, 2018 - 10:03:05 AM
Last modification on : Friday, April 30, 2021 - 9:55:18 AM

File

JFLA19-coq-filtres-num.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01929531, version 2

Citation

Diane Gallois-Wong. Formalisation en Coq d'algorithmes de filtres numériques. JFLA 2019 - Journées Francophones des Langages Applicatifs, Nicolas Magaud, Jan 2019, Les Rousses, France. ⟨hal-01929531v2⟩

Share

Metrics

Record views

157

Files downloads

516