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 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.
• 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.