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