Add Formal Verification chapter v4

[Gedare Bloom]

On Mon, Oct 9, 2023 at 9:34 AM Andrew.Butterfield at scss.tcd.ie
<Andrew.Butterfield at scss.tcd.ie> wrote:
>
> 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
>

I think v5 would be ready to push. I had no further comments beyond
what I put before.

>
>
>