Add Formal Verification chapter v2

[Sebastian Huber]

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.

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