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: nicolas.stouls at insa-lyon.fr (Nicolas Stouls)
  • Date: Mon Oct 20 11:01:09 2008
  • In-reply-to: <1224491260.29534.13.camel@localhost.localdomain>
  • References: <1224314136.21312.10.camel@localhost.localdomain> <48FC2F68.3010206@inria.fr> <48FC3C6B.5090704@insa-lyon.fr> <1224491260.29534.13.camel@localhost.localdomain>
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