Add Formal Verification chapter v2

[Chris Johns]

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