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.
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
How to launch the verification process
First, go to the
Update the variable
with the path of the directory containing Frama-C binary. Then,
launch the script that starts the analysis:
The WP smoke tests can be enabled with the environment variable
SMOKE as follows:
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.shto 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.
The verification process combines the analysis of the
WP plugins of Frama-C. The
EVA plugin requires a program entry point (a
main or a function) to
start its analysis. The script
automatically all the names of the functions in the library using
ctags. Then, verification is launched for every 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
$FUNCTIONas 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
realmodel to represent the arithmetic on floating-point numbers. The
Castoption enables the usage of cast in the code. Finally, the
refoption 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
-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.