Add Formal Verification chapter v4

[Gedare Bloom]

On Thu, Sep 21, 2023 at 9:36 AM Sebastian Huber
<sebastian.huber at embedded-brains.de> wrote:
>
> On 21.09.23 17:28, Gedare Bloom wrote:
> > I've taken a look and resolved / commented. We can leave some of the
> > `sis` specific bits, with the understanding that hopefully the
> > simulation target can be made more generic in the future. This could be
> > a potential GSoC project for Prequalification to hook it up to
> > `rtems-tools.git/tester` to make use of the capabilities we already have
> > for running simulators.
>
> The model based tests are not target-specific. You could run them with
> any (simulator) BSP.
>
Yes, I suspected that. However, the documentation is currently written
toward sis. It may be better to point the reader to another doc that
explains how to run tests, such as
https://docs.rtems.org/branches/master/user/tools/tester.html

I don't recall any documentation that discusses simulator targets specifically.

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