--- layout: fc_discuss_archives title: Message 83 from Frama-C-discuss on October 2008 ---
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