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 条
  • [41] Flight Path Optimization of Solar Powered UAV for Endurance Flight
    Lee, Joo-Seok
    Park, Hyeon-Bo
    Yu, Kee-Ho
    2015 54TH ANNUAL CONFERENCE OF THE SOCIETY OF INSTRUMENT AND CONTROL ENGINEERS OF JAPAN (SICE), 2015, : 820 - 823
  • [42] Design Flight Control System for UAV Full Envelope Flight
    Lu Ke
    Liu Chun-Sheng
    Wang Zheng-Zhong
    Cheng Qi-You
    2015 27TH CHINESE CONTROL AND DECISION CONFERENCE (CCDC), 2015, : 487 - 490
  • [43] Plan Layout Generator (PLG) A Rule-Based Plan Layout Generator for Mardin Houses
    Torus, Belinda
    Colakoglu, Birgul
    ECAADE 2009: COMPUTATION: THE NEW REALM OF ARCHITECTURAL DESIGN, 2009, : 425 - 430
  • [44] First flight a success for Outrider UAV
    Fulghum, DA
    AVIATION WEEK & SPACE TECHNOLOGY, 1997, 146 (11): : 37 - 37
  • [45] Accelerated determination of UAV flight envelopes
    Bodnar, Michael R.
    Long, Lyle N.
    Humphrey, John R.
    Kelmelis, Eric J.
    MODELING AND SIMULATION FOR MILITARY OPERATIONS III, 2008, 6965
  • [46] Helicopter UAV readied for flight test
    Wall, R
    AVIATION WEEK & SPACE TECHNOLOGY, 2000, 153 (08): : 31 - 31
  • [47] Coordinated UAV Manoeuvring Flight Formation
    Hexmoor, Henry
    Rahimi, Shahram
    Little, Jody T.
    INFORMATICA-JOURNAL OF COMPUTING AND INFORMATICS, 2009, 33 (03): : 375 - 383
  • [48] UAV Simulation Flight Training System
    Liu, Horan
    Bi, Zhenni
    Dai, Jianqi
    Yu, Yang
    Shi, Yunda
    2018 8TH INTERNATIONAL CONFERENCE ON VIRTUAL REALITY AND VISUALIZATION (ICVRV), 2018, : 150 - 151
  • [49] Uav shooting flight path optimization
    Gong, Liyue
    Wang, Zhongnan
    Shen, Tiancheng
    BASIC & CLINICAL PHARMACOLOGY & TOXICOLOGY, 2020, 126 : 122 - 123
  • [50] UAV as a reliable wingman: A flight demonstration
    Waydo, S.
    Hauser, J.
    Bailey, R.
    Klavins, E.
    Murray, R. M.
    IEEE TRANSACTIONS ON CONTROL SYSTEMS TECHNOLOGY, 2007, 15 (04) : 680 - 688
12345