Lustre - Revision history

Flixr at 08:06, 1 April 2011

2011-04-01T08:06:23Z

← Older revision		Revision as of 02:06, 1 April 2011
Line 1:		Line 1:
			<span style="color:red">Not used with current Paparazzi Versions anymore.</span>

	'''Lustre implementation of critical code'''<br>		'''Lustre implementation of critical code'''<br>
	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.		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.

Esden at 19:00, 10 March 2011

2011-03-10T19:00:37Z

← Older revision		Revision as of 13:00, 10 March 2011
Line 31:		Line 31:
	make clean_all		make clean_all
	make load		make load

			[[Category:Software]] [[Category:Developer_Documentation]]

SergeLeHuitouze: /* Lustre : a synchronous declarative programming language */

2007-07-18T12:00:33Z

Lustre : a synchronous declarative programming language

← Older revision		Revision as of 06:00, 18 July 2007
Line 7:		Line 7:
	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<sup>th</sup> execution cycle of the program, all involved streams take their n<sup>th</sup> value. A node defines one or several output parameters as functions of one or more input parameters.		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<sup>th</sup> execution cycle of the program, all involved streams take their n<sup>th</sup> 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<sup>th</sup> value of X will always be equal to the n<sup>th</sup> value of Y, ~~and so on~~.		Operators used to write statements in a node operate on the entire stream. This means that if you write X=Y, then the n<sup>th</sup> value of X will always be equal to the n<sup>th</sup> value of Y, for all n.

	Read more at [http://www-verimag.imag.fr/SYNCHRONE/index.php?page=lang-design Verimag.imag.fr]		Read more at [http://www-verimag.imag.fr/SYNCHRONE/index.php?page=lang-design Verimag.imag.fr]

	== Lustre modelling of all variables ==		== Lustre modelling of all variables ==

HectoPascal: /* How to use the Lustre-generated code */

2007-01-16T14:09:09Z

How to use the Lustre-generated code

← Older revision		Revision as of 08:09, 16 January 2007
Line 26:		Line 26:
	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.		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 ~~genetrated~~ 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.		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		cd $PAPARAZZI_HOME/sw/airborne/fly_by_wire/lustre_version
	make clean_all		make clean_all
	make load		make load

HectoPascal: /* Lustre modelling of all variables */

2007-01-16T14:08:41Z

Lustre modelling of all variables

← Older revision		Revision as of 08:08, 16 January 2007
Line 15:		Line 15:
	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).		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 ~~executes~~ 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 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 ==		== Lustre specifications with C types ==

Jeremy at 08:33, 10 December 2006

2006-12-10T08:33:02Z

← Older revision		Revision as of 02:33, 10 December 2006
Line 1:		Line 1:
	'''Lustre implementation of critical code'''<br>		'''Lustre implementation of critical code'''<br>
	~~Robustness~~ is the priority of the Paparazzi project~~. A~~ hardware/software fail-safe is ~~utilized~~ on AVR and Classix autopilots~~, locating~~ all critical code on a ~~separate~~ dedicated microcontroller. 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.		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 : a synchronous declarative programming language ==

Jeremy at 08:21, 10 December 2006

2006-12-10T08:21:47Z

New page

'''Lustre implementation of critical code''' 
Robustness is the priority of the Paparazzi project. A hardware/software fail-safe is utilized on AVR and Classix autopilots, locating all critical code on a separate dedicated microcontroller. 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 nth execution cycle of the program, all involved streams take their nth 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 nth value of X will always be equal to the nth value of Y, and so on.

Read more at [http://www-verimag.imag.fr/SYNCHRONE/index.php?page=lang-design 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 executes 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 genetrated 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