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 条

[21] A flight plan for success
Flynn, G
WORKFORCE, 1997, 76 (07): : 72 - +
[22] A flight plan for 2000
North, DM
AVIATION WEEK & SPACE TECHNOLOGY, 2000, 152 (01): : 70 - 70
[23] Flight dynamics for UAV formations
Chelaru, Teodor-Viorel
Pana, Valentin
Chelaru, Adrian
RECENT ADVANCES IN AUTOMATION & INFORMATION: PROCEEDINGS OF THE 10TH WSEAS INTERNATIONAL CONFERENCE ON AUTOMATION & INFORMATION (ICAI'09), 2009, : 287 - +
[24] Flight dynamics for a BWB UAV
Anton, Ștefan-Mihai
Pârvu, Petrișor
1600, Politechnica University of Bucharest (82): : 73 - 82
[25] Supersonic UAV flight tests
不详
AEROSPACE ENGINEERING, 2002, 22 (11) : 31 - 31
[26] First flight for 'flapless' UAV
Engineer, 2010, SEPTEMBER
[27] OPERABILITY VERIFIED IN GE90 FLIGHT TESTS
KANDEBO, SW
DORNHEIM, MA
AVIATION WEEK & SPACE TECHNOLOGY, 1995, 142 (13): : 52 - 54
[28] Automated multiple UAV flight - the Stanford DragonFly UAV program
Teo, R
Jang, JS
Tomlin, CJ
2004 43RD IEEE CONFERENCE ON DECISION AND CONTROL (CDC), VOLS 1-5, 2004, : 4268 - 4273
[29] RADICAL NEW FLIGHT PLAN
Tully, Shawn
FORTUNE, 2015, 172 (05) : 128 - +
[30] Stochastic Flight Plan Optimization
de Oliveira, Italo Romani
Altus, Steve
Tiourine, Sergey
Neto, Euclides C. Pinto
Leite, Alexandre
de Azevedo, Felipe C. F.
2023 IEEE/AIAA 42ND DIGITAL AVIONICS SYSTEMS CONFERENCE, DASC, 2023,

← 1 2 3 4 5 →