A Coq formalization of digital filters

Diane Gallois-Wong 1, 2 Sylvie Boldo 2 Thibault Hilaire 3, 2
2 TOCCATA - Certified Programs, Certified Tools, Certified Floating-Point Computations
LRI - Laboratoire de Recherche en Informatique, UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR8623
3 PEQUAN - Performance et Qualité des Algorithmes Numériques
LIP6 - Laboratoire d'Informatique de Paris 6
Abstract : Digital filters are small iterative algorithms, used as basic bricks in signal processing (filters) and control theory (controllers). They receive as input a stream of values, and output another stream of values, computed from their internal state and from the previous inputs. These systems can be found in communication, aeronautics, automotive, robotics, etc. As the application domain may be critical, we aim at providing a formal guarantee of the good behavior of these algorithms in time-domain. In particular, we formally proved in Coq some error analysis theorems about digital filters, namely the Worst-Case Peak Gain theorem and the existence of a filter characterizing the difference between the exact filter and the implemented one. Moreover, the digital signal processing literature provides us with many equivalent algorithms, called realizations. We formally defined and proved the equivalence of several realizations (Direct Forms and State-Space).
Type de document :
Communication dans un congrès
The 11th Conference on Intelligent Computer Mathematics, Aug 2018, Hagenberg, Austria. 〈https://www.cicm-conference.org/2018/cicm.php〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01728828
Contributeur : Sylvie Boldo <>
Soumis le : lundi 12 mars 2018 - 09:57:04
Dernière modification le : jeudi 14 juin 2018 - 17:17:03
Document(s) archivé(s) le : mercredi 13 juin 2018 - 12:56:41

Fichier

ITP18.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01728828, version 1

Citation

Diane Gallois-Wong, Sylvie Boldo, Thibault Hilaire. A Coq formalization of digital filters. The 11th Conference on Intelligent Computer Mathematics, Aug 2018, Hagenberg, Austria. 〈https://www.cicm-conference.org/2018/cicm.php〉. 〈hal-01728828〉

Partager

Métriques

Consultations de la notice

158

Téléchargements de fichiers

108