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@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 <ged...@rtems.org> Date: Wednesday 16 November 2022 at 02:00 To: Chris Johns <chr...@rtems.org> Cc: "andrew.butterfi...@scss.tcd.ie" <andrew.butterfi...@scss.tcd.ie>, "rtems-de...@rtems.org" <rtems-de...@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 <chr...@rtems.org> wrote: > > On 9/11/2022 9:48 pm, andrew.butterfi...@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@rtems.org > http://lists.rtems.org/mailman/listinfo/devel _______________________________________________ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel