Formal Verification of Marzullo's Sensor Fusion Interval
John Rushby · 2002
We examine the problem of selecting a best value from a collection of sensor readings, and diagnosing faulty readings in such a collection. We focus on sensor interfaces that re-turn a range of values and describe the “fusion functions ” � f,n (S) of Marzullo and F f n (S) of Schmid and Schossmaier. We use PVS formally to prove the soundness of � f,n (S) (i.e., it always contains the correct value), from which soundness of F f n (S) also follows. F f n (S) is generally to be preferred to � f,n (S) because it satisfies a “Lipschitz Condition ” (small changes in sensor readings produce small changes in its output), and is optimal among all such functions. i