Add Formal Verification chapter v2

[Gedare Bloom]

On Fri, Nov 25, 2022 at 12:45 AM Sebastian Huber
<sebastian.huber at embedded-brains.de> wrote:
>
> On 24/11/2022 14:41, Andrew.Butterfield at scss.tcd.ie wrote:
> >
> >     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.
>
> I am not sure if a new top-level document is really the best option.
>  From my point of view, the RTEMS Software Engineering manual should
> cover everything useful for the general RTEMS maintainer. The models
> cover core services of RTEMS. With different documents you just have to
> open more documents and cross referencing will be more difficult. I am
> more in favour of a top-level chapter in the manual or some sort of an
> appendix chapter.
>

My intuition here is that with suitable How-To's written and the code
pushed, we don't need such detailed implementation notes. Just point
the interested reader to the implementation, and to more general
documentation/reports about Promela or even a tech report published by
the group that did this work.

> --
> embedded brains GmbH
> Herr Sebastian HUBER
> Dornierstr. 4
> 82178 Puchheim
> Germany
> email: sebastian.huber at embedded-brains.de
> phone: +49-89-18 94 741 - 16
> fax:   +49-89-18 94 741 - 08
>
> Registergericht: Amtsgericht München
> Registernummer: HRB 157899
> Vertretungsberechtigte Geschäftsführer: Peter Rasmussen, Thomas Dörfler
> Unsere Datenschutzerklärung finden Sie hier:
> https://embedded-brains.de/datenschutzerklaerung/