Matrix Theory for Data Association in PVS

Consider a collection of data generated by sensors from a set of aircraft. Data association is the process of connecting each sensor measurement with its corresponding aircraft. Furthermore once the data association has taken place, the state of the aircraft can be approximated using a Kalman filter. This talk aims to explore formal specification and verification of data association in the Prototype Verification System (PVS). Formal specification and verification of data association includes development of Kalman filters, Mahalanobis distance, and other topics of matrix analysis in PVS.