Abstract
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.
Baptiste Pollien, PhD
Software Engineer HMI
I am a Software Engineer HMI at Ampere Software Technology.