Applying the Z-transform for the static analysis of floating-point numerical filters

TL;DR

This paper introduces a Z-transform-based method for static analysis of digital linear filters, providing sound bounds for fixed-point and floating-point implementations in safety-critical applications.

Contribution

It presents a novel compositional abstraction technique using the Z-transform to accurately bound filter variables in floating-point digital filters.

Findings

Provides sound bounds for floating-point filters

Applicable to safety-critical digital filter implementations

Enhances static analysis precision for digital filters

Abstract

Digital linear filters are used in a variety of applications (sound treatment, control/command, etc.), implemented in software, in hardware, or a combination thereof. For safety-critical applications, it is necessary to bound all variables and outputs of all filters. We give a compositional, effective abstraction for digital linear filters expressed as block diagrams, yielding sound, precise bounds for fixed-point or floating-point implementations of the filters.