Add Formal Verification chapter v4

[Gedare Bloom]

On Fri, Sep 22, 2023 at 4:50 AM Andrew.Butterfield at scss.tcd.ie
<Andrew.Butterfield at scss.tcd.ie> wrote:
>
>
>
> --------------------------------------------------------------------
> 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
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.

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