Verimag

Seminar details

Seminar Room 1, ground floor (Building IMAG)
2 March 2017 - 14h00
« From Frama-C to Lustre »
par Loïc Correnson de 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 3.0.25 + AHUNTSIC [CC License]

info visites 776129