<div dir="ltr"><div class="gmail_default" style=""><font face="verdana, sans-serif">Dear Andrew,</font></div><div class="gmail_default" style=""><font face="verdana, sans-serif"><br></font></div><div class="gmail_default" style=""><font face="verdana, sans-serif">It's great to see a move toward formal verification for RTEMS.</font></div><div class="gmail_default" style=""><font face="verdana, sans-serif"><br></font></div><div class="gmail_default" style=""><font face="verdana, sans-serif">From our side (TU Dortmund in Germany and the University of Twente in the Netherlands), we recently adopted Frama-C to verify ICPP and MrsP. A potential deadlock is successfully identified, and a remedy is provided. The result will be presented in EMSOFT this year (<a href="https://ieeexplore.ieee.org/document/9852753/">https://ieeexplore.ieee.org/document/9852753/</a>), and the verification framework is publicly released here: <a href="https://github.com/tu-dortmund-ls12-rt/Resource-Synchronization-Protocols-Verification-RTEMS">https://github.com/tu-dortmund-ls12-rt/Resource-Synchronization-Protocols-Verification-RTEMS</a></font></div><div class="gmail_default" style=""><font face="verdana, sans-serif"><br></font></div><div class="gmail_default" style=""><font face="verdana, sans-serif">Due to the double-blind review process, I cannot chime in earlier in this thread. Today earlier I have seen your patches regarding the chapter you proposed. I wonder if you could take our contribution into account when you organize the chapter? </font></div><div class="gmail_default" style=""><font face="verdana, sans-serif">A preprint can be found <a href="https://www.researchgate.net/publication/362599165_Formal_Verification_of_Resource_Synchronization_Protocol_Implementations_A_Case_Study_in_RTEMS">here</a>. (The corresponding ticket will be prepared, and the patch together with a test case will be submitted)<br></font></div><div class="gmail_default" style=""><font face="verdana, sans-serif"><br></font></div><div class="gmail_default" style=""><font face="verdana, sans-serif">Best,<br>Kuan-Hsun</font></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Jul 22, 2022 at 12:37 PM <a href="mailto:Andrew.Butterfield@scss.tcd.ie">Andrew.Butterfield@scss.tcd.ie</a> <<a href="mailto:Andrew.Butterfield@scss.tcd.ie">Andrew.Butterfield@scss.tcd.ie</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div class="msg8166093248812141665">





<div lang="EN-IE" style="overflow-wrap: break-word;">
<div class="m_8166093248812141665WordSection1">
<p class="MsoNormal"><span>Dear RTEMS developers,<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>thanks for the feedback below - I want to wrap this up and move to the next step.<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>I propose to produce a complete draft of a formal methods section for the Software Engineering manual in rtems-docs<u></u><u></u></span></p>
<p class="MsoNormal"><span>This will add a "Formal Verification" section just after the existing "Test Framework" section.<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>This will allow developers to get a much better idea of what is proposed, and for me to get feedback.<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>For now, the section will state clearly at the start that this is a proposal and that the tooling and resources it describes<u></u><u></u></span></p>
<p class="MsoNormal"><span>won't yet be available in RTEMS proper.
<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>Files likely to be modified in rtems-docs:<u></u><u></u></span></p>
<p class="MsoNormal"><span>eng/index.rst<u></u><u></u></span></p>
<p class="MsoNormal"><span>common/refs.bib<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>I'll add in  eng/formal-verification.rst<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>I'll then submit patches for review in the usual way.<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span>Regards,<u></u><u></u></span></p>
<p class="MsoNormal"><span>  Andrew<u></u><u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<div>
<div>
<div>
<p class="MsoNormal">--------------------------------------------------------------------<br>
Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204<br>
Lero@TCD, Head of Software Foundations & Verification Research Group<br>
School of Computer Science and Statistics,<br>
Room G.39, O'Reilly Institute, Trinity College, University of Dublin<br>
                         <a href="http://www.scss.tcd.ie/Andrew.Butterfield/" target="_blank">http://www.scss.tcd.ie/Andrew.Butterfield/</a><br>
--------------------------------------------------------------------<u></u><u></u></p>
</div>
</div>
</div>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<p class="MsoNormal"><span><u></u> <u></u></span></p>
<div>
<div>
<p class="MsoNormal">On 11/07/2022, 12:43, "devel on behalf of <a href="mailto:Andrew.Butterfield@scss.tcd.ie" target="_blank">
Andrew.Butterfield@scss.tcd.ie</a>" <<a href="mailto:devel-bounces@rtems.org" target="_blank">devel-bounces@rtems.org</a> on behalf of
<a href="mailto:Andrew.Butterfield@scss.tcd.ie" target="_blank">Andrew.Butterfield@scss.tcd.ie</a>> wrote:<u></u><u></u></p>
</div>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<div>
<p class="MsoNormal">On 6 Jul 2022, at 20:07, Gedare Bloom <<a href="mailto:gedare@rtems.org" target="_blank">gedare@rtems.org</a>> wrote:<u></u><u></u></p>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
<div>
<div>
<p class="MsoNormal" style="margin-bottom:12pt">On Sun, Jul 3, 2022 at 7:49 PM Chris Johns <<a href="mailto:chrisj@rtems.org" target="_blank">chrisj@rtems.org</a>> wrote:<u></u><u></u></p>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<p class="MsoNormal" style="margin-bottom:12pt"><br>
On 2/7/2022 12:59 am, Andrew Butterfield wrote:<u></u><u></u></p>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<p class="MsoNormal" style="margin-bottom:12pt">On 1 Jul 2022, at 00:59, Chris Johns <<a href="mailto:chrisj@rtems.org" target="_blank">chrisj@rtems.org</a><br>
<mailto:<a href="mailto:chrisj@rtems.org" target="_blank">chrisj@rtems.org</a>>> wrote:<u></u><u></u></p>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<p class="MsoNormal" style="margin-bottom:12pt"><br>
On 28/6/2022 11:09 pm, <a href="mailto:Andrew.Butterfield@scss.tcd.ie" target="_blank">Andrew.Butterfield@scss.tcd.ie</a><br>
<mailto:<a href="mailto:Andrew.Butterfield@scss.tcd.ie" target="_blank">Andrew.Butterfield@scss.tcd.ie</a>> wrote:<u></u><u></u></p>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<p class="MsoNormal">Dear RTEMS Developers,<br>
<br>
While the validation tests from the RTEMS pre-qualification activity are<br>
now merged into the RTEMS master, the work done in investigating and<br>
deploying formal methods techniques is not yet merged.<br>
<br>
The activity had two main phases: a planning phase (Nov 2018-Oct 2019)<br>
that explored various formal techniques, followed by an execution phase<br>
(Oct 2019-Nov 2021) that then applied selected techniques to selected<br>
parts of RTEMS. Some discussions occurred with the RTEMS community<br>
via the mailings lists over this time. A short third phase (Nov 2021 - Dec 2021)<br>
then reported on the outcomes. Each phase resulted in a technical report.<br>
<br>
The key decision made was to use Promela/SPIN for test generation, and<br>
to apply it to the Chains API, the Event Manager, and the SMP scheduler<br>
thread queues. This involved developing models in the Promela language<br>
and using the SPIN model-checker tool to both check their correctness<br>
and to generate execution scenarios that could be used to generate tests.<br>
Tools were developed using Python 3.8 to support this. Initial documentation<br>
about tools and how to use them was put into the 2nd phase report.<u></u><u></u></p>
</blockquote>
<p class="MsoNormal" style="margin-bottom:12pt"><br>
Congratulations for the work and results you and others have managed to achieve.<br>
It is exciting to see this happening with RTEMS and being made public.<br>
<br>
<u></u><u></u></p>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<p class="MsoNormal">We now come to the part where we explore the best way to integrate this<br>
into RTEMS. I am proposing to do this under the guidance of Sebastian Huber.<br>
<br>
The first suggested step is adding in new documentation to the RTEMS<br>
Software Engineering manual, as a new Formal Methods chapter. This would<br>
provide some motivation, as well as a "howto".<br>
<br>
I assume that I would initially describe the proposed changes using the patch<br>
review process described in the section on Preparing and Sending Patches in<br>
the User Manual.<br>
<br>
How do you feel I should best proceed?<u></u><u></u></p>
</blockquote>
<p class="MsoNormal"><br>
It is hard for me to answer until I understand what is being submitted and who<br>
maintains it? I am sure you understand this due to the specialised nature of the<br>
work.<u></u><u></u></p>
</blockquote>
<p class="MsoNormal"><br>
Indeed, I quite agree.  I have some short answers below, with suggestions.<u></u><u></u></p>
</blockquote>
<p class="MsoNormal" style="margin-bottom:12pt"><br>
Thanks.<u></u><u></u></p>
</blockquote>
<p class="MsoNormal" style="margin-bottom:12pt">+1<br>
<br>
<u></u><u></u></p>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<p class="MsoNormal" style="margin-bottom:12pt"><u></u> <u></u></p>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<p class="MsoNormal"><br>
What will be submitted, ie SPIN files, scripts, etc?<u></u><u></u></p>
</blockquote>
<p class="MsoNormal" style="margin-bottom:12pt"><br>
Promela/SPIN model files (ASCII text, C-like syntax)<br>
C template files (.h,.c) to assist test code generation<br>
YAML files to provide a mapping from model concepts to RTEMS C test code<br>
python scripts to automate the test generation<br>
Documentation - largely RTEMS compliant sphinx sources (.rst)<br>
<br>
<u></u><u></u></p>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<p class="MsoNormal"><br>
Where are you looking to add these pieces?<u></u><u></u></p>
</blockquote>
<p class="MsoNormal"><br>
Everything except the documentation could live in a top-level folder ('formal')<br>
in rtems-central.<br>
In fact there is no particular constraint from my perspective for where they can go.<u></u><u></u></p>
</blockquote>
<p class="MsoNormal" style="margin-bottom:12pt"><br>
Using rtems-central is fine.<u></u><u></u></p>
</blockquote>
<p class="MsoNormal">Do they require anything currently located in rtems-central? Are the<br>
models or YAML files related to the current specification files? I<br>
know I'm guilty of not spending the time yet to deeply learn<br>
rtems-central, but I would like to know that these files will fit<br>
within that repo as it currently is intended to operate.<u></u><u></u></p>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<p class="MsoNormal">At the moment there is nothing in rtems-central directly related to this. All the python<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">scripts there support the tools/specs that Sebastian and colleagues developed.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">I can see a new top-level script being added here to support the formal stuff.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal">It is possible that we might introduce a new specification item that integrates<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">in with the spec system that is used to trigger the Spin test generations. I'll discuss the<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">best wat to do this with Sebastian.<u></u><u></u></p>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<p class="MsoNormal" style="margin-bottom:12pt"><u></u> <u></u></p>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<div>
<div>
<p class="MsoNormal"><br>
RSB should be taught how to build the necessary host tools to run Promela/SPIN.<u></u><u></u></p>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<p class="MsoNormal">Spin is open source under a BSD 3-clause license, available from <a href="http://spinroot.com" target="_blank">spinroot.com</a>,<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">and also via <a href="https://github.com/nimble-code/Spin" target="_blank">https://github.com/nimble-code/Spin</a>. It is written in C and has very few<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">dependencies. I'm not sure what is involved in adding it to the RSB, but I guess <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">Sebastian will know. <u></u><u></u></p>
</div>
<div>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<div>
<div>
<p class="MsoNormal" style="margin-bottom:12pt"><u></u> <u></u></p>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<p class="MsoNormal">The plan would be to add the pertinent parts of our project documentation into<br>
new chapters<br>
in the RTEMS software engineering manual. So that would be eng/ in the<br>
rtems-docs repo.<u></u><u></u></p>
</blockquote>
<p class="MsoNormal" style="margin-bottom:12pt"><br>
Great.<u></u><u></u></p>
</blockquote>
<p class="MsoNormal">+1<br>
<br>
A new section in the eng should be suitable. I would actually<br>
recommend using<br>
<a href="https://docs.rtems.org/branches/master/eng/test-framework.html#" target="_blank">https://docs.rtems.org/branches/master/eng/test-framework.html#</a> as a<br>
good example.<u></u><u></u></p>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<p class="MsoNormal">Thanks - that very helpful. I think our section should immediately follow that one.<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal">All we need now is a suitable title.  "Formal Test Framework"?<u></u><u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:12pt"><u></u> <u></u></p>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<div>
<div>
<p class="MsoNormal" style="margin-bottom:12pt"><u></u> <u></u></p>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<p class="MsoNormal">How is the verification run against the code? Do we manage regression testing<br>
and is that even possible?<u></u><u></u></p>
</blockquote>
<p class="MsoNormal"><br>
The python scripts basically run SPIN in such a way as to generate scenarios<br>
that model<br>
correct behaviour which then get turned into standard RTEMS test programs. These all<br>
get added into a new testsuite in the rtems repo (testsuites/models, say).<br>
They are properly integrated into the RTEMS test system, so get built and run by<br>
waf.<br>
This is similar to how the tests generated by Sebastian in testsuites/validation<br>
are handled.<br>
<br>
>From the perspective of a user that works out of <a href="http://git.rtems.org/rtems" target="_blank">git.rtems.org/rtems</a><br>
<<a href="http://git.rtems.org/rtems" target="_blank">http://git.rtems.org/rtems</a>>,<br>
there will be no obvious impact - just some extra tests in among the ones that<br>
already exist.<u></u><u></u></p>
</blockquote>
<p class="MsoNormal" style="margin-bottom:12pt"><br>
Thanks and this make sense.<br>
<br>
<u></u><u></u></p>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<p class="MsoNormal" style="margin-bottom:12pt"><u></u> <u></u></p>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<p class="MsoNormal"><br>
I hope my simple questions highlight a lack of understand on how this works and<br>
how we maintain it and use it once integrated.<u></u><u></u></p>
</blockquote>
<p class="MsoNormal"><br>
I intend to continue to work and maintain this for the foreseeable future. I<br>
would hope as this beds in that other Promela/SPIN users out there will also get<br>
more involved over time.<u></u><u></u></p>
</blockquote>
<p class="MsoNormal" style="margin-bottom:12pt"><br>
Thank, it is appreciated.<u></u><u></u></p>
</blockquote>
<p class="MsoNormal">I'm also interested in tracking this, and I might be able to go after<br>
some resources on the US side. I'll be in touch on that later, but if<br>
any US users are tracking this too, or you know any with interest, I'd<br>
love to talk about it.<u></u><u></u></p>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<p class="MsoNormal">Indeed  - that would be good. <u></u><u></u></p>
</div>
<div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
<div>
<p class="MsoNormal" style="margin-bottom:12pt">Andrew <u></u><u></u></p>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<div>
<div>
<p class="MsoNormal" style="margin-bottom:12pt"><u></u> <u></u></p>
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<blockquote style="margin-top:5pt;margin-bottom:5pt">
<p class="MsoNormal">It is expected that Promela models will be as static as the corresponding APIs.<br>
They capture the specified behaviour of API calls, not their detailed<br>
implementation.<br>
<br>
The python scripts should also be fairly stable, although I can see some<br>
tweaking for a while to improve workflow issues that might arise.<br>
<br>
There are some extra python libraries that are required over and above what is<br>
currently specified in rtems-central/requirements.txt<u></u><u></u></p>
</blockquote>
<p class="MsoNormal"><br>
This all makes sense to me. Thank you for taking the time to respond.<br>
<br>
Chris<br>
_______________________________________________<br>
devel mailing list<br>
<a href="mailto:devel@rtems.org" target="_blank">devel@rtems.org</a><br>
<a href="http://lists.rtems.org/mailman/listinfo/devel" target="_blank">http://lists.rtems.org/mailman/listinfo/devel</a><u></u><u></u></p>
</blockquote>
</div>
</div>
</blockquote>
</div>
<p class="MsoNormal"><u></u> <u></u></p>
</div>
</div>

_______________________________________________<br>
devel mailing list<br>
<a href="mailto:devel@rtems.org" target="_blank">devel@rtems.org</a><br>
<a href="http://lists.rtems.org/mailman/listinfo/devel" rel="noreferrer" target="_blank">http://lists.rtems.org/mailman/listinfo/devel</a></div></blockquote></div><br clear="all"><div><br></div>-- <br><div dir="ltr" class="gmail_signature"><div dir="ltr">Diese Mail wurde mobil geschrieben. Etwaige Rechtschreibfehler sind volle Absicht und als großzügiges Geschenk zu verstehen.<br></div></div>