<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;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
span.EmailStyle18
{mso-style-type:personal-reply;
font-family:"Calibri",sans-serif;
color:windowtext;}
.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="blue" vlink="purple" style="word-wrap:break-word;-webkit-nbsp-mode: space;line-break:after-white-space">
<div class="WordSection1">
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">On 1 Jul 2022, at 00:59, Chris Johns <<a href="mailto:chrisj@rtems.org">chrisj@rtems.org</a>> wrote:<o:p></o:p></p>
<div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal">On 28/6/2022 11:09 pm, <a href="mailto:Andrew.Butterfield@scss.tcd.ie">
Andrew.Butterfield@scss.tcd.ie</a> 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>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">Indeed, I quite agree. I have some short answers below, with suggestions.<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>
What will be submitted, ie SPIN files, scripts, etc?<o:p></o:p></p>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">Promela/SPIN model files (ASCII text, C-like syntax)<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">C template files (.h,.c) to assist test code generation<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">YAML files to provide a mapping from model concepts to RTEMS C test code <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">python scripts to automate the test generation<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">Documentation - largely RTEMS compliant sphinx sources (.rst)<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<p class="MsoNormal"><br>
Where are you looking to add these pieces?<o:p></o:p></p>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Everything except the documentation could live in a top-level folder ('formal') in rtems-central.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">In fact there is no particular constraint from my perspective for where they can go.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">The plan would be to add the pertinent parts of our project documentation into new chapters<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">in the RTEMS software engineering manual. So that would be eng/ in the rtems-docs repo.<o:p></o:p></p>
</div>
</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>
How is the verification run against the code? Do we manage regression testing<br>
and is that even possible?<o:p></o:p></p>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">The python scripts basically run SPIN in such a way as to generate scenarios that model<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">correct behaviour which then get turned into standard RTEMS test programs. These all<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">get added into a new testsuite in the rtems repo (testsuites/models, say).<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">They are properly integrated into the RTEMS test system, so get built and run by waf.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">This is similar to how the tests generated by Sebastian in testsuites/validation are handled.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">From the perspective of a user that works out of <a href="http://git.rtems.org/rtems">
git.rtems.org/rtems</a>, <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">there will be no obvious impact - just some extra tests in among the ones that already exist.<o:p></o:p></p>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<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>
</div>
</div>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">I intend to continue to work and maintain this for the foreseeable future. I would hope as this beds in that other Promela/SPIN users out there will also get more involved over time.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">It is expected that Promela models will be as static as the corresponding APIs. They capture the specified behaviour of API calls, not their detailed implementation.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">The python scripts should also be fairly stable, although I can see some tweaking for a while to improve workflow issues that might arise.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">There are some extra python libraries that are required over and above what is currently specified in rtems-central/requirements.txt<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<div>
<div>
<p class="MsoNormal"><br>
Thanks<br>
Chris<o:p></o:p></p>
</div>
</div>
</blockquote>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Thanks,<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"> Andrew<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal"><br>
<br>
<o:p></o:p></p>
</div>
</body>
</html>