Formal verification of maneuvering target tracking

Abstract

The paper introduces the application of a formal verification (model checking) technique for improvements in the performance of maneuvering target tracking. Formal methods is a well-established completely automatic approach to system verification which analyzes a system model behavior against desired properties. Formal methods provide a full-coverage verification of the system model behavior. In this paper, we look into the problem of tracking a maneuvering ballistic missile, based on bearings-only measurements. The interception parameter estimations are essential for the implementation of efficient guidance laws. Assuming knowledge of a target model, a standard Extended Kalman Filter was applied. This filter is known to produce biased estimations of the range and range rate. The applied estimation debiasing heuristic procedure consists of multiplication of the state covariance matrix by a scalar fudge factor at every sampling time, and the use of this modified state covariance matrix in the covariance update equation. The value of the scalar fudge factor was obtained by using the RuleBase formal verification engine - a formal verification tool developed by the IBM company. We also checked the consistency and capturability properties of the true proportional navigation guidance law. The numerical results of a realistic representative case are presented. © 2003 by the authors.