Add Formal Verification chapter v2

[Andrew.Butterfield at scss.tcd.ie]

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>
Date: Wednesday 16 November 2022 at 02:00
To: Chris Johns <chrisj at rtems.org>
Cc: "Andrew.Butterfield at scss.tcd.ie" <Andrew.Butterfield at scss.tcd.ie>, "rtems-devel at rtems.org" <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> wrote:
    >
    > On 9/11/2022 9:48 pm, 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
    > http://lists.rtems.org/mailman/listinfo/devel