Applying the Z-transform for the static analysis of floating-point numerical filters
作者： David Monniaux
DOI:
关键词:
摘要: Digital linear filters are used in a variety of applications (sound treatment, control/command, etc.), implemented software, hardware, or combination thereof. For safety-critical applications, it is necessary to bound all variables and outputs filters. We give compositional, effective abstraction for digital expressed as block diagrams, yielding sound, precise bounds fixed-point floating-point implementations the
arxiv.org
harvard.edu
archives-ouvertes.fr参考文章(15)
Leland B. Jackson, Digital filters and signal processing ,(1985)
David Monniaux, Optimal abstraction on real-valued programs static analysis symposium. pp. 104- 120 ,(2007) , 10.1007/978-3-540-74061-2_7
Jérôme Feret, Static Analysis of Digital Filters european symposium on programming. pp. 33- 48 ,(2004) , 10.1007/978-3-540-24725-8_4
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, Xavier Rival, Design and Implementation of a Special-Purpose Static Program Analyzer for Safety-Critical Real-Time Embedded Software Lecture Notes in Computer Science. ,vol. 2566, pp. 85- 108 ,(2002) , 10.1007/3-540-36377-7_5
Mardavij Roozbehani, Eric Feron, Alexandre Megrestki, Modeling, Optimization and Computation for Software Verification Hybrid Systems: Computation and Control. pp. 606- 622 ,(2005) , 10.1007/978-3-540-31954-2_39
David Monniaux, Compositional Analysis of Floating-Point Linear Numerical Filters Computer Aided Verification. pp. 199- 212 ,(2005) , 10.1007/11513988_21
P. Caspi, D. Pilaud, N. Halbwachs, J. A. Plaice, LUSTRE: a declarative language for real-time programming symposium on principles of programming languages. pp. 178- 188 ,(1987) , 10.1145/41625.41641
Siegfried M. Rump, Ten methods to bound multiple roots of polynomials Journal of Computational and Applied Mathematics. ,vol. 156, pp. 403- 432 ,(2003) , 10.1016/S0377-0427(03)00381-9
Leland B. Jackson, On the Interaction of Roundoff Noise and Dynamic Range in Digital Filters* Bell System Technical Journal. ,vol. 49, pp. 159- 184 ,(1970) , 10.1002/J.1538-7305.1970.TB01763.X
B.D. Rao, Floating point arithmetic and digital filters IEEE Transactions on Signal Processing. ,vol. 40, pp. 85- 95 ,(1992) , 10.1109/78.157184