A Verified UAV Flight Plan Generator

被引：0
|
作者：
Pollien, Baptiste [1 ]
Garion, Christophe [1 ]
Hattenberger, Gautier [2 ]
Roux, Pierre [3 ]
Thirioux, Xavier [1 ]
机构：
[1] Univ Toulouse, ISAE, SUPAERO, Toulouse, France
[2] Univ Toulouse, ENAC, Toulouse, France
[3] Off Natl Etud & Rech Aerosp, Toulouse, France
来源：
2023 IEEE/ACM 11TH INTERNATIONAL CONFERENCE ON FORMAL METHODS IN SOFTWARE ENGINEERING, FORMALISE | 2023年
关键词：
Code Generation; Compilation; Mechanized proof; Operational semantics;
D O I：
10.1109/FormaliSE58978.2023.00021
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
FPL is a domain specific language used to specify complex drone missions for the Paparazzi open-source autopilot. FPL missions are compiled into C code that is directly embedded into the autopilot code. The FPL to C code generator, currently written in OCaml, is therefore a critical component when addressing the drone safety. This paper presents the formal verification of the FPL compilation process. First, we have developed in Coq a new three-pass code generator, targeting the Clight intermediate language from the CompCert suite. We have then formally defined an operational semantics for FPL. Finally, we have proved a bisimulation relation between FPL semantics and Clight semantics. In the course of the formalization and verification process, we have also unveiled several problems in the original Paparazzi code generator.
引用
收藏
页码：130 / 140
页数：11
相关论文
共 50 条
  • [1] UAV Flight Plan Optimzed for Sensor Requirements
    Lentilhac, Sophie
    IEEE AEROSPACE AND ELECTRONIC SYSTEMS MAGAZINE, 2010, 25 (02) : 11 - 14
  • [2] Plan Sharing: Showcasing Coordinated UAV Formation Flight
    Hexmoor, Henry
    Eluru, Swetha
    Sabaa, Hadi
    INFORMATICA-JOURNAL OF COMPUTING AND INFORMATICS, 2006, 30 (02): : 183 - 192
  • [3] Parametric Statistical Model Checking of UAV Flight Plan
    Bao, Ran
    Attiogbe, Christian
    Delahaye, Benoit
    Fournier, Paulin
    Lime, Didier
    FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS (FORTE 2019), 2019, 11535 : 57 - 74
  • [4] Increasing UAV capabilities through autopilot and flight plan abstraction
    Santamaria, Eduard
    Royo, Pablo
    Lopez, Juan
    Barrado, Cristina
    Pastor, Enric
    Prats, Xavier
    2007 IEEE/AIAA 26TH DIGITAL AVIONICS SYSTEMS CONFERENCE, VOLS 1-3, 2007, : 988 - 997
  • [5] Verbatim: A Verified Lexer Generator
    Egolf, Derek
    Lasser, Sam
    Fisher, Kathleen
    2021 IEEE SYMPOSIUM ON SECURITY AND PRIVACY WORKSHOPS (SPW 2021), 2021, : 92 - 100
  • [6] A verified formal model of a VC generator
    Arthan, R. D.
    30TH ANNUAL IEEE/NASA SOFTWARE ENGINEERING WORKSHOP, PROCEEDINGS, 2006, : 263 - 271
  • [7] Machine-verified code generator
    Walther, C
    Schweitzer, S
    LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2003, 2850 : 91 - 106
  • [8] A MECHANICALLY VERIFIED VERIFICATION CONDITION GENERATOR
    HOMEIER, PV
    MARTIN, DF
    COMPUTER JOURNAL, 1995, 38 (02): : 131 - 141
  • [9] Flight plan
    Hicok, Bob
    AMERICAN POETRY REVIEW, 2017, 46 (04): : 12 - 12
  • [10] Flight plan
    Zolfagharifard, Ellie
    Engineer, 2009, 294 (7773) : 30 - 31
12345