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] Using frama-c Mthread plug-in to verify coding patterns of concurrent sw

  • Subject: [Frama-c-discuss] Using frama-c Mthread plug-in to verify coding patterns of concurrent sw
  • From: Oyvind.Teig at autronicafire.no (Teig, Oyvind BIS)
  • Date: Mon, 20 Oct 2014 08:25:48 +0000
Sirs

I presented my problem last year: "Using frama-c to verify coding patterns of concurrent sw" (2July2013), see http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-July/003678.html

I just now read the "Testing of Formal Verification: DO-178C Alternatives and Industrial Experience" (Moy, Ledinot, Delseny, Wiels, Monate) in IEEE Software May/June 2013, where Frama-C was much mentioned. So I went to the present pages and discovered Mthread: http://frama-c.com/mthread.html and http://frama-c.com/download/frama-c-mthread-manual.pdf

I see one then need to instrument the user C code with stubs. I have some questions:


1.       Could any of the mtread macros be used for synchronous CSP-type channels (occam, golang) that "yield" when it's not possible to proceed. (I use "yield" instead of "block", see http://www.teigfam.net/oyvind/home/technology/092-not-so-blocking-after-all/ )

2.       What about buffered CSP-type channels that turn to synchronous semantics when they are full (golang)?

3.       What about my XCHAN (see 2July2013 ref above), where two channels are used (data and ready), but they have to be used correctly in a pattern. It's not like a semaphore pattern, but the XCHAN pattern. So it's special I assume?

4.       Is Mtread an active SW, being supported and worked on, or is it presented "as is". It's (c) 2011-2012 CEA LIST

Med vennlig hilsen / Best regards
?yvind Teig
Senior utviklingsingeni?r, siv.ing. / Senior Development Engineer, M.Sc.
Autronica Fire and Security AS
Research and Development
UTC Building and Industrial Systems
Phone: +47 735 824 68
E-mail:  oyvind.teig at autronicafire.no<mailto:oyvind.teig at autronicafire.no>
www.autronicafire.no<http://www.autronicafire.no/>
www.teigfam.net/oyvind/home/<http://www.teigfam.net/oyvind/home/> (Also work-related)

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20141020/4272ddc7/attachment.html>