On Formal Verification of Data-Driven Flight Awareness: Leveraging the Cramér-Rao Lower Bound of Stochastic Functional Time Series Models

This work investigates the application of the Cramér-Rao Lower Bound (CRLB) theorem, within the framework of Dynamic Data Driven Applications Systems (DDDAS), in view of the formal verificationof state estimates via stochastic Vector-dependent Functionally Pooled Auto-Regressive (VFP-AR) models. The VFP-AR model is identified via data obtained from wind tunnel experiments on a “fly-by-feel” wing structure under multiple flight states (i.e., angle of attack, velocity). The VFP-based CRLB of the state estimates is derived for each true flight state reflecting the state estimation capability of the model considering the data, model, and estimation assumptions. Apart from the CRLB obtained from pristine data and models, CRLBs are estimated using either artificially corrupted testing data and/or sub-optimal models. Comparisons are made between CRLB and state estimations from corrupted and pristine conditions. The verification of the obtained state estimates is mechanically verified the formal proof of the CRLB Theorem using Athena, which provides irrefutable guarantee of soundness as long as specified assumptions are followed. The results of the study indicate the potential of using a CRLB-based formal verification framework for state estimation via stochastic FP time series models.