Static Analysis of Digital Filters ESOP

pages

English

Documents

Écrit par
Jérôme Feret

Publié par
pefav

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

pages

English

Ebook

Lire un extrait

Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus

Publié par

pefav

Nombre de lectures

Langue

English

MPRI Static Analysis of Digital Filters ESOP 2004 Jérôme Feret Laboratoire d'Informatique de l'École Normale Supérieure INRIA, ÉNS, CNRS feret December, 2008.

laboratoire d'informatique de l'ecole normale

requires special care

filter expansion

run time error

floating-point arithmetics

linear invariants

Voir

Publié par

pefav

Nombre de lectures

Langue

English

Run time (computing)

nferetf.i.wwwh//e:dps.ttr/
MPRI
Static Analysis of Digital Filters
ESOP 2004
Jérôme Feret
Laboratoire d’Informatique de l’École Normale Supérieure
INRIA, ÉNS, CNRS
∼
December, 2008.Overview
1. Introduction
2. Case study
3. Concrete semantics
4. Generic aproximation
5. Filter extension
6. Post ﬁxpoint inference of contracting function in ﬂoating-point arithmetics
7. Basic simpliﬁed ﬁlters
8. Other simpliﬁed ﬁlters
9. Filter expansion
10. Conclusion
Jérôme Feret 2 December 2008Context
We want to prove run time error absence, in critical embedded software.
Filter behaviour is implemented at the software level, using hardware ﬂoating
point numbers.
Full certiﬁcation requires special care about these ﬁlters.
Jérôme Feret 3 December 2008Issues
• Control ﬂow detection: to locate ﬁlter resets and ﬁlter iterations.
• Invariant inference: we are not interested in functional properties.
We seek precise bounds on the output, using information inferred about
the input.
(Linear invariants do not yield accurate bounds).
• To take into account ﬂoating-point rounding:
-- in the semantics,
-- when implementing the abstract domain.
Jérôme Feret 4 December 2008Overview
1. Introduction
2. Case study
3. Concrete semantics
4. Generic aproximation
5. Filter extension
6. Post ﬁxpoint inference of contracting function in ﬂoating-point arithmetics
7. Basic simpliﬁed ﬁlters
8. Other simpliﬁed ﬁlters
9. Filter expansion
10. Conclusion
Jérôme Feret 5 December 2008;;;;;
The high bandpass ﬁlter
We consider the following example:
V ∈R E := 0 S := 0
1
while (V ≥ 0){
V ∈R T ∈R
E ∈ [−1;1];
0
if (T ≥ 0){S := 0}
else{S := 0.999×S +E −E }
0 1
E := E ;
1 0
}
Jérôme Feret 6 December 2008Interval approximation (simpliﬁed)
With a view to simplifying, we ignore rounding errors !!!
♯
The analyzer infers the following sound counterpartF :
? ?
♯
F X ={0.999∗s +e +e | s∈ X, e ,e ∈ [−1; 1]}
0 1 0 1
to the loop body.
Jérôme Feret 7 December 2008Abstract iteration
♯
1. The analyzer starts iteratingF :
♯
F ({0}) = [−2;2],
♯
F ([−2;2]) = [−3.998;3.998],
. . . ;
2. then it widens the iterates:
♯
F ([−10;10])6? [−10;10],
♯
F ([−100;100])6? [−100;100],
. . . ;
3. until it discovers a stable threshold:
♯
F ([−10000;10000]) = [−9992;9992];
4. ﬁnally, it keeps iterating to reﬁne the solution:
♯
F ([−9992;9992]) = [−9984.008;9984.008].
Jérôme Feret 8 December 2008Driving the analysis
Better results could have been obtained by driving the analysis:
Theorem 1 (High bandpass ﬁlter (history-insensitive))
Let D≥ 0, m≥ 0, a, X and Z be real numbers such that:
1. |X|≤ D;
2. aX−m≤ Z ≤ aX +m;
then we have:
1. |Z|≤|a|D +m;
? ?
m
2. |a| < 1 and D≥ =⇒ |Z|≤ D. ?
1−|a|
Theorem 1 implies that 2000 can be used as a threshold.
Jérôme Feret 9 December 2008History sensitive approximation
Theorem 2 (High bandpass ﬁlter (history-sensitive version))
1
Let α∈ [ ;1[, i and m > 0 be real numbers.
2
Let E be a real number sequence, such that∀k∈N, E ∈ [−m;m].
n k
Let S be the following sequence:
n
?
S = i
0
S = α.S +E −E .
n+1 n n+1 n
We have:
P
n−1
n n l−1
1. S = α .i +E −α E + (α− 1)α E
n n 0 n−l
l=1
n n n−1
2. |S |≤|α| |i| + (1 +|α| +|1−α |)m;
n
3. |S |≤ 2.m +|i|. ?
n
Theorem 2 implies that 2 is a sound bound on|S|.
Jérôme Feret 10 December 2008