Sciweavers

Share
CAV
2003
Springer

Certifying Optimality of State Estimation Programs

11 years 4 months ago
Certifying Optimality of State Estimation Programs
Abstract. The theme of this paper is certifying software for state estimation of dynamic systems, which is an important problem found in spacecraft, aircraft, geophysical, and in many other applications. The common way to solve state estimation problems is to use Kalman filters, i.e., stochastic, recursive algorithms providing statistically optimal state estimates based on noisy sensor measurements. We present an optimality certifier for Kalman filter programs, which is a system taking a program claiming to implement a given formally specified Kalman filter, as well as a formal certificate in the form of assertions and proof scripts merged within the program via annotations, and tells whether the code correctly implements the specified state estimation problem. Kalman filter specifications and certificates can be either produced manually by expert users or can be generated automatically: we also present our first steps in merging our certifying technology with AutoFilter, a ...
Grigore Rosu, Ram Prasad Venkatesan, Jon Whittle,
Added 06 Jul 2010
Updated 06 Jul 2010
Type Conference
Year 2003
Where CAV
Authors Grigore Rosu, Ram Prasad Venkatesan, Jon Whittle, Laurentiu Leustean
Comments (0)
books