Formal Verification for Autopilot - Preliminary state of the art

Christophe Garion (1) , Gautier Hattenberger (2) , Baptiste Pollien (1) , Pierre Roux (3) , Xavier Thirioux (1)

1 ISAE-SUPAERO - Institut Supérieur de l'Aéronautique et de l'Espace
2 ENAC - Ecole Nationale de l'Aviation Civile
3 DTIS, ONERA, Université de Toulouse [Toulouse]

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.

Mots clés: Verification and validation; Formal methods; Cyberphysical systems

Domaines: Informatique [cs]; Logiciel mathématique [cs.MS]; Théorie et langage formel [cs.FL]; Systèmes embarqués

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⟩