--- layout: fc_discuss_archives title: Message 83 from Frama-C-discuss on October 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Timed properties



Hi,

 > Thank your for info about the ongoing plugin. It would be very
 > interesting to check new release. Is there a chance to look on it now,
 > just to understand, how the integration is implemented.

If you have a CVS access to Frama-C, then a runnable version of the plug-in is 
include (but requires the installation of LTL2BA tool : 
http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/download.php).

If you don't have CVS access, I can try to sent you a partial release of the 
current CVS version.


> Well, my original intent is to estimate how far Frama-C from my view on "perfect"
> software certification tool which could include:
> 
> * multiple aspect-like high level models of the distributed software
> * the way to verify models consistency
> * the way to check model properties
> * the method to express various resources like time, memory and so on.
> * the support for runtime checking some of the assumptions

In my opinion, its a very good idea with a lot of perspectives. This way is also 
the one that I plan to follow in the context of QoS in sensor networks. Hence, 
if you want to exchange some ideas, you're welcome.

Nicolas.
-------------- section suivante --------------
Une pi?ce jointe non texte a ?t? nettoy?e...
Nom: nicolas_stouls.vcf
Type: text/x-vcard
Taille: 482 octets
Desc: non disponible
Url: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081020/48bb98d7/nicolas_stouls.vcf