Lustre

Not used with current Paparazzi Versions anymore.

Lustre implementation of critical code
As robustness is the priority of the Paparazzi project, a hardware/software fail-safe is implemented on AVR and Classix autopilots by processing all critical code on a dedicated microcontroller, independent from the navigation, communication, and payload processor. As the role of this processor is absolutely critical, source code must be certified. Typical industry practice is to certify only methods of programming, not source code. In the Paparazzi project, we make this code safer by writing clear specifications in reference to which we can prove safety properties. The operational code in C is then automatically generated from these specifications.

Lustre : a synchronous declarative programming language

Lustre is a data-flow programming language, which means that all precedent values of the variables are known. Lustre is also a synchronous language, meaning all instructions are considered to be executed simultaneously.

Lustre functions are referred to as nodes, operating on input streams to compute the output streams. A Lustre program has a cyclic behavior - on the n^th execution cycle of the program, all involved streams take their n^th value. A node defines one or several output parameters as functions of one or more input parameters.

Operators used to write statements in a node operate on the entire stream. This means that if you write X=Y, then the n^th value of X will always be equal to the n^th value of Y, for all n.

Read more at Verimag.imag.fr

Lustre modelling of all variables

The natural way to write proven code is to write Lustre statements between state variables. The problem is that Lustre proposed types are limited to bool, int and float. To produce code for a µC, we had to specify custom types used on the µC, such as uint16_t (unsigned 16-bits integer) or uint8_t (unsigned 8-bits integer).
As defining custom types is not possible in Lustre, we use the natural Lustre types, specifying how our types can be represented with natural types. We then redefine common operators to preserve modularity. For instance, uint16_t is a modular integer type. This method allows simulations of the code with Lustre tools (luciole for example).

Lustre generated code can not be used on the µC. Our definitions preserve modularity on state variables, but the internal variables managed by Lustre generated code are not aware of µC limitations. Consequently, generated code cannot be executed on a real µC. For instance, some tests are always true or false due to range limitations of data types, and ignored by the code generator.

Lustre specifications with C types

From a practical standpoint, we prefer to use only C-defined types. Lustre can manage this type, but every operator must be defined as Lustre can not create operators for unknown types. This method gives good results with generated code that is ready to execute on the µC but there is a problem. As Lustre is not aware of C types, the Lustre tools cannot prove anything in this form and any potential benefits are lost.

Separating the proof code from the execution code

The method we use combines the best attributes of the above mentioned strategies. We write the operational code using C-defined types, which gives us ready-to-use code, and the proof is done only with Lustre code. The only remaining work is to ensure that the C-code and the Lustre-code of the operators are equivalent, a trivial task since operators are very simple functions/nodes (usually defined by macros in C).

How to use the Lustre-generated code

Currently only PPM decoding is implemented using the Lustre code. This Lustre description of PPM decoding provides safety by defining precisely what type of PPM frame is to be accepted and what should be rejected. Hardware testing has proven that Lustre implemented PPM decoding outperforms hand written C implemented decoding as we occasionally see valid PPM frames lost with hand written code, but not with Lustre code.

Lustre generated code is not yet entirely generic. It works only with the CockpitMM R/C transmitter used during our hardware tests. Efforts are underway to make it selectable from the configuration file. If you use the CockpitMM transmitter you can use Lustre code - simply go to the lustre directory in Paparazzi tree, compile, and upload the program to the µC.

cd $PAPARAZZI_HOME/sw/airborne/fly_by_wire/lustre_version
make clean_all
make load