<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;}
@font-face
{font-family:Menlo-Regular;
panose-1:2 11 6 9 3 8 4 2 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;}
.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;-webkit-line-break: after-white-space">
<div class="WordSection1">
<p class="MsoNormal"><o:p> </o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal"><span style="font-family:Menlo-Regular">Hi Andrew,</span><o:p></o:p></p>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">Hi Gerard,<o:p></o:p></p>
<div>
<p class="MsoNormal"> first, thanks for the very comprehensive review below - this feedback is very useful for me.<br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal"><span style="font-family:Menlo-Regular"><br>
I guess I was overly optimistic last night. The note on the front<br>
matter should be resolved before we push the full documentation. I<br>
guess it's a bit of chicken-and-egg but the documentation should be<br>
pushed concurrent with the software that it documents. So, when there<br>
is a `formal` folder in `rtems-central` then it makes sense to push<br>
this documentation. I think the documentation is valuable, but I'm not<br>
sure how relevant it is without the associated tooling?</span><o:p></o:p></p>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">Ok, should I do a separate "adding formal to RTEMS" patch for this, or merge it with the revisions<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">for this patch set? <o:p></o:p></p>
<p class="MsoNormal">At this stage it would consist of adding the folder `formal`
<o:p></o:p></p>
<p class="MsoNormal">from the main branch at <a href="https://github.com/andrewbutterfield/RTEMS-SMP-Formal">
https://github.com/andrewbutterfield/RTEMS-SMP-Formal</a><o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">The current state of main at RTEMS-SMP-Formal is that is has two new managers added in<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">(Barrier and Messages) and all tests run and pass. This has been recently checked by the team<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">currently doing IV&V on the work we delivered at the end of last year, plus our newer stuff.<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">
<p class="MsoNormal"><span style="font-family:Menlo-Regular"><br>
We probably need to rearrange this section slightly to accommodate the<br>
possibility (extant) of other formal verification approaches. I think<br>
I'd like to see Sections "9.2 Formal Tools Setup" and 9.4 through the<br>
end of the section become nested beneath "9.3 Modelling RTEMS with<br>
Promela". Add a new section 9.2 to introduce the different approaches<br>
that have/are/might be used to formally verify RTEMS. This will allow<br>
alternatives to be documented and acknowledged by the RTEMS Project.</span><o:p></o:p></p>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">Fine - I'll do that .<br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal"><span style="font-family:Menlo-Regular"><br>
There's a bunch of terminology that is introduced in this chapter<br>
without additions to the glossary/index. I think we need some<br>
definitions added there to complement the new material. At the very<br>
least I would like to see definitions added for the keywords that are<br>
defined especially in the introduction:<br>
* semantics, formal model, artifact, refinement, LTL<br>
Once those are defined, the terms should be linked to the glossary.<br>
You can see how this is done for example in Section 5.3.4 Traceability<br>
between Software Requirements, Architecture and Design. Glossary<br>
definitions can/should link to each other as relevant.</span><o:p></o:p></p>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">OK - I'll do the glossary mods<br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal"><span style="font-family:Menlo-Regular"><br>
"To avoid using (long) absolute pathnames to the tools directory" ...<br>
--> maybe it makes sense for you to provide these as part of the env?<br>
Is this stuff using venv or something else?</span><o:p></o:p></p>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">I have a student looking at the python code - he is adding a lot of config related stuff into the<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">testbuilder python scripts. I might ask him to look at adding that into the venv we use.<br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal"><span style="font-family:Menlo-Regular"><br>
incomplete section header? "need to explain how to configure testbuilder"<br>
RTMES typo in that section</span><o:p></o:p></p>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">That's a note to self that I missed - I'll fix that up.<br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal"><span style="font-family:Menlo-Regular"><br>
In section "9.2.2 Running Test Generation" please add some notion of<br>
what is the expected output that one would be checking in the step<br>
"use a simulator to run ts-model-0.exe directly."</span><o:p></o:p></p>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">Ok<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">
<p class="MsoNormal"><span style="font-family:Menlo-Regular"><br>
There is overuse of double quotations throughout. Sometimes double<br>
quotes are being used to introduce terminology, avoid that. Sometimes<br>
double quotes appear in section headings, avoid that. Prefer to use<br>
double quotes only for quoting (e.g., from references or tool output).<br>
Most cases of the double quotes use in this document should be<br>
eliminated.</span><o:p></o:p></p>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">Will do.<br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal"><span style="font-family:Menlo-Regular"><br>
In section "9.4 Promela to C Refinement" what is the name of the YAML<br>
file? Is there more than one, or is it unique.</span><o:p></o:p></p>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">Currently there is one, with a filename based on the model name, in a similar manner to the way that the preamble and postamble files are named. I'll add a reminder here about the naming convention in use.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">There is a longer term issue to be addressed here as the number of models grows. <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">There will be quite a lot of commonality in the refinement YAML files, <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">and it might make sense to have both general and model-specific files for this.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">That is future work at present.<br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal"><span style="font-family:Menlo-Regular"><br>
Some of the text that provides examples of how to do some of this<br>
might be suited to a new How-To subsection such as in the end of the<br>
"BSP Build System" section.</span><o:p></o:p></p>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">OK<br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal"><span style="font-family:Menlo-Regular"><br>
In Section "9.6 Test Generation Maintenance" please refer to Section<br>
"Software Development Management" instead of hard-coding the patch<br>
submission process.</span><o:p></o:p></p>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">Ok<br>
<br>
<o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal"><span style="font-family:Menlo-Regular"><br>
Section 9.7 "RTEMS Formal Model Guide" seems like it includes both<br>
some aspects of a How-To but also a lot of details that might be<br>
better as a separate document specific to the Promela/Verification<br>
detailed implementation. The point of the RTEMS Software Engineering<br>
manual is to provide developers with the guidelines of how to work<br>
with RTEMS. This section is very detailed about the implementation of<br>
specific models and feels unbalanced with the rest of the new section.<br>
For example, this section is about 3/5 of the entire "Formal<br>
Verification" section.</span><o:p></o:p></p>
</blockquote>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<p class="MsoNormal">I agree - this was what struck me after I had sent the patch set. In a sense I think we need a new top-level document, analagous to the Classic API and POSIX API guides.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">So, I need to fix this section in the Engineering manual, add in the actual formal software,<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal">and develop a new guide to promela modelling. <o:p></o:p></p>
<p class="MsoNormal">The formal software will a patch-set relative to rtems-central.<o:p></o:p></p>
<p class="MsoNormal">I guess I do two patch-sets off rtems-docs, one for the revisions above, the other for a new Promela model guide document.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal">Regards, <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">
<p class="MsoNormal"><span style="font-family:Menlo-Regular"><br>
Gedare<br>
<br>
On Wed, Nov 16, 2022 at 3:57 AM </span><a href="mailto:Andrew.Butterfield@scss.tcd.ie"><span style="font-family:Menlo-Regular">Andrew.Butterfield@scss.tcd.ie</span></a><span style="font-family:Menlo-Regular"><br>
<</span><a href="mailto:Andrew.Butterfield@scss.tcd.ie"><span style="font-family:Menlo-Regular">Andrew.Butterfield@scss.tcd.ie</span></a><span style="font-family:Menlo-Regular">> wrote:<br>
<br>
</span><o:p></o:p></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal"><span style="font-family:Menlo-Regular"><br>
Dear Gedare,<br>
thanks for doing this - all feedback welcome!<br>
<br>
Best regards,<br>
Andrew<br>
<br>
--------------------------------------------------------------------<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/">http://www.scss.tcd.ie/Andrew.Butterfield/</a><br>
--------------------------------------------------------------------<br>
<br>
<br>
-----Original Message-----<br>
From: Gedare Bloom <<a href="mailto:gedare@rtems.org">gedare@rtems.org</a>><br>
Date: Wednesday 16 November 2022 at 02:00<br>
To: Chris Johns <<a href="mailto:chrisj@rtems.org">chrisj@rtems.org</a>><br>
Cc: "<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>>, "<a href="mailto:rtems-devel@rtems.org">rtems-devel@rtems.org</a>" <<a href="mailto:rtems-devel@rtems.org">rtems-devel@rtems.org</a>><br>
Subject: Re: Add Formal Verification chapter v2<br>
<br>
I plan to look at this tomorrow and will plan to push it as-is. I will<br>
push any modifications I think should be made, or send notes back<br>
here, after I look through it very carefully.<br>
<br>
On Wed, Nov 9, 2022 at 5:39 PM Chris Johns <<a href="mailto:chrisj@rtems.org">chrisj@rtems.org</a>> wrote:<br>
<br>
<o:p></o:p></span></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal"><span style="font-family:Menlo-Regular"><br>
On 9/11/2022 9:48 pm, <a href="mailto:Andrew.Butterfield@scss.tcd.ie">Andrew.Butterfield@scss.tcd.ie</a> wrote:<br>
<br>
<o:p></o:p></span></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal" style="margin-bottom:12.0pt"><span style="font-family:Menlo-Regular">ping<br>
<br>
(my fault really, i've let this sit!)<o:p></o:p></span></p>
</blockquote>
<p class="MsoNormal"><span style="font-family:Menlo-Regular"><br>
Thank you for raising this and I am sorry we have not been as proactive<br>
as we should be.<br>
<br>
<br>
<o:p></o:p></span></p>
<blockquote style="margin-top:5.0pt;margin-bottom:5.0pt">
<p class="MsoNormal" style="margin-bottom:12.0pt"><span style="font-family:Menlo-Regular">But I have been busy, interacting with a group doing a follow-up IV&V project with the qualification data package we produced.<br>
A conseuience of this is that I am helping them to add two extra manager models developed by students, for Barriers and Message Queues.<br>
<br>
This would add two more entries to the model guide, and raises the question of the best place to document the models.<br>
Is the RTEMS Software Engineering manual the best location for those? If not, where should they live?<br>
<br>
Another side effect fo all this is that there is now a definitive version of the formal models and test generation in a public repo:<br>
<br>
<a href="https://github.com/andrewbutterfield/RTEMS-SMP-Formal">https://github.com/andrewbutterfield/RTEMS-SMP-Formal</a><o:p></o:p></span></p>
</blockquote>
<p class="MsoNormal"><span style="font-family:Menlo-Regular"><br>
Excellent.<br>
<br>
I have no expertise in this area and I am more than happy to defer to<br>
you and your team in this area.<br>
<br>
I have no objections to this working being merge as is. I see it as<br>
green field work and yours is the first here. I am sure updates or<br>
changes can be made over time by you or others as the work is absorbed<br>
and reviewed.<br>
<br>
Thank you for all the efforts you and those with you have made. I<br>
personally think it is fantastic to have this work happen and being made<br>
public in this way so thank you from me.<br>
<br>
Chris<br>
_______________________________________________<br>
devel mailing list<br>
<a href="mailto:devel@rtems.org">devel@rtems.org</a><br>
<a href="http://lists.rtems.org/mailman/listinfo/devel">http://lists.rtems.org/mailman/listinfo/devel</a><o:p></o:p></span></p>
<p class="MsoNormal"><span style="font-family:Menlo-Regular"><o:p> </o:p></span></p>
</blockquote>
</blockquote>
</blockquote>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<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/"><span style="color:#0563C1">http://www.scss.tcd.ie/Andrew.Butterfield/</span></a><br>
--------------------------------------------------------------------<o:p></o:p></p>
<p class="MsoNormal"><span style="font-family:Menlo-Regular"><o:p> </o:p></span></p>
</div>
</body>
</html>