--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on July 2013 ---
[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/1 Teig, Oyvind              CCS <Oyvind.Teig at autronicafire.no>:

>
> ?        Is it possible to set up an ACSL specification that would be able
> to verify that certain combinations of local state variables _now_ and
> certain other combinations _later_ on will sooner or later arrive?
>
> ?        Even more than that: I will need to verify more than two steps!
>
> www.teigfam.net/oyvind/home/ (also work-related)

I think that you might be interested by the Aora? plug-in
(http://frama-c.com/aorai.html and
http://amazones.gforge.inria.fr/aorai/), that generate ACSL
specifications from an automaton describing the sequences of function
calls that are authorized for the program. Be aware though that it is
still a quite experimental plug-in. Some extensions might be devised
inside the FP7 project Stance and the ITEA project OpenETCS, but as
usual, we'd be happy to start further collaborations around the
subject.

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