Static Analysis of Digital Filters ESOP

Jérôme Feret

Description

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

Sujets

• Run time (computing)

Informations

• Publié par: pefav
• Nombre de lectures: 7
• Langue: English

Extrait

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 fixpoint inference of contracting function in floating-point arithmetics
7. Basic simplified filters
8. Other simplified filters
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 floating
point numbers.
Full certification requires special care about these filters.
Jérôme Feret 3 December 2008Issues
• Control flow detection: to locate filter resets and filter 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 floating-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 fixpoint inference of contracting function in floating-point arithmetics
7. Basic simplified filters
8. Other simplified filters
9. Filter expansion
10. Conclusion
Jérôme Feret 5 December 2008;;;;;
The high bandpass filter
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 (simplified)
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. finally, it keeps iterating to refine 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 filter (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 filter (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