Add Formal Verification chapter v2

[Andrew.Butterfield at scss.tcd.ie]

> On 25/11/2022 07:46, Sebastian Huber <sebastian.huber at embedded-brains.de> wrote:
>>  On 24/11/2022 14:41, Andrew.Butterfield at scss.tcd.ie wrote:
>>>  On 16/11/2022 16:44, Gedare Bloom <gedare at rtems.org> 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.

Now that the integration of the formal models and tools is in progress, I want 
to revisit this issue. Yes, the models cover core services, but those are
described in other documents like the Classic API guide (and POSIX). It would
seem that a better place to put any model documentation would be in those guides.

However, the formal verification/qualification is something very new, and I’m 
not sure how regular users would feel about that kind of extra material, at
least at this early stage of adopting qual/FV techniques.

For now, I am going fixup all the other issues raised by Gedare, 
and submit a v2 patch set.

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/
--------------------------------------------------------------------