Add Formal Verification chapter v4

[Sebastian Huber]

On 21.09.23 17:41, Gedare Bloom wrote:
> 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.

Yes, we should not duplicate this documentation. This is not maintainable.

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