Formal Verification for Autopilot - Preliminary state of the art
Baptiste Pollien, Xavier Thirioux, Christophe Garion, Gautier Hattenberger, Pierre Roux · Open Archive Toulouse Archive Ouverte (University of Toulouse) · 2021
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.