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.
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)
- Menhir (tested with version 20220210)
- Coq-Mathcomp-SSReflect (tested with version 1.15.0)
The dependencies can be installed using OPAM (version 2.0 or later):
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq ocamlbuild xml-light menhir coq-mathcomp-ssreflect
To generate the documentation, the package graphviz
must be installed:
sudo apt install graphviz
Using the Generator
The project needs the source of Paparazzi and CompCert@8d21a7fa. 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 description of the build process is described here
The generator can then be used with the following command:
export PAPARAZZI_HOME=`pwd`/paparazzi
./vfpg.native [XML input file] [C output file]
The Makefile can also launch tests.
make tests
All the tests available are described here
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 withclightgen
. They are stored as they are used in Coq proofs. Currently, it only contains CommonFP that is the Clight code ofcommon-c-code/common_flight_plan.c
. This file has been modified to use the functioncreate_ident
used for the verification,arbitrary_ident
for the definition ofnav_init_stage
function and the variable_t'1
has been replaced from a specific positive value (128) to#"t'1
. -
ocaml-generator
: The Ocaml code of the previous Flight Plan generator of Paparazzi. This code has been extracted from the whole Paparazzi project and slightly modified for testing purpose (see here for the list of the modifications). 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. 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 Flight Plan Generator
This new Coq Flight Plan generator is based on the previous paparazzi generator. It supports almost all the same features and brings some new features.
New Features added
- Forbidden deroute: Possibility to forbid certain deroute between blocks in order to prevent unwanted change (for example passing from a block where the drone flies to a block where the engines are stopped).
- The field
on_enter
andon_exit
has been added for the blocks to specify specific code to execute when entering or leaving a block. - The
height
field has been added for theoval
stage. - An error is raised if a flight plan contains more than 256 blocks or stages.
Modification of the generated C code
Some minor modification to the generated code has been made to simplify the proof.
- When there is a
deroute
, the following stage is stored as the last stage. In the case of areturn
, we then jump to the next stage instead of the samederoute
stage. - The
case
after thedefault
in the stage switch has been removed as it not modifies the behavior of the flight plan. - A
SetNavStage
instruction has been added after theend_while
label to ensure that thenav_stage
variable contains the correct stage id. - A constant variable
nb_block
is generated instead of the macro constantNB_BLOCK
.
Current Limitations
Currently, the generator as some limitations and known issues:
- 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_wp
is a string. - Exceptions and forbidden deroute in loops are ignored.
- If the next block is forbidden then the execution state does not change. In theory, a warning should be raised in this case.
- If there is an exception but the block is forbidden, then no deroute will occur.
- The field
exec
must be an instruction.
Future works
- Add a verified parser in Coq using menhir.
- Prove that the
on_enter
andon_enter
are always executed when entering or leaving a block. - Generate a new
common_flight_plan.c
file from the modified version ofCommonFP.v
. The Coq file is used to verify the semantics preservation theorem. - Add a warning for the exceptions with deroute that can be forbidden.
- Prove that the errors detection always work for forbidden deroute.
- Reduce the amount of modifications in the preprocessing:
- Verify that the transformation of the
for
loop into awhile
loop is correct. - Generate and verify the variables defined by the user.
- Verify that the transformation of the
- Fix limitations problems
- Remove the
NB\_BLOCK
and block name
More information about Paparazzi
To have information about Paparazzi, go directly on the website or on the GitLab project.