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 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 easily support other 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 project needs the source of Paparazzi and CompCert@9d3521b4. The sources must be modified and compiled in order to use the generator. These steps can be easily retrieved with the following script.
The generator can then be built using the Makefile.
The description of the build process is described here
The generator can then be used with the following command:
./vfpg.native [XML input file] [C output file]
The Makefile can also launch tests.
All the tests available are described here
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 files 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. A description of these files can be found here.
tests: The scripts that launch all tests described here.
tools: Script use during the build process
Generate Coq Doc
make doc firefox html/toc.html
A description of all Coq files can be found here.
New Features added
- Forbidden deroute: Possibility to forbid certain deroute between blocks.
- The filed
on_exithas been added for the blocks.
- Height added to the oval (not added everywhere)
- Return an errors if a flight plan contains more thant 256 blocks or stages.
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 as a boolean (returned value are converted into 0 or 1 only).
- The parameter
last_wpis a string.
- Exceptions and forbidden deroute in loops are ignored.
on_enteroption do not work for the first block.
- If the next block is forbidden then the execution state does not change.
- If there is an exception but the block is forbidden, then no deroute will occur.
- The field
execmust be an instruction.
- The constant
NB_BLOCKhas been replaced by constant variables.
- When there is a deroute, the current stage is not changed. In the case of a return, we jump in the deroute stage.
- TODO: The proof uses a simplified version of the whole CommonFP.