Formal Verification of Marzullo's Sensor Fusion Interval

John Rushby

Technical Report, January 2002

Abstract

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 return a range of values and describe the "fusion functions" of Marzullo and of Schmid and Schossmaier. We use PVS formally to prove the soundness of Marzullo's function (i.e., it always contains the correct value), from which soundness of Schmid and Schossmaier's function follows. The latter is generally to be preferred to the former because it satisfies a "Lipschitz Condition" (small changes in sensor readings produce small changes in its output), and is optimal among all such functions.

gzipped postscript, or plain postscript or PDF or crude ascii (for your Palm Pilot)

BibTeX Entry


@TECHREPORT{Rushby02:Marzullo,
	TITLE = {Formal Verification of {Marzullo's} Sensor Fusion Interval},
	AUTHOR = {John Rushby},
	INSTITUTION = {Computer Science Laboratory, SRI International},
	ADDRESS = {Menlo Park, CA},
	MONTH = jan,
	YEAR = 2002
}
Having trouble reading our papers?
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page