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 条

[31] Plan targets flight schools
不详
AVIATION WEEK & SPACE TECHNOLOGY, 2001, 154 (09): : 69 - 69
[32] FLIGHT PLAN . MAN TO MARS
LEARY, F
SPACE AERONAUTICS, 1970, 53 (02): : 28 - &
[33] FAA files flight plan
Fiorino, F
AVIATION WEEK & SPACE TECHNOLOGY, 2003, 159 (17): : 43 - 43
[34] NEW FLIGHT PLAN FOR AIRLINES
BURCK, G
FORTUNE, 1969, 79 (04) : 98 - &
[35] CLEMENTINE FLIGHT PLAN WAS MINE
FARQUHAR, RW
AVIATION WEEK & SPACE TECHNOLOGY, 1995, 142 (07): : 6 - 6
[36] A FLIGHT PLAN FOR ANESTHESIA - COMMENT
HAIN, WR
ANAESTHESIA, 1983, 38 (04) : 390 - 390
[37] THE LIBRARY TOUR FLIGHT PLAN
VOIGT, K
OHIO JOURNAL OF SCIENCE, 1983, 83 (02) : 98 - 98
[38] BAES FLIGHT PLAN FOR THE FUTURE
GREEK, D
PROFESSIONAL ENGINEERING, 1994, 7 (15) : 7 - 8
[39] Australia approves UAV patrol plan
Nrown, Nick
Kemp, Damian
Jane's Defence Weekly, 2006, (JULY):
[40] Flight Planning and Guidance Features for an UAV Flight Management Computer
Eliker, Karam
Bouadi, H.
Haddad, M.
2016 IEEE 21ST INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION (ETFA), 2016,

← 1 2 3 4 5 →