Seminar details

Seminar Room 1, ground floor (Building IMAG)

2 March 2017 - 14h00
« From Frama-C to Lustre »
by Loïc Correnson from CEA - Equipe LIST

Abstract: The Frama-C platform is well equipped to prove functional and robustness properties of C functions, thanks to ACSL specification language and the mature WP and EVA plug-ins.
However, ACSL is not well suited for specifying (temporal) properties of reactive-synchronous programs written in C. On the contrary, Lustre is a perfect language to write observers and specify such properties. But not all reactive programs comes from an original Lustre/Scade program.
This talk presents a new Frama-C plug-in that combines the public API of EVA and WP plug-ins to extract a Lustre model from a synchronous, reactive program written in C. It also presents how this plugin is used to specify and prove properties written in Lustre on a real-world control-command software.

Contact | Site Map | Site powered by SPIP 4.2.8 + AHUNTSIC [CC License]

info visites 3967626