Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.


[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Value Analysis plugin versus Simulation Tool


  • Subject: [Frama-c-discuss] Value Analysis plugin versus Simulation Tool
  • From: rovedy at ig.com.br (Rovedy Aparecida Busquim e Silva)
  • Date: Fri, 25 Jan 2013 10:41:26 -0300

Hello,


We applied the Value Analysis plugin in a case study based on an embedded
aerospace control software.



The case study considered two scenarios where the sensors measurements are
treated in different ways.



The first scenario considered the maximum range of values accepted by the
sensors (Frama C float interval and Frama C interval functions). The
analysis was performed smoothly and gave valid ranges of values for the
variables.



In the second scenario it was adopted a different approach. It was used all
the values of sensors measurements obtained from a flight simulation record
(ascii file) as input to the Value Analysis/Frama-, i. e., the Frama C
interval functions do not were used. As a result, the analysis gave
variables profiles very similar to the simulation ones.



Is valid the second scenario? Can the Value Analysis/Frama-C be used as a
tool for simulation?


Best regards
Nanci, Rovedy and Luciana
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130125/04da5a21/attachment.html>