OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Formal Verification for Autopilot - Preliminary state of the art

Pollien, Baptiste and Thirioux, Xavier and Garion, Christophe and Gautier, Hattenberger and Roux, Pierre Formal Verification for Autopilot - Preliminary state of the art. (2021) [Report]

(Document in English)

PDF (Author's version) - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader


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.

Item Type:Report
Uncontrolled Keywords:
Institution:Université de Toulouse > Ecole Nationale de l'Aviation Civile - ENAC (FRANCE)
Université de Toulouse > Institut Supérieur de l'Aéronautique et de l'Espace - ISAE-SUPAERO (FRANCE)
French research institutions > Office National d'Etudes et Recherches Aérospatiales - ONERA (FRANCE)
Laboratory name:
Deposited On:10 Jun 2021 15:40

Repository Staff Only: item control page