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 detailed 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 : Thursday, December 2, 2021 - 10:18:02 AM
Long-term archiving on: : Saturday, September 11, 2021 - 6:07:21 PM


Files produced by the author(s)


  • HAL Id : hal-03255656, version 1



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



Les métriques sont temporairement indisponibles