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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
IEEE Standard for Binary Floating-Point Arithmetic, p. 754. IEEE, Los Alamitos
Bomar, B.W., et al.: Roundoff noise analysis of state-space digital filters implemented on floating-point digital signal processors. IEEE Trans. on Circuits and Systems II 44(11), 952–955 (1997)
Cousot, P., et al.: The ASTRÉE analyzer. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 21–30. Springer, Heidelberg (2005)
Feret, J.: Static analysis of digital filters. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 33–48. Springer, Heidelberg (2004)
Free Software Foundation. GSL — GNU scientific library (2004)
Jackson, L.B.: On the interaction of roundoff noise and dynamic range in digital filters. The Bell System Technical J. 49(2), 159–184 (1970)
Jackson, L.B.: Digital Filters and Signal Processing. Kluwer, Dordrecht (1989)
Lamb, A.A., Thies, W., Amarasinghe, S.: Linear analysis and optimization of stream programs. In: PLDI 2003, pp. 12–25. ACM, New York (2003)
Miné, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 3–17. Springer, Heidelberg (2004)
Rao, B.D.: Floating point arithmetic and digital filters. IEEE Trans. on Signal Processing 40(1), 85–95 (1992)
Roozbehani, M., Feron, E., Megretski, A.: Modeling, optimization and computation for software verification. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, p. 606. Springer, Heidelberg (2005)
Rump, S.M.: Ten methods to bound multiple roots of polynomials. J. of Computational and Applied Math. 156(2), 403–432 (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Monniaux, D. (2005). Compositional Analysis of Floating-Point Linear Numerical Filters. In: Etessami, K., Rajamani, S.K. (eds) Computer Aided Verification. CAV 2005. Lecture Notes in Computer Science, vol 3576. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11513988_21
Download citation
DOI: https://doi.org/10.1007/11513988_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27231-1
Online ISBN: 978-3-540-31686-2
eBook Packages: Computer ScienceComputer Science (R0)