Add Formal Verification chapter v4

[Andrew.Butterfield at scss.tcd.ie]

Eliding some stuff....
>On 05/10/2023, 16:02, "Gedare Bloom" <gedare at rtems.org <mailto:gedare at rtems.org>> wrote:
>>On Fri, Sep 22, 2023 at 4:50 AM Andrew.Butterfield at scss.tcd.ie <mailto:Andrew.Butterfield at scss.tcd.ie> wrote:
>>On 21/09/2023, 16:42, "Sebastian Huber" <sebastian.huber at embedded-brains.de >>> wrote:
>>>On 21.09.23 17:41, Gedare Bloom wrote:
>>>> On Thu, Sep 21, 2023 at 9:36 AM Sebastian Huber
>>>> I don't recall any documentation that discusses simulator targets specifically.
>>Yes, we should not duplicate this documentation. This is not maintainable.
>>>I can remove all references to `sis` from the documentation and point to tester.html
>>>However note that the python sources for all of this, in rtems-central/formal/promela/src
>>>we have explicit references in testbuilder-template.yml to `simulator: <path-to>/sparc-rtems6-sis`
>>>I guess that needs to be changed
>> I've referred to the RTEMS Tester, (replacing `sis`),
>> and also just noted that the default template for testbuilder refers to `sis`
>> Also, I'm not sure the best way to refer to a sub-section of another document
>> I used something like (See Host Tools in the RTEMS User Manual)
>> I guessed the URL might be less robust
>Yes this is basically correct. We don't want explicit links between
>documents. It's a bit challenging at the moment to validate
>cross-document references and we don't have a great solution or
>standard approach for how to do it.

Is it now worthwhile my preparing a v5 set of patches for committing into rtems-docs master,
Or are there more edits that need doing?

Rergards, Andrew