15 Pages
English

Static Analysis of Digital Filters

-

Gain access to the library to view online
Learn more

Description

Niveau: Supérieur, Doctorat, Bac+8
Static Analysis of Digital Filters? Jerome Feret DI, Ecole Normale Superieure, Paris, FRANCE Abstract We present an Abstract Interpretation-based framework for automatically analyzing programs containing digital filters. Our frame- work allows refining existing analyses so that they can handle given classes of digital filters. We only have to design a class of symbolic prop- erties that describe the invariants throughout filter iterations, and to describe how these properties are transformed by filter iterations. Then, the analysis allows both inference and proofs of the properties about the program variables that are tied to any such filter. 1 Introduction Digital filters are widely used in real-time embedded systems (as found in auto- motive, aeronautic, and aerospace applications) since they allow modeling into software behaviors previously ensured by analogical filters. A filter transforms an input stream of floating-point values into an output stream. Existing analyses are very imprecise in bounding the range of the output stream, because of the lack of precise linear properties that would entail that the output is bounded. The lack of precise domains when analyzing digital filters was indeed the cause of almost all the remaining warnings (potential floating-point overflows) in the certification of a critical software family with the analyzer described in [1,2]. In this paper, we propose an Abstract Interpretation-based framework for designing new abstract domains which handle filter classes.

  • abstract interpretation

  • all real

  • filter can

  • floating- point rounding errors

  • variable e0 denotes

  • handle given

  • global behavior

  • a? ?

  • such


Subjects

Informations

Published by
Reads 15
Language English
Static Analysis of Digital Filters?
Je´rˆomeFeret´DI,EcoleNormaleSup´erieure,Paris,FRANCEjerome.feret@ens.fr
AbstractWe present an Abstract Interpretation-based framework forautomatically analyzing programs containing digital filters. Our frame-work allows refining existing analyses so that they can handle givenclasses of digital filters. We only have to design a class of symbolic prop-erties that describe the invariants throughout filter iterations, and todescribe how these properties are transformed by filter iterations. Then,the analysis allows both inference and proofs of the properties about theprogram variables that are tied to any such filter.
1 IntroductionDigital filters are widely used in real-time embedded systems (as found in auto-motive, aeronautic, and aerospace applications) since they allow modeling intosoftware behaviors previously ensured by analogical filters. A filter transformsan input stream of floating-point values into an output stream. Existing analysesare very imprecise in bounding the range of the output stream, because of thelack of precise linear properties that would entail that the output is bounded.The lack of precise domains when analyzing digital filters was indeed the causeof almost all the remaining warnings (potential floating-point overflows) in thecertification of a critical software family with the analyzer described in [1,2].In this paper, we propose an Abstract Interpretation-based framework fordesigning new abstract domains which handle filter classes. Human interventionis required for discovering the general shape of the properties that are requiredin proving the stability of such a filter. Roughly speaking, filter properties aremainly an abstraction of the input stream, from which we deduce bounds onthe output stream. Our framework can then be used to build the correspondingabstract domain. This domain propagates all these properties throughout theabstract computations of programs. Our approach is not syntactic, so that loopunrolling, filter reset, boolean control, and trace (or state) partitioning are dealtwith for free and any filter of the class (for any setting) is analyzed precisely.Moreover, in case of linear filters, we propose a general approach to build thecorresponding class of properties. We first design a rough abstraction, in whichat each filter iteration, we do not distinguish between the contributions of eachinput. Then, we design a precise abstraction: using linearity, we split the outputbetween the global contribution of floating-point errors, and the contribution of´?This work was partially supported by the ASTREE RNTL project.