--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on October 2014 ---
[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



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>