Certifying optimality of state estimation programs

Grigore Rosu, Ram Prasad Venkatesan, Jon Whittle, Laurenţiu Leuştean

Research output: Chapter in Book/Report/Conference proceedingChapter

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 NASA Ames state estimation program synthesis system, the idea being that AUTOFILTER synthesizes proof certificates together with the code.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsWarren A. Hunt, Fabio Somenzi
PublisherSpringer-Verlag
Pages301-314
Number of pages14
ISBN (Print)3540405240, 9783540405245
StatePublished - Jan 1 2003

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2725
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

State Estimation
State estimation
Kalman filters
Kalman Filter
Optimality
Certificate
Program Synthesis
Recursive Algorithm
NASA
Spacecraft
Assertion
Merging
Dynamic Systems
Annotation
Aircraft
Dynamical systems
Specification
Specifications
Sensor
Software

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Rosu, G., Venkatesan, R. P., Whittle, J., & Leuştean, L. (2003). Certifying optimality of state estimation programs. In W. A. Hunt, & F. Somenzi (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 301-314). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2725). Springer-Verlag.

Certifying optimality of state estimation programs. / Rosu, Grigore; Venkatesan, Ram Prasad; Whittle, Jon; Leuştean, Laurenţiu.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). ed. / Warren A. Hunt; Fabio Somenzi. Springer-Verlag, 2003. p. 301-314 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 2725).

Research output: Chapter in Book/Report/Conference proceedingChapter

Rosu, G, Venkatesan, RP, Whittle, J & Leuştean, L 2003, Certifying optimality of state estimation programs. in WA Hunt & F Somenzi (eds), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 2725, Springer-Verlag, pp. 301-314.
Rosu G, Venkatesan RP, Whittle J, Leuştean L. Certifying optimality of state estimation programs. In Hunt WA, Somenzi F, editors, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer-Verlag. 2003. p. 301-314. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Rosu, Grigore ; Venkatesan, Ram Prasad ; Whittle, Jon ; Leuştean, Laurenţiu. / Certifying optimality of state estimation programs. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). editor / Warren A. Hunt ; Fabio Somenzi. Springer-Verlag, 2003. pp. 301-314 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inbook{69b81c106cbf4f1ab833b7604d58559b,
title = "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 NASA Ames state estimation program synthesis system, the idea being that AUTOFILTER synthesizes proof certificates together with the code.",
author = "Grigore Rosu and Venkatesan, {Ram Prasad} and Jon Whittle and Laurenţiu Leuştean",
year = "2003",
month = "1",
day = "1",
language = "English (US)",
isbn = "3540405240",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "301--314",
editor = "Hunt, {Warren A.} and Fabio Somenzi",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - CHAP

T1 - Certifying optimality of state estimation programs

AU - Rosu, Grigore

AU - Venkatesan, Ram Prasad

AU - Whittle, Jon

AU - Leuştean, Laurenţiu

PY - 2003/1/1

Y1 - 2003/1/1

N2 - 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 NASA Ames state estimation program synthesis system, the idea being that AUTOFILTER synthesizes proof certificates together with the code.

AB - 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 NASA Ames state estimation program synthesis system, the idea being that AUTOFILTER synthesizes proof certificates together with the code.

UR - http://www.scopus.com/inward/record.url?scp=35248895371&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=35248895371&partnerID=8YFLogxK

M3 - Chapter

AN - SCOPUS:35248895371

SN - 3540405240

SN - 9783540405245

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 301

EP - 314

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

A2 - Hunt, Warren A.

A2 - Somenzi, Fabio

PB - Springer-Verlag

ER -