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] Using frama-c to verify coding patterns of concurrent sw

Hello,

2013/7/2 Teig, Oyvind              CCS <Oyvind.Teig at autronicafire.no>:
> Q1. What is not supported?
>
> It looked like the "safety" (state) part is present, not the temporal things. Which would probably be ok. I am only after verifying that a software pattern is kept.
>

More precisely, in temporal logic terms, you can use Aora? to solve
reachability problems (i.e. that you will always be in a given state
at the end of the execution of a program), but not to solve liveness
problems. Moreover, Aora? can only consider programs that do
terminate: the instrumentation will not work in presence of infinite
loops.
In addition, Aora? cannot handle function pointers. Other than that,
the main shortcoming is that it has not been tested on very complex
specifications, especially for the extended ya syntax.

> Between every state that I want to check, any number of calls (=schedule) may be done, and they would side effect into the preconditions of the test. Some message would arrive on a channel (a call into the function (process)) or some timeout (the same) would cause the state changes that will trigger some code that I want to verify. A temporal requirement may be "eventually", it must be possible to detect if bad coding causes entering a certain state as not possible, i.e. "not eventually".
>
> Q2. Do you think this is possible?

I'm not sure that I completely understand what you have described, but
it looks to be that you're looking at some liveness property (at any
time, whatever happens, the system eventually reaches a good state at
some point somewhere in the future). Thus I'm not too sure that this
is directly feasible with Aora? (but again, maybe I've misunderstood
what you're saying). That said, we have has some success (but
unfortunately never took the time to publish about it, so that I don't
have a reference to point you to) in using Aora? + Value analysis in
"bug finding mode", i.e. to describe a threat scenario with an
automaton and explore with Value the various possible executions paths
until we find some sequence of event that leads to the alarm.

>
> Q3. What's the state of the Promela interface?

The promela interface is barely maintained at this point. The
preferred input nowadays for Aora? is a ya automaton. My colleague
S?bastien Bardin and myself have proposed an internship to revisit the
LTL input, as well as proposing (very) partial solutions for handling
infinite loops and liveness properties
(http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:positions#internships),
but we have not found anyone. If you (or anyone on this list) know a
student that would be interested, we'd be happy to hear about em.

--
E tutto per oggi, a la prossima volta
Virgile