Date of Award
3-2022
Document Type
Thesis
Degree Name
Master of Science in Electrical Engineering
Department
Department of Electrical and Computer Engineering
First Advisor
Kenneth M. Hopkinson, PhD
Abstract
The software verification in this thesis concentrates on verifying a particle filter for use in tracking and estimation, a key application area for the Air Force. The development and verification process described in this thesis is a demonstration of the power, limitation, and compromises involved in applying automated software verification tools to critical embedded software applications.
AFIT Designator
AFIT-ENG-MS-22-M-067
DTIC Accession Number
AD1166932
Recommended Citation
Terry, Osiris J., "Formal SPARK Verification of Various Resampling Methods in Particle Filters" (2022). Theses and Dissertations. 5370.
https://scholar.afit.edu/etd/5370