Le filtrage numérique est couramment utilisé dans les systèmes temps réels embarqués (par exemple dans l'automobile, l'aéronautique ou l'aérospatiale). Il permet de modéliser au niveau logiciel des comportements (comme la recherche d'équilibre) qui étaient autrefois assurés par des filtres mécaniques (hydrauliques par exemple), puis par des filtres analogiques. Cependant, la modélisation de ces filtres au niveau logiciel peut poser des problèmes, comme par exemple la stabilité du flux de sortie en présence d'arrondis. Notre but est alors de prouver l'absence d'erreurs à l'exécution (essentiellement des débordements de nombres à virgule flottante) dans un programme comprenant du filtrage numérique.
Nous utilisons l'interprétation abstraite pour construire des domaines adaptés au filtrage. Nous pouvons ainsi raffiner des analyses existantes pour tenir compte de ces filtres. Nous associons à chaque famille de filtres, un domaine abstrait. Ce domaine est essentiellement une boîte noire, qui associe à l'approximation du flux d'entrée du filtre une approximation du flux de sortie. Le domaine se charge alors de repérer toutes les instances des filtres de cette famille, et d'utiliser les contraintes que l'analyseur a découvert sur les entrées, pour inférer les contraintes sur les sorties de ces filtres.
Cette méthodologie a été entièrement incorporé à ASTRÉE (analyseur statique de logiciels temps-réel embarqués). Elle fait l'objet d'un papier à paraître dans ESOP'04.