Add Formal Verification chapter v4

[Andrew.Butterfield at scss.tcd.ie]

On 21/09/2023, 16:42, "Sebastian Huber" <sebastian.huber at embedded-brains.de <mailto: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
>> <sebastian.huber at embedded-brains.de <mailto: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 <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.

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.

Regards, Andrew


-------------------------------------------------------------------- 
Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 
Lero at TCD, Head of Software Foundations & Verification Research Group 
School of Computer Science and Statistics, 
Room G.39, O'Reilly Institute, Trinity College, University of Dublin 
http://www.scss.tcd.ie/Andrew.Butterfield/ <http://www.scss.tcd.ie/Andrew.Butterfield/> 
--------------------------------------------------------------------
-- 
embedded brains GmbH
Herr Sebastian HUBER
Dornierstr. 4
82178 Puchheim
Germany
email: sebastian.huber at embedded-brains.de <mailto: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/ <https://embedded-brains.de/datenschutzerklaerung/>