Formal SPARK Verification of Various Resampling Methods in Particle Filters

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 25, 2022
Accession Number
AD1166932

Entities

People

  • Osiris J Terry

Organizations

  • Air Force Institute of Technology

Tags

DTIC Thesaurus Topics

  • Abstracts
  • Availability
  • Classification
  • Contracts
  • Cooperation
  • Copyrights
  • Department Of Defense
  • Instructions
  • Law
  • Monitoring
  • Security
  • Translations

Fields of Study

  • Computer science
  • Engineering

Readers

  • Computational Modeling and Simulation
  • Computer Vision.
  • Internal Combustion Engine (ICE) Technology.