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