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 with clightgen. They are stored as they are used in Coq proofs. Currently, it only contains CommonFP that is the Clight code of common-c-code/common_flight_plan.c. This file has been modified to use the function create_ident used for the verification, arbitrary_ident for the definition of nav_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 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 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 and on_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 the oval 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 a return, we then jump to the next stage instead of the same deroute stage.
• The case after the default in the stage switch has been removed as it not modifies the behavior of the flight plan.
• A SetNavStage instruction has been added after the end_while label to ensure that the nav_stage variable contains the correct stage id.
• A constant variable nb_block is generated instead of the macro constant NB_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 and on_enter are always executed when entering or leaving a block.
• Generate a new common_flight_plan.c file from the modified version of CommonFP.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 a while loop is correct.
  • Generate and verify the variables defined by the user.
• 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.