<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-IE" link="#0563C1" vlink="#954F72" style="word-wrap:break-word;-webkit-nbsp-mode: space;line-break:after-white-space">
<div class="WordSection1">
<div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<p class="MsoNormal">On 6 Jul 2022, at 20:07, Gedare Bloom <gedare@rtems.org> wrote:<o:p></o:p></p>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal">On Sun, Jul 3, 2022 at 7:49 PM Chris Johns <chrisj@rtems.org> wrote:<br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal"><br>
On 2/7/2022 12:59 am, Andrew Butterfield wrote:<br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal">On 1 Jul 2022, at 00:59, Chris Johns <chrisj@rtems.org<br>
<mailto:chrisj@rtems.org>> wrote:<br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal"><br>
On 28/6/2022 11:09 pm, Andrew.Butterfield@scss.tcd.ie<br>
<mailto:Andrew.Butterfield@scss.tcd.ie> wrote:<br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<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.<o:p></o:p></p>
</blockquote>
<p class="MsoNormal"><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>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<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?<o:p></o:p></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.<o:p></o:p></p>
</blockquote>
<p class="MsoNormal"><br>
Indeed, I quite agree. I have some short answers below, with suggestions.<o:p></o:p></p>
</blockquote>
<p class="MsoNormal" style="margin-bottom:12.0pt"><br>
Thanks.<o:p></o:p></p>
</blockquote>
<p class="MsoNormal">+1<br>
<br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal"><br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal"><br>
What will be submitted, ie SPIN files, scripts, etc?<o:p></o:p></p>
</blockquote>
<p class="MsoNormal"><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>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal"><br>
Where are you looking to add these pieces?<o:p></o:p></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.<o:p></o:p></p>
</blockquote>
<p class="MsoNormal" style="margin-bottom:12.0pt"><br>
Using rtems-central is fine.<o:p></o:p></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.<o:p></o:p></p>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">At the moment there is nothing in rtems-central directly related to this. All the python<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">scripts there support the tools/specs that Sebastian and colleagues developed.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">I can see a new top-level script being added here to support the formal stuff.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">It is possible that we might introduce a new specification item that integrates<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">in with the spec system that is used to trigger the Spin test generations. I'll discuss the<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">best wat to do this with Sebastian.<o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal"><br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<p class="MsoNormal"><br>
RSB should be taught how to build the necessary host tools to run Promela/SPIN.<o:p></o:p></p>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">Spin is open source under a BSD 3-clause license, available from spinroot.com,<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">and also via https://github.com/nimble-code/Spin. It is written in C and has very few<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">dependencies. I'm not sure what is involved in adding it to the RSB, but I guess <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">Sebastian will know. <o:p></o:p></p>
</div>
<div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<p class="MsoNormal"><br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<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.<o:p></o:p></p>
</blockquote>
<p class="MsoNormal" style="margin-bottom:12.0pt"><br>
Great.<o:p></o:p></p>
</blockquote>
<p class="MsoNormal">+1<br>
<br>
A new section in the eng should be suitable. I would actually<br>
recommend using<br>
https://docs.rtems.org/branches/master/eng/test-framework.html# as a<br>
good example.<o:p></o:p></p>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">Thanks - that very helpful. I think our section should immediately follow that one.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">All we need now is a suitable title. "Formal Test Framework"?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<p class="MsoNormal"><br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal">How is the verification run against the code? Do we manage regression testing<br>
and is that even possible?<o:p></o:p></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 git.rtems.org/rtems<br>
<http://git.rtems.org/rtems>,<br>
there will be no obvious impact - just some extra tests in among the ones that<br>
already exist.<o:p></o:p></p>
</blockquote>
<p class="MsoNormal"><br>
Thanks and this make sense.<br>
<br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal"><br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<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.<o:p></o:p></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.<o:p></o:p></p>
</blockquote>
<p class="MsoNormal" style="margin-bottom:12.0pt"><br>
Thank, it is appreciated.<o:p></o:p></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.<o:p></o:p></p>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">Indeed - that would be good. <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Andrew <br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<p class="MsoNormal"><br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<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<o:p></o:p></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>
devel@rtems.org<br>
http://lists.rtems.org/mailman/listinfo/devel<o:p></o:p></p>
</blockquote>
</div>
</div>
</blockquote>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
</body>
</html>