VFPG
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.
Dependencies
- 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. The sources must be modified and compiled in order to use the generator. These steps can be easily retrieved with the following script.
./configure
The generator can then be built using the Makefile.
make build
The generator can then be used with the following command:
./vfpg.native [XML input file] [C output file]
The Makefile can also launch tests.
make tests
It is also possible to test the Clight generator using the command:
make CommonFP
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 out/common_flight_plan.h
file.
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 withclightgen
. 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
src
containing the main source of the previous generator. - The folder
src_paparazzi
that contains all the libraries needed by the generator. - The script
run.sh
that build and run the generator. It will produce in theout
folder the C flight plan corresponding toexamples/new_features.xml
.
- 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)
Current Limitations
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_wp
is a string. - Exceptions and forbidden deroute in loop are ignored.
on_enter
option 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
exec
must an instruction. - The constant
NB_BLOCK
have 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.
More information about Paparazzi
To have information about Paparazzi, go directly on the website or on the GitLab project.