VFPG: Verified Flight Plan Generator
VFPG is a generator of flight plan developed in Ocaml and Coq. The generator takes as input an XML describing the a flight plan and it generates a C code that can be compiled and embedded on a drone.
This project is mainely designed to work with the Paparazzi UAV autopilot (https://github.com/paparazzi/paparazzi). However, the generator has a modular architecture that can be adapted to support easily others autopilots.
- Coq (tested with version 8.15)
- OCaml (tested with version 4.13.1)
- OCamlbuild (tested with version 0.14.1)
- xml-light (tested with version 2.4)
MathComp is required and can be installed using OPAM (version 2.0 or later):
opam repo add coq-released https://coq.inria.fr/opam/released opam install coq-mathcomp-ssreflect
Using the Generator
The generator can then be built using the Makefile.
The generator can then be used with the following command:
./vfpg.native [XML input file] [C output file]
The Makefile can also launch tests.
It is also possible to test the Clight generator using the command:
This command will use
CompCert to generate a Clight version of the file
common-c-code/common_flight_plan.c (saved in the file
generated/CommonFP.v). This file is then converted into C code using the
CompCert printer. The result is written in
Description of folders in the project
common-c-code: The common C code for all the flight plan.
docs: The documentation of the project.
frontend: The frontend Ocaml code for the generator.
generated: The Clight file generated with
clightgen. They are stored as they are used in Coq proofs.
ocaml-generator: The Ocaml code of the previous Flight Plan generator of Paparazzi. This code has been extracted from the whole Paparazzi project for testing purpose. In this folder you can find:
- The folder
srccontaining the main source of the previous generator.
- The folder
src_paparazzithat contains all the libraries needed by the generator.
- The script
run.shthat build and run the generator. It will produce in the
outfolder the C flight plan corresponding to
- The folder
src: All the Coq sources of the generator.
tests: The scripts that launch all tests.
tools: Script use during the build process.
Generate Coq Doc
make doc firefox html/toc.html
New Features added
- Forbidden deroute: Possibility to forbidden certain deroute between blocks.
- Height added to the oval (not added everywhere)
Currently, all the features are not implemented and some modifications from the original flight plan generator has been made:
- When a C code is used for a condition, we considered that the execution return an integer value, evaluated has a boolean (returned value are converted into 0 or 1 only).
- The parameter
last_wpis a string.
- Exceptions and forbidden deroute in loop are ignored.
on_enteroption do not work for the first block.
- If the next block is forbidden then the execution state do not change.
- If there is a exception but the block is forbidden, then no deroute will occur.
- The field
execmust an instruction.
- The constant
NB_BLOCKhave been replaced by the a constante variable.
- When there is a deroute, the current stage it is not change. In the case of a return, we jump in the deroute stage.