Skip to Main content Skip to Navigation

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
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 produced by the author(s)


  • HAL Id : hal-03255656, version 1



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⟩



Record views


Files downloads