Certifying optimality of state estimation programs

The common way to solve state estimation problems is to use Kalman filters. A Kalman filter is essentially a set of mathematical equations implementing a predictor-corrector type estimation that is optimal in the sense that it minimizes the estimated error between the real and the predicted states.

Despite their apparent simplicity, implementations of state estimation problems are quite hard to prove correct. Correctness in this context means that the state calculated by a given implementation, called the state estimate, is mathematically optimal when one considers all the hypotheses given in the description of the state estimation problem. Description of such problems are given as sets of stochastic difference equations, and optimality is rigorously, and statistically formulated using matrix differentiation.

We next provide a certifier to validate Kalman filters. The prototype can be downloaded and is easy to use. We refer the interested reader to a draft paper and to CS497GR Fall 2002 lecture notes commenting on certification with respect to specifications.

  • Certifying Optimality of State Estimation Programs [ps, pdf],
  • CS497GR Fall 2002lecture notes (see lectures 14 to 19).

    Preparing for Installation

    In order to run the Certifier, one first needs to have Maude and Perl installed on one's platform. Both these languages are freely distributed: It is not necessary to know these languages in order to use our prototype below.

    In addition, you will also need Maude's Inductive Theorem prover: itp-2.3.6.tar.gz

    Downloading and Installing Domain Specific Certifier for Kalman Filters

    Our tool should work on any system running both Maude and Perl. On Unix platforms users can do the following:
    • Step 1: download kalman.tar.gz and save it in the directory where you want to install it;
    • Step 2: run gunzip and then tar -xvf to extract all the needed files;
    • Step 3: remove the file kalman.tar. The following files should be now in your directory: 
      bash$ ls -R
.:
certifier    domain    ekf.txt    if.txt    kf.txt

./domain:
domain.maude    lemmas

./lemmas:
lemma-1    lemma-15   lemma-2    lemma-24   lemma-29   lemma-33   lemma-7
lemma-10   lemma-16   lemma-20   lemma-25   lemma-30   lemma-34   lemma-8
lemma-12   lemma-17   lemma-21   lemma-26   lemma-31   lemma-4    lemma-9
lemma-13   lemma-18   lemma-22   lemma-27   lemma-32   lemma-5    
lemma-14   lemma-19   lemma-23   lemma-28   lemma-33   lemma-6    


bash$
      The tool certifier, written in PERL, is a domain specific certifier that validates the Kalman filter codes using the axioms and lemmas present in domain. kf.txt is a simple Kalman filter code written by hand while ekf.txt and if.txt represent the extended Kalman filter and information filter, respectively. Our tool can validate all the three Kalman filter codes.

      Configuration

      The prototype needs to be configured before use. This essentially means to update the absolute paths to the needed files, and it can all be done by simply editing the PERL file certifier as follows:
      • Perl. Line 1: Add the path to your desired PERL binary to be used with this application;
      • Maude. Line 7: Add the path to your Maude V.1.0.5. binary;
      • Maude ITP. Line 9: Add the path to your Maude itp-2.3.6 directory;
      • Domain. Line 11: Change the path appropriately if you decide to store the domain in a different directory;
      • Lemmas. Line 13: Change the path appropriately if you decide to store the lemmas in a different directory.
      In case you want to use the tool from any directory on your machine then make sure that you add the path to the file certifier to your environment PATH variable.

      Execution

      The certifier runs in command mode: 
      certifier [-cgv] filename
      By default, the certifier cleans the Kalman filter code, generates the proof scripts for the lemmas and proof tasks and then validates the code. It saves two intermediate codes obtained after cleaning and generating the proof scripts for potential further interest. For example, running certifier kf.txt would certify the code after creating two intermediate versions kf-clean.txt and kf-expand.txt . In addition to verifying the code, the certifier also creates a copy of the proof tasks and the interaction with Maude ITP in a directory called tasks

      In addition, options are provided to suit the varied needs of the user. Each of the option disables the saving of that particular operation. -c disables the saving of the cleaned code, -g results in the expanded proof script not being saved while -v just cleans and generates the proof scripts and doesn't verify the code. These options can be used together depending on the user's needs. For example certifier -g kf.txt would verifying the code and save only the cleaned code.

      Contact Information

      For further questions, please mail us at Grigore Rosu, and/or Ram Prasad Venkatesan.

      Last modified: February 07, 2002.