Add Formal Verification chapter v4

[Andrew.Butterfield at scss.tcd.ie]

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




From: "Andrew.Butterfield at scss.tcd.ie <mailto:Andrew.Butterfield at scss.tcd.ie>" <Andrew.Butterfield at scss.tcd.ie <mailto:Andrew.Butterfield at scss.tcd.ie>>
Date: Thursday 21 September 2023 at 17:02

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

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

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/> <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> <mailto: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/> <https://embedded-brains.de/datenschutzerklaerung/> <https://embedded-brains.de/datenschutzerklaerung/>>