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] Timed properties

  • Subject: [Frama-c-discuss] Timed properties
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
  • Date: Sat Oct 18 12:30:12 2008
  • References: <1224314136.21312.10.camel@localhost.localdomain>
Hi!

>I'm going to try to build some extended example of frama-c with proof of
>LTL properties, probably realtime properties, and probably some runtime
>check integration. Also I'd like to build an example proof of validation
>of the code and model, say validation for an automata model.

>As far as I see now I should extend axioms and write some logic as well.

>Do you think it's something doable?

The ACSL annotation language does not have any constructions to express
temporal properties. So my opinion, for what it's worth, is that
encoding LTL properties in ACSL with the help of ghost code is probably
doable but is going to require a lot of elbow grease.

Also, if you think about it, the good thing
about ACSL properties as opposed to run-time assertions is that they
can be composed, allowing a modular approach to the difficult problem
of building sizable software that works.
Typically, once the contract for one particular function is defined,
writing the function and proving that the function satisfies the
contract on the one hand and on the other hand writing the calling function,
proving that the precondition of the contract is satisfied at the call site
and that the calling function satisfies its own specification have become
two separate, independent, smaller sub-problems that can even be
assigned to different people. And you know that your program will work
when you put the pieces of the puzzle together!
With run-time assertion checking you can't test the calling function
until you have something to execute for the called function.

Although Frama-C offers the possibility to write ghost code to help
where ACSL alone does not allow to express the desired properties,
when you take this road I am not sure if you can retain the modularity
that makes the approach promising. 

Yes, the first step would be to think about the axioms and logic functions
that express the properties that you are interested in. Do not hesitate 
to show your experiments on this list, everyone would be very interested
and there are experts (not me!) that read it and that will be able to provide
feedback.

Pascal