Formal verification of the Paparazzi autopilot

This project is a fork of Paparazzi UAV autopilot repository (https://github.com/paparazzi/paparazzi). The aim of this project is to verify the pprz_algebra library using Frama-C.

The GitLab project adds ACSL annotations and provides a script to automatically launch Frama-C. Frama-C analyses the code, checks for the absence of RTE (RunTime Errors) and verify some functional properties.

Required software

To run the verification, the following software are required:

  • Frama-C 23.0 (Vanadium)
  • Alt-Ergo 2.4.0
  • CVC4 1.9-prerelease
  • Z3 4.8.6
  • Coq 8.12.2
  • Why3 1.4.0
  • ctags

How to launch the verification process

First, go to the sw/airborne directory:

cd sw/airborne

Update the variable FRAMAC_PREFIX in frama-c-analysis.sh with the path of the directory containing Frama-C binary. Then, launch the script that starts the analysis:

./frama-c-analysis.sh

The WP smoke tests can be enabled with the environment variable SMOKE as follows:

SMOKE=1 ./frama-c-analysis.sh

Quick description of modified files

  • sw/airborne/frama-c-analysis.sh: a shell script that automatically launches the verification using Frama-C.
  • sw/airborne/output-frama-c-analysis.sh: a Python script used by frama-c-analysis.sh to read and analyse the results from Frama-C.
  • sw/airborne/math/pprz_algebra_(int|float|double).(h|c): the mathematical library of Paparazzi that has been verified. These files have been annotated with ACSL.
  • sw/airborne/math/pprz_algebra_(int|float|double)_frama_c.h: files containing definition of predicates, lemmas and logical functions used to verify the absence of RTE in the library.
  • sw/airborne/math/pprz_algebra_float_convert_rmat_frama_c.h: definition of predicates, lemmas and logical functions for the verification of functional properties.
  • sw/airborne/.frama-c/wp/interactive: Coq scripts containing the proof lemmas.
  • sw/airborne/.frama-c/wp/script: WP scripts containing the tactics used to prove some goals.

Verification process

The verification process combines the analysis of the EVA and WP plugins of Frama-C. The EVA plugin requires a program entry point (a main or a function) to start its analysis. The script frama-c-analysis.sh finds automatically all the names of the functions in the library using ctags. Then, verification is launched for every function FUNCTION with the following parameters:

  • -rte: adds RTE annotations in the code.
  • -no-warn-left-shift-negative: allows left shift for negative values.
  • -eva -lib-entry -main $FUNCTION: launches EVA analysis with $FUNCTION as the entry point. The initial state is determined by the preconditions specified in the contract of the function.
  • -wp-fct $FUNCTION: launches the WP verification with the following options:
    • -wp-cache update: enables and uses cache.
    • -wp-model real+Cast+ref: enables the real model to represent the arithmetic on floating-point numbers. The Cast option enables the usage of cast in the code. Finally, the ref option is used to enable optimization for reference parameters.
    • -wp-prover alt-ergo,cvc4-strings-ce,z3,z3-ce,z3-nobv,coq,tip: adds the different provers needed to verify the goals.
    • -wp-check-memory-model: Insert memory model hypotheses in the function contracts. Necessary as we use the ref memory model.
  • -cpp-extra-args=-I../include: adds the include directory of Paparazzi.
  • -cpp-extra-args=-DFRAMA_C_ANALYSIS: defines a C constant in order to remove certain portions of code that are not supported by Frama-C.

More information about Paparazzi

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

Baptiste Pollien
Baptiste Pollien
PhD Student in Formal Methods

My research interests focus on formal methods applied for UAV Autopilot.

Related