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

? ???, 20/10/2008 ? 10:08 +0200, Nicolas Stouls ?????:
> Hi,
> 
> Note that this plug-in is experimental (and its documentation too).
> Hence, if you have any specific problem or question about this plug-in or its 
> usage, don't hesitate to write me.
> 

Thank you all for your answers.

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

and probably more. Logic framework used seems to be generic enough to handle 
this all, but it's not trivial to make this on practice.

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.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 197 bytes
Desc: =?koi8-r?Q?=FC=D4=C1?= =?koi8-r?Q?_=DE=C1=D3=D4=D8?=
	=?koi8-r?Q?_=D3=CF=CF=C2=DD=C5=CE=C9=D1?=
	=?koi8-r?Q?_=D0=CF=C4=D0=C9=D3=C1=CE=C1?=
	=?koi8-r?Q?_=C3=C9=C6=D2=CF=D7=CF=CA?=
	=?koi8-r?Q?_=D0=CF=C4=D0=C9=D3=D8=C0?=
Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081020/8a7035b3/attachment.pgp