Skip to Main content Skip to Navigation
Reports

Formal Verification for Autopilot - Preliminary state of the art

Abstract : This document is a preliminary state of the art for the formal verification of the autopilot of an Unmanned Air Vehicle (UAV). We will first present UAV autopilots and more specifically the Paparazzi autopilot developed at ENAC which will be our case study. We then present which properties could be verified and on which representation of the autopilot (source code, model). A more complete state of the art of current formal methods will be then detail and focus on deductive methods, abstract interpretation, model checking and proof assistants. Finally, some immediate perspective for the thesis are proposed.
Complete list of metadata

https://hal.archives-ouvertes.fr/hal-03255656
Contributor : Baptiste Pollien Connect in order to contact the contributor
Submitted on : Thursday, June 10, 2021 - 10:08:40 AM
Last modification on : Wednesday, March 30, 2022 - 1:08:57 PM
Long-term archiving on: : Saturday, September 11, 2021 - 6:07:21 PM

Files

formal_verification_for_autopi...
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03255656, version 1

Collections

Citation

Christophe Garion, Gautier Hattenberger, Baptiste Pollien, Pierre Roux, Xavier Thirioux. Formal Verification for Autopilot - Preliminary state of the art. [Technical Report] ISAE-SUPAERO; ONERA -- The French Aerospace Lab; ENAC. 2022. ⟨hal-03255656⟩

Share

Metrics

Record views

142

Files downloads

77