Add Formal Verification chapter v2

[Gedare Bloom]

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