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)

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.

./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:

./vfpg.native [XML input file] [C output file]

The Makefile can also launch tests.

make tests

All the tests available are described here

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 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 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 the out folder the C flight plan corresponding to examples/new_features.xml.
• 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_enter and on_exit has 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.

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 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.
• on_enter option 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 exec must be an instruction.
• The constant NB_BLOCK has 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.

More information about Paparazzi

To have information about Paparazzi, go directly on the website or on the GitLab project.