Re: Add Formal Verification chapter v2

2022-11-16 Thread andrew.butterfi...@scss.tcd.ie 
Dear Gedare,
 thanks for doing this - all feedback welcome!

Best regards,
  Andrew


Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
Lero@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/

 

-Original Message-
From: Gedare Bloom 
Date: Wednesday 16 November 2022 at 02:00
To: Chris Johns 
Cc: "andrew.butterfi...@scss.tcd.ie" , 
"rtems-de...@rtems.org" 
Subject: Re: Add Formal Verification chapter v2

I plan to look at this tomorrow and will plan to push it as-is. I will
push any modifications I think should be made, or send notes back
here, after I look through it very carefully.

On Wed, Nov 9, 2022 at 5:39 PM Chris Johns  wrote:
>
> On 9/11/2022 9:48 pm, andrew.butterfi...@scss.tcd.ie wrote:
> > ping
> >
> > (my fault really, i've let this sit!)
> >
>
> Thank you for raising this and I am sorry we have not been as proactive
> as we should be.
>
> > But I have been busy, interacting with a group doing a follow-up IV&V 
project with the qualification data package we produced.
> > A conseuience of this is that I am helping them to add two extra 
manager models developed by students, for Barriers and Message Queues.
> >
> > This would add two more entries to the model guide, and raises the 
question of the best place to document the models.
> > Is the RTEMS Software Engineering manual the best location for those? 
If not, where should they live?
> >
> > Another side effect fo all this is that there is now a definitive 
version of the formal models and test generation in a public repo:
> >
> > https://github.com/andrewbutterfield/RTEMS-SMP-Formal
> >
>
> Excellent.
>
> I have no expertise in this area and I am more than happy to defer to
> you and your team in this area.
>
> I have no objections to this working being merge as is. I see it as
> green field work and yours is the first here. I am sure updates or
> changes can be made over time by you or others as the work is absorbed
> and reviewed.
>
> Thank you for all the efforts you and those with you have made. I
> personally think it is fantastic to have this work happen and being made
> public in this way so thank you from me.
>
> Chris
> ___
> devel mailing list
> devel@rtems.org
> http://lists.rtems.org/mailman/listinfo/devel

___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: Add Formal Verification chapter v2

2022-11-24 Thread andrew.butterfi...@scss.tcd.ie 
the entire "Formal
Verification" section.

I agree - this was what struck me after I had sent the patch set. In a sense I 
think we need a new top-level document, analagous to the Classic API and POSIX 
API guides.

So, I need to fix this section in the Engineering manual, add in the actual 
formal software,
and develop a new guide to promela modelling.
The formal software will a patch-set relative to rtems-central.
I guess I do two patch-sets off rtems-docs, one for the revisions above, the 
other for a new Promela model guide document.


Regards,
Andrew


Gedare

On Wed, Nov 16, 2022 at 3:57 AM 
andrew.butterfi...@scss.tcd.ie<mailto:andrew.butterfi...@scss.tcd.ie>
mailto:andrew.butterfi...@scss.tcd.ie>> wrote:


Dear Gedare,
thanks for doing this - all feedback welcome!

Best regards,
 Andrew


Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
Lero@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/
--------


-Original Message-
From: Gedare Bloom mailto:ged...@rtems.org>>
Date: Wednesday 16 November 2022 at 02:00
To: Chris Johns mailto:chr...@rtems.org>>
Cc: "andrew.butterfi...@scss.tcd.ie<mailto:andrew.butterfi...@scss.tcd.ie>" 
mailto:andrew.butterfi...@scss.tcd.ie>>, 
"rtems-de...@rtems.org<mailto:rtems-de...@rtems.org>" 
mailto:rtems-de...@rtems.org>>
Subject: Re: Add Formal Verification chapter v2

   I plan to look at this tomorrow and will plan to push it as-is. I will
   push any modifications I think should be made, or send notes back
   here, after I look through it very carefully.

   On Wed, Nov 9, 2022 at 5:39 PM Chris Johns 
mailto:chr...@rtems.org>> wrote:


On 9/11/2022 9:48 pm, 
andrew.butterfi...@scss.tcd.ie<mailto:andrew.butterfi...@scss.tcd.ie> wrote:

ping

(my fault really, i've let this sit!)

Thank you for raising this and I am sorry we have not been as proactive
as we should be.


But I have been busy, interacting with a group doing a follow-up IV&V project 
with the qualification data package we produced.
A conseuience of this is that I am helping them to add two extra manager models 
developed by students, for Barriers and Message Queues.

This would add two more entries to the model guide, and raises the question of 
the best place to document the models.
Is the RTEMS Software Engineering manual the best location for those? If not, 
where should they live?

Another side effect fo all this is that there is now a definitive version of 
the formal models and test generation in a public repo:

https://github.com/andrewbutterfield/RTEMS-SMP-Formal

Excellent.

I have no expertise in this area and I am more than happy to defer to
you and your team in this area.

I have no objections to this working being merge as is. I see it as
green field work and yours is the first here. I am sure updates or
changes can be made over time by you or others as the work is absorbed
and reviewed.

Thank you for all the efforts you and those with you have made. I
personally think it is fantastic to have this work happen and being made
public in this way so thank you from me.

Chris
___
devel mailing list
devel@rtems.org<mailto:devel@rtems.org>
http://lists.rtems.org/mailman/listinfo/devel




Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
Lero@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/


___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: Add Formal Verification chapter v2

2022-12-19 Thread andrew.butterfi...@scss.tcd.ie 
Hi Sebastian,
 I will do that - so I expect to have two new separate patch sets.
I have already checked a lot of it for license/copyright stuff, but I'll 
double-check this.

The first will add a `formal` folder to rtems-central, as  you specified.
The second will add a revised version of the FV chapter to the software 
engineering manual,
as suggested by Gedare.

Best regards,
  Andrew



On 25/11/2022, 07:48, "Sebastian Huber" mailto:sebastian.hu...@embedded-brains.de>> wrote:


On 16/11/2022 17:44, Gedare Bloom wrote:
> I guess I was overly optimistic last night. The note on the front
> matter should be resolved before we push the full documentation. I
> guess it's a bit of chicken-and-egg but the documentation should be
> pushed concurrent with the software that it documents. So, when there
> is a `formal` folder in `rtems-central` then it makes sense to push
> this documentation. I think the documentation is valuable, but I'm not
> sure how relevant it is without the associated tooling?


Since rtems-central is currently a bit isolated, we could start with the 
integration of the "formal" directory.


Andrew, please check that every file in "formal" has a clear copyright 
and license statement (SPDX identifiers would be great). If you used 
third-party code, then there should be one commit which adds this 
third-party code unmodified with a source of origin in the commit message.


-- 
embedded brains GmbH
Herr Sebastian HUBER
Dornierstr. 4
82178 Puchheim
Germany
email: sebastian.hu...@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/ 




___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

[PATCH 00/18] Adds Formal Verification Material

2022-12-22 Thread andrew.butterfi...@scss.tcd.ie 
>From 3390ccc51f46ce0a4baa60422a62530c7c3c29bd Mon Sep 17 00:00:00 2001
From: Andrew Butterfield 
Date: Wed, 21 Dec 2022 18:03:47 +
Subject: [PATCH 00/18] Adds Formal Verification Material

This patch-set adds in the Promela/SPIN models and tools developed as part of
the ESA-sponsored activity "Qualification of RTEMS Symmetric Multiprocessing
(SMP)" as well as result of ongoing contributions by students at Trinity College
Dublin to improve and extend them.

It is a subset of the material contained at
  https://github.com/andrewbutterfield/RTEMS-SMP-Formal

It focusses in the main on what currently produces RTEMS test code.

Andrew Butterfield (18):
  adds in high-level directories and READMEs
  adds barrier manager model
  adds barrier manager generated material
  adds chains API model
  adds chain api generated material
  adds event manager model
  adds event manager generated material
  adds message manager model
  adds message manager generated material
  adds weak memory models
  adds in draft MrsP models for requirements and code
  third party code - promela parser
  modifies 3rd party code - promela parser
  third party code - comment filter
  modifies 3rd party code - comment filter
  adds test generation source code
  adds tests for testgen code
  adds automatic testgen examples

 formal/.gitignore |3 +
 formal/README.md  |   27 +
 formal/promela/.gitignore |4 +
 formal/promela/README.md  |   27 +
 formal/promela/models/README.md   |   53 +
 formal/promela/models/barriers/README.md  |   11 +
 formal/promela/models/barriers/STATUS.md  |   95 +
 .../20221220-102256/barrier-mgr-model-0.spn   |  220 +++
 .../20221220-102256/barrier-mgr-model-1.spn   |  216 +++
 .../20221220-102256/barrier-mgr-model-10.spn  |  233 +++
 .../20221220-102256/barrier-mgr-model-11.spn  |  229 +++
 .../20221220-102256/barrier-mgr-model-12.spn  |  236 +++
 .../20221220-102256/barrier-mgr-model-13.spn  |  232 +++
 .../20221220-102256/barrier-mgr-model-14.spn  |  212 +++
 .../20221220-102256/barrier-mgr-model-15.spn  |  208 +++
 .../20221220-102256/barrier-mgr-model-16.spn  |  224 +++
 .../20221220-102256/barrier-mgr-model-17.spn  |  220 +++
 .../20221220-102256/barrier-mgr-model-18.spn  |  297 +++
 .../20221220-102256/barrier-mgr-model-19.spn  |  293 +++
 .../20221220-102256/barrier-mgr-model-2.spn   |  220 +++
 .../20221220-102256/barrier-mgr-model-3.spn   |  216 +++
 .../20221220-102256/barrier-mgr-model-4.spn   |  227 +++
 .../20221220-102256/barrier-mgr-model-5.spn   |  223 +++
 .../20221220-102256/barrier-mgr-model-6.spn   |  233 +++
 .../20221220-102256/barrier-mgr-model-7.spn   |  229 +++
 .../20221220-102256/barrier-mgr-model-8.spn   |  233 +++
 .../20221220-102256/barrier-mgr-model-9.spn   |  229 +++
 .../barrier-mgr-model.pml1.trail  |  355 
 .../barrier-mgr-model.pml10.trail |  384 
 .../barrier-mgr-model.pml11.trail |  393 
 .../barrier-mgr-model.pml12.trail |  390 
 .../barrier-mgr-model.pml13.trail |  406 +
 .../barrier-mgr-model.pml14.trail |  403 +
 .../barrier-mgr-model.pml15.trail |  349 
 .../barrier-mgr-model.pml16.trail |  346 
 .../barrier-mgr-model.pml17.trail |  385 
 .../barrier-mgr-model.pml18.trail |  382 
 .../barrier-mgr-model.pml19.trail |  705 
 .../barrier-mgr-model.pml2.trail  |  352 
 .../barrier-mgr-model.pml20.trail |  702 +++
 .../barrier-mgr-model.pml3.trail  |  354 
 .../barrier-mgr-model.pml4.trail  |  351 
 .../barrier-mgr-model.pml5.trail  |  388 
 .../barrier-mgr-model.pml6.trail  |  385 
 .../barrier-mgr-model.pml7.trail  |  394 
 .../barrier-mgr-model.pml8.trail  |  391 
 .../barrier-mgr-model.pml9.trail  |  387 
 .../archive/20221220-102256/model-0-test.log  | 1469 +++
 .../20221220-102256/tr-barrier-mgr-model-0.c  |  399 
 .../20221220-102256/tr-barrier-mgr-model-1.c  |  372 
 .../20221220-102256/tr-barrier-mgr-model-10.c |  414 +
 .../20221220-102256/tr-barrier-mgr-model-11.c |  387 
 .../20221220-102256/tr-barrier-mgr-model-12.c |  419 +
 .../20221220-102256/tr-barrier-mgr-model-13.c |  392 
 .../20221220-102256/tr-barrier-mgr-model-14.c |  380 
 .../20221220-102256/tr-barrier-mgr-model-15.c |  353 
 .../20221220-102256/tr-barrier-mgr-model-16.c |  395 
 .../20221220-102256/tr-barrier-mgr-model-17.c |  368 
 .../20221220-102256/tr-barrier-mgr-model-18.c |  401 
 .../20221220-102256/tr-barrier-mgr-model-19.c |  374 
 .../20221220-102256/tr-barrier-mgr-model-2.c  |  399 
 .../20221220-102256/tr-barrier-mgr-model-3.c  |  372 
 .../20221220-102256/tr-barrier-mgr-model-4.c

[PATCH 01/18] adds in high-level directories and READMEs

2022-12-22 Thread andrew.butterfi...@scss.tcd.ie 

---
 formal/.gitignore   |  3 ++
 formal/README.md| 27 +
 formal/promela/.gitignore   |  4 ++
 formal/promela/README.md| 27 +
 formal/promela/models/README.md | 53 
 formal/promela/src/README.md| 71 +
 6 files changed, 185 insertions(+)
 create mode 100644 formal/.gitignore
 create mode 100644 formal/README.md
 create mode 100644 formal/promela/.gitignore
 create mode 100644 formal/promela/README.md
 create mode 100644 formal/promela/models/README.md
 create mode 100644 formal/promela/src/README.md

diff --git a/formal/.gitignore b/formal/.gitignore
new file mode 100644
index ..2cfdbe69
--- /dev/null
+++ b/formal/.gitignore
@@ -0,0 +1,3 @@
+NOTES.pdf
+*.out
+
diff --git a/formal/README.md b/formal/README.md
new file mode 100644
index ..d3ff71a6
--- /dev/null
+++ b/formal/README.md
@@ -0,0 +1,27 @@
+# Formal Verification
+
+`formal`
+
+This directory contains the models and tooling developed as part of the 
ESA-sponsored activity ***Qualification of RTEMS Symmetric Multiprocessing
(SMP)***, that has been added into RTEMS in the `rtems-central` repository.
+
+## Contributors
+
+* Andrew Butterfield
+* Frédéric Tuong
+* Robert Jennings
+* Jerzy Jaśkuć
+* Eoin Lynch
+* James Gooding Hunt
+
+## License
+
+This project is licensed under the
+[BSD-2-Clause](https://spdx.org/licenses/BSD-2-Clause.html) or
+[CC-BY-SA-4.0](https://spdx.org/licenses/CC-BY-SA-4.0.html).
+
+## Overview
+
+At present, the only formal verification in play here is the use of Promela to 
build formal models of key RTEMS components, and the SPIN model-checker to 
perform C test generation.
+
+This can be found in the `promela` sub-directory
+
diff --git a/formal/promela/.gitignore b/formal/promela/.gitignore
new file mode 100644
index ..5b5b65fa
--- /dev/null
+++ b/formal/promela/.gitignore
@@ -0,0 +1,4 @@
+*/refine_command.py
+*/spin2test.py
+*/pan*
+*/testbuilder.yml
diff --git a/formal/promela/README.md b/formal/promela/README.md
new file mode 100644
index ..87f7299e
--- /dev/null
+++ b/formal/promela/README.md
@@ -0,0 +1,27 @@
+# Promela/SPIN
+
+`formal/promela`
+
+This directory contains formal models written in Promela and tools that use 
SPIN to do test generation from those models.
+
+## Contributors
+
+* Andrew Butterfield
+* Frédéric Tuong
+* Robert Jennings
+* Jerzy Jaśkuć
+* Eoin Lynch
+* James Gooding Hunt
+
+## License
+
+This project is licensed under the
+[BSD-2-Clause](https://spdx.org/licenses/BSD-2-Clause.html) or
+[CC-BY-SA-4.0](https://spdx.org/licenses/CC-BY-SA-4.0.html).
+
+## Overview
+
+The  Promela models and supporting material can be found in the `models` 
subdirectory.
+
+The tools, written in Python3, are in the `src` directory.
+
diff --git a/formal/promela/models/README.md b/formal/promela/models/README.md
new file mode 100644
index ..17de6f2b
--- /dev/null
+++ b/formal/promela/models/README.md
@@ -0,0 +1,53 @@
+# RTEMS Promela Models
+
+`formal/promela/models/'
+
+This directory contains formal models written in Promela to support test 
generation.
+
+## Contributors
+
+* Andrew Butterfield
+* Frédéric Tuong
+* Robert Jennings
+* Jerzy Jaśkuć
+* Eoin Lynch
+
+## License
+
+This project is licensed under the
+[BSD-2-Clause](https://spdx.org/licenses/BSD-2-Clause.html) or
+[CC-BY-SA-4.0](https://spdx.org/licenses/CC-BY-SA-4.0.html).
+
+## Models Overview
+
+There are currently five models present. Four are test-generation ready, 
whilst the fifth is still work in progress.
+
+We identify the usual RTEMS name for the component,
+the Promela "model-name", and the path to the model directory.
+
+* Barrier Manager: "barrier-mgr-model" `formal/promela/models/barriers`
+* Chains API:  "chains-api-model" `formal/promela/models/chains`
+* Event Manager "event-mgr-model" `formal/promela/models/events`
+* Message Manager "msg-mgr-model" `formal/promela/models/messages`
+* MrsP Thread Queues "mrsp-threadq-model" `formal/promela/models/threadq`
+
+## Doing Test Generation
+
+Ensure that the virtual environment defined in `formal/promela/src/env` is 
active.
+
+We shall assume that the alias `tb` has been defined as suggested in  
`formal/promela/src/README.md`.
+
+Simply enter the relevant model sub-directory and invoke `tb` from the command 
line with desired command line arguments.
+
+A simple sequence that clears out all previously generated tests (from all 
models), clears all generated artifacts from this model,
+and then does the whole test generation process is:
+
+```
+tb zero
+tb clean
+tb all 
+```
+
+This will produce a test report in `-test.log`.
+
+
diff --git a/formal/promela/src/README.md b/formal/promela/src/README.md
new file mode 100644
index ..dd80420a
--- /dev/null
+++ b/formal/promela/src/README.md
@@ -0,0 +1,71 @@
+# Test Generation Tools
+
+`formal/promela/src`
+
+This directory contains tools that use SPIN to do test generation

[PATCH 02/18] adds barrier manager model

2022-12-22 Thread andrew.butterfi...@scss.tcd.ie 


---
 formal/promela/models/barriers/README.md  |   11 +
 formal/promela/models/barriers/STATUS.md  |   95 ++
 .../models/barriers/barrier-mgr-model-post.h  |   44 +
 .../models/barriers/barrier-mgr-model-pre.h   |   51 +
 .../models/barriers/barrier-mgr-model-rfn.yml |  169 +++
 .../models/barriers/barrier-mgr-model-run.h   |   91 ++
 .../models/barriers/barrier-mgr-model.pml | 1158 +
 .../models/barriers/tc-barrier-mgr-model.c|  180 +++
 .../models/barriers/tr-barrier-mgr-model.c|  249 
 .../models/barriers/tr-barrier-mgr-model.h|  197 +++
 10 files changed, 2245 insertions(+)
 create mode 100644 formal/promela/models/barriers/README.md
 create mode 100644 formal/promela/models/barriers/STATUS.md
 create mode 100644 formal/promela/models/barriers/barrier-mgr-model-post.h
 create mode 100644 formal/promela/models/barriers/barrier-mgr-model-pre.h
 create mode 100644 formal/promela/models/barriers/barrier-mgr-model-rfn.yml
 create mode 100644 formal/promela/models/barriers/barrier-mgr-model-run.h
 create mode 100644 formal/promela/models/barriers/barrier-mgr-model.pml
 create mode 100644 formal/promela/models/barriers/tc-barrier-mgr-model.c
 create mode 100644 formal/promela/models/barriers/tr-barrier-mgr-model.c
 create mode 100644 formal/promela/models/barriers/tr-barrier-mgr-model.h

diff --git a/formal/promela/models/barriers/README.md 
b/formal/promela/models/barriers/README.md
new file mode 100644
index ..5ed32946
--- /dev/null
+++ b/formal/promela/models/barriers/README.md
@@ -0,0 +1,11 @@
+# Barrier Manager model
+
+Developer: Jerzy Jaśkuć
+
+SPIN/Promela based test generation framework for RTEMS Barrier Manager
+
+This directory contains all of the necessary files needed to perform test 
generation for [RTEMS](https://www.rtems.org/ "RTEMS Homepage") [Barrier 
Manager](https://docs.rtems.org/branches/master/c-user/barrier/background.html 
"Barrier Manager") using SPIN/Promela framework.
+
+It is a subset of the material available at [Jerzy Jaśkuć's project 
repository](https://github.com/EZCodes/SPIN-PromelaRTEMSTestGen).
+
+These files were produced as a part of his research work done in Trinity 
College Dublin in partial fulfilment of the requirements for the degree of MCS 
in Integrated Computer Science.
diff --git a/formal/promela/models/barriers/STATUS.md 
b/formal/promela/models/barriers/STATUS.md
new file mode 100644
index ..5e8f52de
--- /dev/null
+++ b/formal/promela/models/barriers/STATUS.md
@@ -0,0 +1,95 @@
+# BARRIER MANAGER status
+
+## 7th Nov 2022 COMPLETE
+
+* Platform: Dell G5, Ubuntu 20.04.5 LTS
+* Generated: OK
+* Compiles: OK
+* Runs: OK
+* All Tests Pass: OK
+
+See `barriers/archive/20221107-131233`
+
+## 7th Nov 2022 DIAGNOSIS
+
+Test cases 12 and 13 fail because there is a misinterpretation of how the
+maximum number of barriers is determined. The actual configuration is set 
statically
+in `ts-config.h` to be 7, as `TEST_MAXIMUM_BARRIERS`. In `ts-default.h`, this 
is used to set the
+value of `CONFIGURE_MAXIMUM_BARRIERS`. This is not easily changed.
+
+The current Promela model only allows 2 barriers.
+
+## 5th Nov 2022 TEST FAIL
+
+* Platform: Dell G5, Ubuntu 20.04.5 LTS
+* Generated: OK
+* Compiles: OK
+* Runs: OK
+* All Tests Pass: No, 4 fail
+
+Log extract showing all four fails:
+
+```
+:0.19:0:WRK0/PML-BarrierMgr013:tr-barrier-mgr-model-13.c:185:RTEMS_SUCCESSFUL 
== RTEMS_TOO_MANY
+F:*:0:RUN:*:*:RTEMS barrier leak (1)
+E:RtemsModelBarrierMgr13:N:33:F:2:D:0.011053
+
+F:0.21:0:WRK0/PML-BarrierMgr012:tr-barrier-mgr-model-12.c:203:RTEMS_SUCCESSFUL 
== RTEMS_TOO_MANY
+F:*:0:RUN:*:*:RTEMS barrier leak (1)
+E:RtemsModelBarrierMgr12:N:36:F:2:D:0.011254
+```
+
+# 4th Nov 2022 TEST FAIL
+
+* Platform: Dell G5, Ubuntu 20.04.5 LTS
+* Generated: OK
+* Compiles: OK
+* Runs: OK
+* All Tests Pass: No, 27 fail
+
+Log extract showing representative sample:
+
+```
+F:0.7:0:RUN/PML-BarrierMgr000:tr-barrier-mgr-model-9.c:332:1 == 4
+F:*:0:RUN:*:*:Wrong runner priority, expected 1, actual 4
+E:RtemsModelBarrierMgr9:N:33:F:2:D:0.012084
+
+F:*:0:RUN:*:*:Wrong runner priority, expected 1, actual 4
+E:RtemsModelBarrierMgr8:N:36:F:1:D:0.012003
+
+F:*:0:RUN:*:*:Wrong runner priority, expected 1, actual 4
+E:RtemsModelBarrierMgr14:N:37:F:1:D:0.012264
+
+F:0.19:0:WRK0/PML-BarrierMgr013:tr-barrier-mgr-model-13.c:185:RTEMS_SUCCESSFUL 
== RTEMS_TOO_MANY
+F:*:0:RUN:*:*:RTEMS barrier leak (1)
+F:*:0:RUN:*:*:Wrong runner priority, expected 1, actual 4
+E:RtemsModelBarrierMgr13:N:33:F:3:D:0.011301
+
+F:0.21:0:WRK0/PML-BarrierMgr012:tr-barrier-mgr-model-12.c:203:RTEMS_SUCCESSFUL 
== RTEMS_TOO_MANY
+F:*:0:RUN:*:*:RTEMS barrier leak (1)
+F:*:0:RUN:*:*:Wrong runner priority, expected 1, actual 4
+E:RtemsModelBarrierMgr12:N:36:F:3:D:0.011563
+
+F:*:0:RUN:*:*:Wrong runner priority, expected 1, actual 4
+E:RtemsModelBarrierMgr0:N:36:F:1:D:0.009776
+Z:Model0:C:22:N:757:F:27:D:0.246403
+Y:ReportHash:SHA256:H_j2zroRO1RaYJR3cZx9Bn68EfP5EBnpXZej6By5tIU=
+cpu

[PATCH 04/18] adds chains API model

2022-12-22 Thread andrew.butterfi...@scss.tcd.ie 


---
 formal/promela/models/chains/.gitignore   |   1 +
 formal/promela/models/chains/STATUS.md|  11 +
 .../models/chains/chains-api-model-post.h |   3 +
 .../models/chains/chains-api-model-pre.h  |  43 
 .../models/chains/chains-api-model-rfn.yml|  64 ++
 .../models/chains/chains-api-model-run.h  |  18 ++
 .../models/chains/chains-api-model.pml| 203 ++
 .../models/chains/tr-chains-api-model.c   |  70 ++
 .../models/chains/tr-chains-api-model.h   |  57 +
 9 files changed, 470 insertions(+)
 create mode 100644 formal/promela/models/chains/.gitignore
 create mode 100644 formal/promela/models/chains/STATUS.md
 create mode 100644 formal/promela/models/chains/chains-api-model-post.h
 create mode 100644 formal/promela/models/chains/chains-api-model-pre.h
 create mode 100644 formal/promela/models/chains/chains-api-model-rfn.yml
 create mode 100644 formal/promela/models/chains/chains-api-model-run.h
 create mode 100644 formal/promela/models/chains/chains-api-model.pml
 create mode 100644 formal/promela/models/chains/tr-chains-api-model.c
 create mode 100644 formal/promela/models/chains/tr-chains-api-model.h

diff --git a/formal/promela/models/chains/.gitignore 
b/formal/promela/models/chains/.gitignore
new file mode 100644
index ..daa24295
--- /dev/null
+++ b/formal/promela/models/chains/.gitignore
@@ -0,0 +1 @@
+tr-model-chains-api-*.c
diff --git a/formal/promela/models/chains/STATUS.md 
b/formal/promela/models/chains/STATUS.md
new file mode 100644
index ..e45cc5d3
--- /dev/null
+++ b/formal/promela/models/chains/STATUS.md
@@ -0,0 +1,11 @@
+# CHAINS API status
+
+## 3rd Nov 2022 COMPLETE
+
+* Platform: Dell G5, Ubuntu 20.04.5 LTS
+* Generated: OK
+* Compiles: OK
+* Runs: OK
+* All Tests Pass: OK
+
+See `chains/archive/20221103-163702`
diff --git a/formal/promela/models/chains/chains-api-model-post.h 
b/formal/promela/models/chains/chains-api-model-post.h
new file mode 100644
index ..d826725d
--- /dev/null
+++ b/formal/promela/models/chains/chains-api-model-post.h
@@ -0,0 +1,3 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/* post-amble empty for now */
diff --git a/formal/promela/models/chains/chains-api-model-pre.h 
b/formal/promela/models/chains/chains-api-model-pre.h
new file mode 100644
index ..9816a5ad
--- /dev/null
+++ b/formal/promela/models/chains/chains-api-model-pre.h
@@ -0,0 +1,43 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/**
+ * Chains API Model
+ *
+ * Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+ *
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * * Redistributions of source code must retain the above copyright
+ *   notice, this list of conditions and the following disclaimer.
+ *
+ * * Redistributions in binary form must reproduce the above
+ *   copyright notice, this list of conditions and the following
+ *   disclaimer in the documentation and/or other materials provided
+ *   with the distribution.
+ *
+ * * Neither the name of the copyright holders nor the names of its
+ *   contributors may be used to endorse or promote products derived
+ *   from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ 
**/
+
+
+#include 
+#include 
+#include 
+#include "tr-chains-api-model.h"
diff --git a/formal/promela/models/chains/chains-api-model-rfn.yml 
b/formal/promela/models/chains/chains-api-model-rfn.yml
new file mode 100644
index ..103e32ce
--- /dev/null
+++ b/formal/promela/models/chains/chains-api-model-rfn.yml
@@ -0,0 +1,64 @@
+# SPDX-License-Identifier: BSD-2-Clause
+# Event Manager: Promela to RTEMS Refinement
+
+# Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+#
+# Redistribution and use in source and binary forms, with or without
+# modification, are permitted provided that the following conditions
+# are met:
+# 1. Re

[PATCH 06/18] adds event manager model

2022-12-22 Thread andrew.butterfi...@scss.tcd.ie 



---
 formal/promela/models/events/.gitignore   |   1 +
 formal/promela/models/events/STATUS.md|  21 +
 .../models/events/event-mgr-model-post.h  |   8 +
 .../models/events/event-mgr-model-pre.h   |  51 ++
 .../models/events/event-mgr-model-rfn.yml | 182 
 .../models/events/event-mgr-model-run.h   | 164 
 .../promela/models/events/event-mgr-model.pml | 848 ++
 .../models/events/tc-event-mgr-model.c| 358 
 .../models/events/tr-event-mgr-model.c| 257 ++
 .../models/events/tr-event-mgr-model.h| 245 +
 10 files changed, 2135 insertions(+)
 create mode 100644 formal/promela/models/events/.gitignore
 create mode 100644 formal/promela/models/events/STATUS.md
 create mode 100644 formal/promela/models/events/event-mgr-model-post.h
 create mode 100644 formal/promela/models/events/event-mgr-model-pre.h
 create mode 100644 formal/promela/models/events/event-mgr-model-rfn.yml
 create mode 100644 formal/promela/models/events/event-mgr-model-run.h
 create mode 100644 formal/promela/models/events/event-mgr-model.pml
 create mode 100644 formal/promela/models/events/tc-event-mgr-model.c
 create mode 100644 formal/promela/models/events/tr-event-mgr-model.c
 create mode 100644 formal/promela/models/events/tr-event-mgr-model.h

diff --git a/formal/promela/models/events/.gitignore 
b/formal/promela/models/events/.gitignore
new file mode 100644
index ..a1fcab96
--- /dev/null
+++ b/formal/promela/models/events/.gitignore
@@ -0,0 +1 @@
+tr-model-events-mgr-*.c
diff --git a/formal/promela/models/events/STATUS.md 
b/formal/promela/models/events/STATUS.md
new file mode 100644
index ..71518926
--- /dev/null
+++ b/formal/promela/models/events/STATUS.md
@@ -0,0 +1,21 @@
+# EVENT MANAGER status
+
+## 7th Nov 2022 COMPLETE
+
+* Platform: Dell G5, Ubuntu 20.04.5 LTS
+* Generated: OK
+* Compiles: OK
+* Runs: OK
+* All Tests Pass: OK
+
+See `events/archive/20221107-165035`
+
+## 3rd Nov 2022 COMPLETE
+
+* Platform: Dell G5, Ubuntu 20.04.5 LTS
+* Generated: OK
+* Compiles: OK
+* Runs: OK
+* All Tests Pass: OK
+
+See `events/archive/20221103-165851`
diff --git a/formal/promela/models/events/event-mgr-model-post.h 
b/formal/promela/models/events/event-mgr-model-post.h
new file mode 100644
index ..df2738a4
--- /dev/null
+++ b/formal/promela/models/events/event-mgr-model-post.h
@@ -0,0 +1,8 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+static void Runner( RtemsModelEventsMgr_Context *ctx )
+{
+  T_log( T_NORMAL, "Runner running" );
+  TestSegment4( ctx );
+  T_log( T_NORMAL, "Runner finished" );
+}
diff --git a/formal/promela/models/events/event-mgr-model-pre.h 
b/formal/promela/models/events/event-mgr-model-pre.h
new file mode 100644
index ..9a764a82
--- /dev/null
+++ b/formal/promela/models/events/event-mgr-model-pre.h
@@ -0,0 +1,51 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/**
+ * @file
+ *
+ * @ingroup RTEMSTestCaseRtemsModelEventsMgr
+ */
+
+/*
+ * Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de)
+ *Trinity College Dublin (http://www.tcd.ie)
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ * 1. Redistributions of source code must retain the above copyright
+ *notice, this list of conditions and the following disclaimer.
+ * 2. Redistributions in binary form must reproduce the above copyright
+ *notice, this list of conditions and the following disclaimer in the
+ *documentation and/or other materials provided with the distribution.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
+ * POSSIBILITY OF SUCH DAMAGE.
+ */
+
+/*
+ * This file was automatically generated.  Do not edit it manually.
+ * Please have a look at
+ *
+ * https://docs.rtems.org/branches/master/eng/req/howto.html
+ *
+ * for information how to maintain and re-generate this file.
+ */
+
+#ifndef HAVE_CONFIG_H
+#include "config.h"
+#endif
+
+#include 
+
+
+#include "tr-event-mgr-model.h"
diff --git a/formal/promela/models/events/event-mgr-model-rfn.yml 
b/formal/promela/models/events/event-mgr-model-rfn.yml
new file mode 100644
index ..96727b88
--- /dev/null
+

[PATCH 08/18] adds message manager model

2022-12-22 Thread andrew.butterfi...@scss.tcd.ie 



>From 4364f65705b387697c33181cb8a9a7b772ea7f58 Mon Sep 17 00:00:00 2001
From: Andrew Butterfield 
Date: Wed, 21 Dec 2022 16:31:40 +
Subject: [PATCH 08/18] adds message manager model

---
 formal/promela/models/messages/README.md  |  10 +
 formal/promela/models/messages/STATUS.md  |  14 +
 .../models/messages/msg-mgr-model-post.h  |   8 +
 .../models/messages/msg-mgr-model-pre.h   |  51 ++
 .../models/messages/msg-mgr-model-rfn.yml | 202 +
 .../models/messages/msg-mgr-model-run.h   | 191 
 .../promela/models/messages/msg-mgr-model.pml | 842 ++
 .../models/messages/tc-msg-mgr-model.c| 211 +
 .../models/messages/tr-msg-mgr-model.c| 240 +
 .../models/messages/tr-msg-mgr-model.h| 132 +++
 10 files changed, 1901 insertions(+)
 create mode 100644 formal/promela/models/messages/README.md
 create mode 100644 formal/promela/models/messages/STATUS.md
 create mode 100644 formal/promela/models/messages/msg-mgr-model-post.h
 create mode 100644 formal/promela/models/messages/msg-mgr-model-pre.h
 create mode 100644 formal/promela/models/messages/msg-mgr-model-rfn.yml
 create mode 100644 formal/promela/models/messages/msg-mgr-model-run.h
 create mode 100644 formal/promela/models/messages/msg-mgr-model.pml
 create mode 100644 formal/promela/models/messages/tc-msg-mgr-model.c
 create mode 100644 formal/promela/models/messages/tr-msg-mgr-model.c
 create mode 100644 formal/promela/models/messages/tr-msg-mgr-model.h

diff --git a/formal/promela/models/messages/README.md 
b/formal/promela/models/messages/README.md
new file mode 100644
index ..2eb723b5
--- /dev/null
+++ b/formal/promela/models/messages/README.md
@@ -0,0 +1,10 @@
+# Message Manager model
+
+Developer: Eoin Lynch
+
+This directory contains the code for the generation/running of tests for the 
[RTEMS Message 
Manager](https://docs.rtems.org/branches/master/c-user/message/index.html)
+
+It is a subset of the material available at [Eoin Lynch's project 
repository](https://github.com/lynche12/SPIN-PromelaTestGeneration).
+
+This project is research work done for his dissertation as part of the MAI in 
Computer Engineering program at Trinity College Dublin
+
diff --git a/formal/promela/models/messages/STATUS.md 
b/formal/promela/models/messages/STATUS.md
new file mode 100644
index ..361984c6
--- /dev/null
+++ b/formal/promela/models/messages/STATUS.md
@@ -0,0 +1,14 @@
+# MESSAGE MANAGER status
+
+## 3rd Nov 2022 TEST FAIL
+
+* Platform: Dell G5, Ubuntu 20.04.5 LTS
+* Generated: OK
+* Compiles: OK
+* Runs: OK
+* All Tests Pass: NO, 1 failure
+```
+F:0.17:0:"x/PML-MessageMgr022:tr-msg-mgr-model-22.c:192:RTEMS_SUCCESSFUL == 
RTEMS_TIMEOUT
+```
+
+See `events/archive/20221103-170322`
diff --git a/formal/promela/models/messages/msg-mgr-model-post.h 
b/formal/promela/models/messages/msg-mgr-model-post.h
new file mode 100644
index ..9a9606d3
--- /dev/null
+++ b/formal/promela/models/messages/msg-mgr-model-post.h
@@ -0,0 +1,8 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+static void Runner( RtemsModelMessageMgr_Context *ctx )
+{
+  T_log( T_NORMAL, "Runner running" );
+  TestSegment3( ctx );
+  T_log( T_NORMAL, "Runner finished" );
+}
diff --git a/formal/promela/models/messages/msg-mgr-model-pre.h 
b/formal/promela/models/messages/msg-mgr-model-pre.h
new file mode 100644
index ..f3986267
--- /dev/null
+++ b/formal/promela/models/messages/msg-mgr-model-pre.h
@@ -0,0 +1,51 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/**
+ * @file
+ *
+ * @ingroup RTEMSTestCaseRtemsModelMessageMgr
+ */
+
+/*
+ * Copyright (C) 2020 embedded brains GmbH (http://www.embedded-brains.de)
+ *Trinity College Dublin (http://www.tcd.ie)
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions
+ * are met:
+ * 1. Redistributions of source code must retain the above copyright
+ *notice, this list of conditions and the following disclaimer.
+ * 2. Redistributions in binary form must reproduce the above copyright
+ *notice, this list of conditions and the following disclaimer in the
+ *documentation and/or other materials provided with the distribution.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+ * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+ * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
+ * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
+ * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
+ * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
+ * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
+ * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
+ * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
+ * ARISING IN ANY WAY OUT OF

[PATCH 10/18] adds weak memory models

2022-12-22 Thread andrew.butterfi...@scss.tcd.ie 



---
 .../models/threadq/Weak-Memory/RAM.pml|  48 +
 .../models/threadq/Weak-Memory/SPARC-TSO.pml  | 198 ++
 .../threadq/Weak-Memory/memory_model.pml  |  60 ++
 .../models/threadq/Weak-Memory/wmemory.pml|  74 +++
 4 files changed, 380 insertions(+)
 create mode 100644 formal/promela/models/threadq/Weak-Memory/RAM.pml
 create mode 100644 formal/promela/models/threadq/Weak-Memory/SPARC-TSO.pml
 create mode 100644 formal/promela/models/threadq/Weak-Memory/memory_model.pml
 create mode 100644 formal/promela/models/threadq/Weak-Memory/wmemory.pml

diff --git a/formal/promela/models/threadq/Weak-Memory/RAM.pml 
b/formal/promela/models/threadq/Weak-Memory/RAM.pml
new file mode 100644
index ..70851917
--- /dev/null
+++ b/formal/promela/models/threadq/Weak-Memory/RAM.pml
@@ -0,0 +1,48 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/**
+ * RAM
+ *
+ * Copyright (C) 2021 Trinity College Dublin (www.tcd.ie)
+ *
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * * Redistributions of source code must retain the above copyright
+ *   notice, this list of conditions and the following disclaimer.
+ *
+ * * Redistributions in binary form must reproduce the above
+ *   copyright notice, this list of conditions and the following
+ *   disclaimer in the documentation and/or other materials provided
+ *   with the distribution.
+ *
+ * * Neither the name of the copyright holders nor the names of its
+ *   contributors may be used to endorse or promote products derived
+ *   from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ 
**/
+
+#ifndef _FORMAL_MEMORY_RAM
+#define _FORMAL_MEMORY_RAM
+
+
+// We assume a byte-memory
+#define MEM_SIZE 8
+byte memory[MEM_SIZE] ;
+
+
+#endif
diff --git a/formal/promela/models/threadq/Weak-Memory/SPARC-TSO.pml 
b/formal/promela/models/threadq/Weak-Memory/SPARC-TSO.pml
new file mode 100644
index ..d47e1284
--- /dev/null
+++ b/formal/promela/models/threadq/Weak-Memory/SPARC-TSO.pml
@@ -0,0 +1,198 @@
+/* SPDX-License-Identifier: BSD-2-Clause */
+
+/**
+ * SPARC-TSO.pml
+ *
+ * Copyright (C) 2021 Trinity College Dublin (www.tcd.ie)
+ *
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * * Redistributions of source code must retain the above copyright
+ *   notice, this list of conditions and the following disclaimer.
+ *
+ * * Redistributions in binary form must reproduce the above
+ *   copyright notice, this list of conditions and the following
+ *   disclaimer in the documentation and/or other materials provided
+ *   with the distribution.
+ *
+ * * Neither the name of the copyright holders nor the names of its
+ *   contributors may be used to endorse or promote products derived
+ *   from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ 
**

[PATCH 12/18] third party code - promela parser

2022-12-22 Thread andrew.butterfi...@scss.tcd.ie 

forked from https://github.com/johnyf/promela,
commit 32d14184a50e920a92201058e4f601329be8c9c7
---
 .../src/src/modules/promela_yacc/.gitignore   |   20 +
 .../src/src/modules/promela_yacc/.travis.yml  |   21 +
 .../src/src/modules/promela_yacc/LICENSE  |   31 +
 .../src/src/modules/promela_yacc/MANIFEST.in  |4 +
 .../src/src/modules/promela_yacc/README.md|   27 +
 .../src/src/modules/promela_yacc/doc.md   |  100 ++
 .../modules/promela_yacc/promela/__init__.py  |6 +
 .../src/modules/promela_yacc/promela/ast.py   | 1035 +
 .../src/modules/promela_yacc/promela/lex.py   |  211 
 .../src/modules/promela_yacc/promela/yacc.py  |  955 +++
 .../src/src/modules/promela_yacc/setup.py |   65 ++
 .../modules/promela_yacc/tests/yacc_test.py   |  759 
 12 files changed, 3234 insertions(+)
 create mode 100644 formal/promela/src/src/modules/promela_yacc/.gitignore
 create mode 100644 formal/promela/src/src/modules/promela_yacc/.travis.yml
 create mode 100644 formal/promela/src/src/modules/promela_yacc/LICENSE
 create mode 100644 formal/promela/src/src/modules/promela_yacc/MANIFEST.in
 create mode 100644 formal/promela/src/src/modules/promela_yacc/README.md
 create mode 100644 formal/promela/src/src/modules/promela_yacc/doc.md
 create mode 100644 
formal/promela/src/src/modules/promela_yacc/promela/__init__.py
 create mode 100644 formal/promela/src/src/modules/promela_yacc/promela/ast.py
 create mode 100644 formal/promela/src/src/modules/promela_yacc/promela/lex.py
 create mode 100644 formal/promela/src/src/modules/promela_yacc/promela/yacc.py
 create mode 100644 formal/promela/src/src/modules/promela_yacc/setup.py
 create mode 100644 
formal/promela/src/src/modules/promela_yacc/tests/yacc_test.py

diff --git a/formal/promela/src/src/modules/promela_yacc/.gitignore 
b/formal/promela/src/src/modules/promela_yacc/.gitignore
new file mode 100644
index ..f4cd3f85
--- /dev/null
+++ b/formal/promela/src/src/modules/promela_yacc/.gitignore
@@ -0,0 +1,20 @@
+build/*
+dist/*
+promela/_version.py
+*parsetab.py
+.coverage
+.DS_Store
+Icon?
+
+*.*~
+__pycache__
+*.pyc
+*.swp
+*.pdf
+*.PDF
+*.txt
+*.log
+*.egg-info
+*.html
+*.css
+
diff --git a/formal/promela/src/src/modules/promela_yacc/.travis.yml 
b/formal/promela/src/src/modules/promela_yacc/.travis.yml
new file mode 100644
index ..2fee40c9
--- /dev/null
+++ b/formal/promela/src/src/modules/promela_yacc/.travis.yml
@@ -0,0 +1,21 @@
+language: python
+
+python:
+  - 2.7
+  - 3.4
+  - 3.5
+  - 3.6
+
+install:
+  - sudo apt-get update -qq
+  - sudo apt-get install -y graphviz
+  - pip install --upgrade pip setuptools
+  - pip install -r requirements.txt
+  - pip install .
+
+script:
+  - cd tests/
+  - nosetests --with-coverage --cover-package=promela
+
+after_success:
+  - coveralls
diff --git a/formal/promela/src/src/modules/promela_yacc/LICENSE 
b/formal/promela/src/src/modules/promela_yacc/LICENSE
new file mode 100644
index ..bebe3694
--- /dev/null
+++ b/formal/promela/src/src/modules/promela_yacc/LICENSE
@@ -0,0 +1,31 @@
+Copyright (c) 2014-2018 by California Institute of Technology
+Copyright (c) 2014-2018 by Ioannis Filippidis
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the California Institute of Technology nor
+   the names of its contributors may be used to endorse or promote
+   products derived from this software without specific prior
+   written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL CALTECH OR THE
+CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL,
+EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO,
+PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
+PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF
+LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING
+NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/formal/promela/src/src/modules/promela_yacc/MANIFEST.in 
b/formal/promela/src/src/modules/promela_yacc/MANIFEST.in
new file mode 100644
index ..bbacf5bf
--- /dev/null
+++ b/formal/promela/src/src/modules/promela_yacc/MANIFEST.in
@@ -0,0 +1,4 @@
+include tests/*.py

[PATCH 13/18] modifies 3rd party code - promela parser

2022-12-22 Thread andrew.butterfi...@scss.tcd.ie 



---
 .../src/src/modules/promela_yacc/.gitignore   |  20 -
 .../src/src/modules/promela_yacc/.travis.yml  |  21 -
 .../src/src/modules/promela_yacc/LICENSE  |   1 +
 .../src/src/modules/promela_yacc/MANIFEST.in  |   4 -
 .../src/src/modules/promela_yacc/doc.md   | 100 ---
 .../src/modules/promela_yacc/promela/ast.py   | 120 ++-
 .../src/modules/promela_yacc/promela/lex.py   |  18 +-
 .../src/modules/promela_yacc/promela/yacc.py  | 207 +++--
 .../modules/promela_yacc/tests/yacc_test.py   | 759 --
 9 files changed, 228 insertions(+), 1022 deletions(-)
 delete mode 100644 formal/promela/src/src/modules/promela_yacc/.gitignore
 delete mode 100644 formal/promela/src/src/modules/promela_yacc/.travis.yml
 delete mode 100644 formal/promela/src/src/modules/promela_yacc/MANIFEST.in
 delete mode 100644 formal/promela/src/src/modules/promela_yacc/doc.md
 delete mode 100644 
formal/promela/src/src/modules/promela_yacc/tests/yacc_test.py

diff --git a/formal/promela/src/src/modules/promela_yacc/.gitignore 
b/formal/promela/src/src/modules/promela_yacc/.gitignore
deleted file mode 100644
index f4cd3f85..
--- a/formal/promela/src/src/modules/promela_yacc/.gitignore
+++ /dev/null
@@ -1,20 +0,0 @@
-build/*
-dist/*
-promela/_version.py
-*parsetab.py
-.coverage
-.DS_Store
-Icon?
-
-*.*~
-__pycache__
-*.pyc
-*.swp
-*.pdf
-*.PDF
-*.txt
-*.log
-*.egg-info
-*.html
-*.css
-
diff --git a/formal/promela/src/src/modules/promela_yacc/.travis.yml 
b/formal/promela/src/src/modules/promela_yacc/.travis.yml
deleted file mode 100644
index 2fee40c9..
--- a/formal/promela/src/src/modules/promela_yacc/.travis.yml
+++ /dev/null
@@ -1,21 +0,0 @@
-language: python
-
-python:
-  - 2.7
-  - 3.4
-  - 3.5
-  - 3.6
-
-install:
-  - sudo apt-get update -qq
-  - sudo apt-get install -y graphviz
-  - pip install --upgrade pip setuptools
-  - pip install -r requirements.txt
-  - pip install .
-
-script:
-  - cd tests/
-  - nosetests --with-coverage --cover-package=promela
-
-after_success:
-  - coveralls
diff --git a/formal/promela/src/src/modules/promela_yacc/LICENSE 
b/formal/promela/src/src/modules/promela_yacc/LICENSE
index bebe3694..40f0a792 100644
--- a/formal/promela/src/src/modules/promela_yacc/LICENSE
+++ b/formal/promela/src/src/modules/promela_yacc/LICENSE
@@ -1,3 +1,4 @@
+Copyright (c) 2019-2021 by Trinity College Dublin, Ireland
 Copyright (c) 2014-2018 by California Institute of Technology
 Copyright (c) 2014-2018 by Ioannis Filippidis
 All rights reserved.
diff --git a/formal/promela/src/src/modules/promela_yacc/MANIFEST.in 
b/formal/promela/src/src/modules/promela_yacc/MANIFEST.in
deleted file mode 100644
index bbacf5bf..
--- a/formal/promela/src/src/modules/promela_yacc/MANIFEST.in
+++ /dev/null
@@ -1,4 +0,0 @@
-include tests/*.py
-include README.md
-include LICENSE
-include doc.md
diff --git a/formal/promela/src/src/modules/promela_yacc/doc.md 
b/formal/promela/src/src/modules/promela_yacc/doc.md
deleted file mode 100644
index 02d73431..
--- a/formal/promela/src/src/modules/promela_yacc/doc.md
+++ /dev/null
@@ -1,100 +0,0 @@
-This package provides a lexer, parser, and abstract syntax tree (AST) for the 
[Promela](http://en.wikipedia.org/wiki/Promela) modeling language.
-The lexer and parser are generated using 
[PLY](https://pypi.python.org/pypi/ply/3.4) (Python `lex`-`yacc`).
-The [grammar](http://spinroot.com/spin/Man/grammar.html) is based on that used 
in the [SPIN](http://spinroot.com/spin/whatispin.html) model checker (in the 
files `spin.y` and `spinlex.c` of SPIN's source distribution), with 
modifications where needed.
-
-To instantiate a Promela parser:
-
-```python
-from promela.yacc import Parser
-parser = Parser()
-```
-
-Then Promela code, as a string, can be parsed by:
-
-```python
-s = '''
-active proctype foo(){
-   int x;
-   do
-   :: x = x + 1;
-   od
-}
-'''
-program = parser.parse(s)
-```
-
-then
-
-```python
->>> print(program)
-active [1]  proctype foo(){
-   int x
-   do
-   :: x = (x + 1)
-   od;
-}
-```
-
-The parser returns the result as an abstract syntax tree using classes from 
the `promela.ast` module.
-The top production rule returns a `Program` instance, which itself is a `list`.
-The contents of this list
-
-There are two categories of AST classes: those that represent control flow 
constructs:
-
-- `Proctype`, (`Init`, `NeverClaim`), `Node`, (`Expression`, `Assignment`, 
`Assert`, `Options` (if, do), `Else`, `Break`, `Goto`, `Label`, `Call`, 
`Return`, `Run`), `Sequence`
-
-and those that represent only syntax inside an expression:
-
-- `Terminal`, (`VarRef`, `Integer`, `Bool`), `Operator`, (`Binary`, `Unary`)
-
-The classes in parentheses are subclasses of the last class preceding the 
parentheses.
-Each control flow class has a method `to_pg` that recursively converts the 
abstract syntax tree to a program graph.
-
-A program graph is a directed graph whose edges are labeled with statements 
from the program.

[PATCH 14/18] third party code - comment filter

2022-12-22 Thread andrew.butterfi...@scss.tcd.ie 


forked from https://github.com/quic/comment-filter/commits/master
commit 9cfb52318e5f71af56b5808e280a9b089b9abc32
---
 .../comment-filter/.circleci/config.yml   |   9 +
 .../src/modules/comment-filter/.coveragerc|   2 +
 .../src/src/modules/comment-filter/.gitignore | 104 +
 .../src/src/modules/comment-filter/AUTHORS|   7 +
 .../modules/comment-filter/CODE-OF-CONDUCT.md |  73 +++
 .../modules/comment-filter/CONTRIBUTING.md|  87 
 .../src/src/modules/comment-filter/Dockerfile |   9 +
 .../src/src/modules/comment-filter/LICENSE|  13 +
 .../src/modules/comment-filter/MANIFEST.in|   7 +
 .../src/src/modules/comment-filter/README.md  | 158 +++
 .../src/modules/comment-filter/bin/comments   |  25 ++
 .../comment-filter/bin/testdata/hello.c   |   8 +
 .../comment-filter/comment_filter/__init__.py |   1 +
 .../comment-filter/comment_filter/_version.py |   0
 .../comment-filter/comment_filter/language.py |  60 +++
 .../comment-filter/comment_filter/rfc.py  | 423 ++
 .../comment-filter/comment_filter/rfc_test.py | 258 +++
 .../src/src/modules/comment-filter/setup.cfg  |   5 +
 .../src/src/modules/comment-filter/setup.py   |  12 +
 .../src/src/modules/comment-filter/tox.ini|  12 +
 20 files changed, 1273 insertions(+)
 create mode 100644 
formal/promela/src/src/modules/comment-filter/.circleci/config.yml
 create mode 100644 formal/promela/src/src/modules/comment-filter/.coveragerc
 create mode 100644 formal/promela/src/src/modules/comment-filter/.gitignore
 create mode 100644 formal/promela/src/src/modules/comment-filter/AUTHORS
 create mode 100644 
formal/promela/src/src/modules/comment-filter/CODE-OF-CONDUCT.md
 create mode 100644 
formal/promela/src/src/modules/comment-filter/CONTRIBUTING.md
 create mode 100644 formal/promela/src/src/modules/comment-filter/Dockerfile
 create mode 100644 formal/promela/src/src/modules/comment-filter/LICENSE
 create mode 100644 formal/promela/src/src/modules/comment-filter/MANIFEST.in
 create mode 100644 formal/promela/src/src/modules/comment-filter/README.md
 create mode 100755 formal/promela/src/src/modules/comment-filter/bin/comments
 create mode 100644 
formal/promela/src/src/modules/comment-filter/bin/testdata/hello.c
 create mode 100644 
formal/promela/src/src/modules/comment-filter/comment_filter/__init__.py
 create mode 100644 
formal/promela/src/src/modules/comment-filter/comment_filter/_version.py
 create mode 100644 
formal/promela/src/src/modules/comment-filter/comment_filter/language.py
 create mode 100644 
formal/promela/src/src/modules/comment-filter/comment_filter/rfc.py
 create mode 100644 
formal/promela/src/src/modules/comment-filter/comment_filter/rfc_test.py
 create mode 100644 formal/promela/src/src/modules/comment-filter/setup.cfg
 create mode 100644 formal/promela/src/src/modules/comment-filter/setup.py
 create mode 100644 formal/promela/src/src/modules/comment-filter/tox.ini

diff --git a/formal/promela/src/src/modules/comment-filter/.circleci/config.yml 
b/formal/promela/src/src/modules/comment-filter/.circleci/config.yml
new file mode 100644
index ..dc96c5c2
--- /dev/null
+++ b/formal/promela/src/src/modules/comment-filter/.circleci/config.yml
@@ -0,0 +1,9 @@
+version: 2
+jobs:
+  build:
+docker:
+  - image: themattrix/tox
+steps:
+  - checkout
+  - run:
+ command: tox
diff --git a/formal/promela/src/src/modules/comment-filter/.coveragerc 
b/formal/promela/src/src/modules/comment-filter/.coveragerc
new file mode 100644
index ..9b6154a0
--- /dev/null
+++ b/formal/promela/src/src/modules/comment-filter/.coveragerc
@@ -0,0 +1,2 @@
+[run]
+omit = *_test.py
diff --git a/formal/promela/src/src/modules/comment-filter/.gitignore 
b/formal/promela/src/src/modules/comment-filter/.gitignore
new file mode 100644
index ..af2f5375
--- /dev/null
+++ b/formal/promela/src/src/modules/comment-filter/.gitignore
@@ -0,0 +1,104 @@
+# Byte-compiled / optimized / DLL files
+__pycache__/
+*.py[cod]
+*$py.class
+
+# C extensions
+*.so
+
+# Distribution / packaging
+.Python
+build/
+develop-eggs/
+dist/
+downloads/
+eggs/
+.eggs/
+lib/
+lib64/
+parts/
+sdist/
+var/
+wheels/
+*.egg-info/
+.installed.cfg
+*.egg
+MANIFEST
+
+# PyInstaller
+#  Usually these files are written by a python script from a template
+#  before PyInstaller builds the exe, so as to inject date/other infos into it.
+*.manifest
+*.spec
+
+# Installer logs
+pip-log.txt
+pip-delete-this-directory.txt
+
+# Unit test / coverage reports
+htmlcov/
+.tox/
+.coverage
+.coverage.*
+.cache
+nosetests.xml
+coverage.xml
+*.cover
+.hypothesis/
+
+# Translations
+*.mo
+*.pot
+
+# Django stuff:
+*.log
+.static_storage/
+.media/
+local_settings.py
+
+# Flask stuff:
+instance/
+.webassets-cache
+
+# Scrapy stuff:
+.scrapy
+
+# Sphinx documentation
+docs/_build/
+
+# PyBuilder
+target/
+
+# Jupyter Notebook
+.ipynb_checkpoints
+
+# pyenv
+.python-version
+
+# celery beat schedule file
+celerybeat-schedule
+

[PATCH 15/18] modifies 3rd party code - comment filter

2022-12-22 Thread andrew.butterfi...@scss.tcd.ie 

---
 .../comment-filter/.circleci/config.yml   |   9 -
 .../src/modules/comment-filter/.coveragerc|   2 -
 .../src/src/modules/comment-filter/.gitignore | 104 ---
 .../modules/comment-filter/CODE-OF-CONDUCT.md |  73 -
 .../modules/comment-filter/CONTRIBUTING.md|  87 --
 .../src/src/modules/comment-filter/Dockerfile |   9 -
 .../src/src/modules/comment-filter/LICENSE|   4 +-
 .../src/modules/comment-filter/MANIFEST.in|   7 -
 .../src/modules/comment-filter/bin/comments   |  25 --
 .../comment-filter/bin/testdata/hello.c   |   8 -
 .../comment-filter/comment_filter/_version.py |   0
 .../comment-filter/comment_filter/language.py |  14 +-
 .../comment-filter/comment_filter/rfc.py  |  62 +++--
 .../comment-filter/comment_filter/rfc_test.py | 258 --
 14 files changed, 42 insertions(+), 620 deletions(-)
 delete mode 100644 
formal/promela/src/src/modules/comment-filter/.circleci/config.yml
 delete mode 100644 formal/promela/src/src/modules/comment-filter/.coveragerc
 delete mode 100644 formal/promela/src/src/modules/comment-filter/.gitignore
 delete mode 100644 
formal/promela/src/src/modules/comment-filter/CODE-OF-CONDUCT.md
 delete mode 100644 
formal/promela/src/src/modules/comment-filter/CONTRIBUTING.md
 delete mode 100644 formal/promela/src/src/modules/comment-filter/Dockerfile
 delete mode 100644 formal/promela/src/src/modules/comment-filter/MANIFEST.in
 delete mode 100755 formal/promela/src/src/modules/comment-filter/bin/comments
 delete mode 100644 
formal/promela/src/src/modules/comment-filter/bin/testdata/hello.c
 delete mode 100644 
formal/promela/src/src/modules/comment-filter/comment_filter/_version.py
 delete mode 100644 
formal/promela/src/src/modules/comment-filter/comment_filter/rfc_test.py

diff --git a/formal/promela/src/src/modules/comment-filter/.circleci/config.yml 
b/formal/promela/src/src/modules/comment-filter/.circleci/config.yml
deleted file mode 100644
index dc96c5c2..
--- a/formal/promela/src/src/modules/comment-filter/.circleci/config.yml
+++ /dev/null
@@ -1,9 +0,0 @@
-version: 2
-jobs:
-  build:
-docker:
-  - image: themattrix/tox
-steps:
-  - checkout
-  - run:
- command: tox
diff --git a/formal/promela/src/src/modules/comment-filter/.coveragerc 
b/formal/promela/src/src/modules/comment-filter/.coveragerc
deleted file mode 100644
index 9b6154a0..
--- a/formal/promela/src/src/modules/comment-filter/.coveragerc
+++ /dev/null
@@ -1,2 +0,0 @@
-[run]
-omit = *_test.py
diff --git a/formal/promela/src/src/modules/comment-filter/.gitignore 
b/formal/promela/src/src/modules/comment-filter/.gitignore
deleted file mode 100644
index af2f5375..
--- a/formal/promela/src/src/modules/comment-filter/.gitignore
+++ /dev/null
@@ -1,104 +0,0 @@
-# Byte-compiled / optimized / DLL files
-__pycache__/
-*.py[cod]
-*$py.class
-
-# C extensions
-*.so
-
-# Distribution / packaging
-.Python
-build/
-develop-eggs/
-dist/
-downloads/
-eggs/
-.eggs/
-lib/
-lib64/
-parts/
-sdist/
-var/
-wheels/
-*.egg-info/
-.installed.cfg
-*.egg
-MANIFEST
-
-# PyInstaller
-#  Usually these files are written by a python script from a template
-#  before PyInstaller builds the exe, so as to inject date/other infos into it.
-*.manifest
-*.spec
-
-# Installer logs
-pip-log.txt
-pip-delete-this-directory.txt
-
-# Unit test / coverage reports
-htmlcov/
-.tox/
-.coverage
-.coverage.*
-.cache
-nosetests.xml
-coverage.xml
-*.cover
-.hypothesis/
-
-# Translations
-*.mo
-*.pot
-
-# Django stuff:
-*.log
-.static_storage/
-.media/
-local_settings.py
-
-# Flask stuff:
-instance/
-.webassets-cache
-
-# Scrapy stuff:
-.scrapy
-
-# Sphinx documentation
-docs/_build/
-
-# PyBuilder
-target/
-
-# Jupyter Notebook
-.ipynb_checkpoints
-
-# pyenv
-.python-version
-
-# celery beat schedule file
-celerybeat-schedule
-
-# SageMath parsed files
-*.sage.py
-
-# Environments
-.env
-.venv
-env/
-venv/
-ENV/
-env.bak/
-venv.bak/
-
-# Spyder project settings
-.spyderproject
-.spyproject
-
-# Rope project settings
-.ropeproject
-
-# mkdocs documentation
-/site
-
-# mypy
-.mypy_cache/
diff --git a/formal/promela/src/src/modules/comment-filter/CODE-OF-CONDUCT.md 
b/formal/promela/src/src/modules/comment-filter/CODE-OF-CONDUCT.md
deleted file mode 100644
index 7ef343f5..
--- a/formal/promela/src/src/modules/comment-filter/CODE-OF-CONDUCT.md
+++ /dev/null
@@ -1,73 +0,0 @@
-# Contributor Covenant Code of Conduct
-
-## Our Pledge
-
-In the interest of fostering an open and welcoming environment, we as
-contributors and maintainers pledge to making participation in our project and
-our community a harassment-free experience for everyone, regardless of age, 
body
-size, disability, ethnicity, gender identity and expression, level of 
experience,
-nationality, personal appearance, race, religion, or sexual identity and
-orientation.
-
-## Our Standards
-
-Examples of behavior that contributes to creating a positive environment
-include:
-
-* Using welco

[PATCH 18/18] adds automatic testgen examples

2022-12-22 Thread andrew.butterfi...@scss.tcd.ie 


---
 formal/promela/src/examples/draft/make.sh |  77 +++
 formal/promela/src/examples/draft/parse.pml   | 129 ++
 .../src/examples/model_checker/spin.pml   |   8 ++
 formal/promela/src/examples/requirements.txt  |  35 +
 4 files changed, 249 insertions(+)
 create mode 100644 formal/promela/src/examples/draft/make.sh
 create mode 100644 formal/promela/src/examples/draft/parse.pml
 create mode 100644 formal/promela/src/examples/model_checker/spin.pml
 create mode 100644 formal/promela/src/examples/requirements.txt

diff --git a/formal/promela/src/examples/draft/make.sh 
b/formal/promela/src/examples/draft/make.sh
new file mode 100644
index ..b4da0981
--- /dev/null
+++ b/formal/promela/src/examples/draft/make.sh
@@ -0,0 +1,77 @@
+#!/bin/bash
+
+# SPDX-License-Identifier: BSD-3-Clause
+# Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+
+set -e
+set -x
+
+##
+
+HOME0="$(dirname "$(python3 -c "import os; print(os.path.realpath('$0'))")")"
+cd "$HOME0"
+
+##
+
+pip_check_test='true'
+function pip_check () {
+if [ "$pip_check_test" ] ; then
+   set +e
+   version=$(pip3 show "$1")
+   st="$?"
+   set -e
+   [ "$st" = 0 ] || (echo '`'"pip3 show $1"'`'" failed: "'`'"pip3 install 
$1"'`' && exit "$st")
+
+   version=$(echo "$version" | grep -m 1 Version | cut -d ' ' -f 2)
+set +x
+   [ "$version" = "$2" ] || (echo "$1 version $version installed instead 
of $2: "'`'"pip3 install $1==$2"'`' && echo -n "Continue? (ENTER/CTRL+C): " && 
read)
+set -x
+fi
+}
+
+# The compilation will require the installation of these libraries:
+
+pip_check coconut 1.4.3
+pip_check mypy 0.761
+
+coconut --target 3 library.coco --mypy --ignore-missing-imports 
--allow-redefinition
+coconut --target 3 syntax_pml.coco --mypy --ignore-missing-imports 
--allow-redefinition
+coconut --target 3 syntax_yaml.coco --mypy --ignore-missing-imports 
--allow-redefinition
+coconut --target 3 syntax_ml.coco --mypy --ignore-missing-imports 
--allow-redefinition
+coconut --target 3 refine_command.coco refine_command.py
+coconut --target 3 testgen.coco --mypy --follow-imports silent 
--ignore-missing-imports --allow-redefinition
+
+##
+
+# as well as all dependencies of ( https://github.com/johnyf/promela ):
+
+pip_check promela 0.0.2
+
+# The above command was mainly executed to install dependencies of the package.
+
+## git clone g...@gitlab.scss.tcd.ie:tuongf/promela_yacc.git # see also 
deliverables/FV2-201/wip/ftuong/src_ext
+
+##
+
+# Additionally, we use a library to do various operations on C-style comments 
( https://github.com/codeauroraforum/comment-filter ):
+
+## git clone g...@gitlab.scss.tcd.ie:tuongf/comment-filter.git # see also 
deliverables/FV2-201/wip/ftuong/src_ext
+
+# We also modify $PYTHONPATH (so that the library can be used, at least while 
mypy is executing):
+
+export PYTHONPATH=`pwd`/comment-filter
+
+##
+
+# At run-time, we will need these libraries:
+
+pip_check parsec 3.5
+## apt install spin # 6.4.6+dfsg-2
+
+##
+
+cd -
+
+# Finally, the main execution proceeds as follows:
+
+exec python3 "$HOME0/testgen.py" "$@"
diff --git a/formal/promela/src/examples/draft/parse.pml 
b/formal/promela/src/examples/draft/parse.pml
new file mode 100644
index ..ec86d1fd
--- /dev/null
+++ b/formal/promela/src/examples/draft/parse.pml
@@ -0,0 +1,129 @@
+/**
+ * FV2-201
+ *
+ * Copyright (C) 2019-2021 Trinity College Dublin (www.tcd.ie)
+ *
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * * Redistributions of source code must retain the above copyright
+ *   notice, this list of conditions and the following disclaimer.
+ *
+ * * Redistributions in binary form must reproduce the above
+ *   copyright notice, this list of conditions and the following
+ *   disclaimer in the documentation and/or other materials provided
+ *   with the distribution.
+ *
+ * * Neither the name of the copyright holders nor the names of its
+ *   contributors may be used to endorse or promote products derived
+ *   from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHE

Re: [PATCH 00/18] Adds Formal Verification Material

2023-01-03 Thread andrew.butterfi...@scss.tcd.ie 
Hello Sebastian,

 Yes - I noticed that problem - I got a lot of responses about those emails 
being referred to the moderator.

Some of those blocked patches were adding in archive material. I did this 
because of recent interactions
with the follow-up ESA project looking at Independent Validation and 
Verification (IV&V). They didn't just 
want to see the starting models and final test code and results, but also all 
the intermediate artifacts.
This can be quite a large amount of data. 

On reflection, it may not make much sense to include this stuff 
- rather the proposed new section in the Software Engineering Manual should 
mention the need to make 
such archives available.

I'll do the fork/patch/PR as you suggested (I can leave the archive stuff out - 
it's generated by the tooling anyway).

Best regards, and Happy New Year,

 Andrew



On 03/01/2023, 09:11, "Sebastian Huber" mailto:sebastian.hu...@embedded-brains.de>> wrote:


Hello Andrew,


On 22/12/2022 12:29, andrew.butterfi...@scss.tcd.ie 
<mailto:andrew.butterfi...@scss.tcd.ie> wrote:
> From 3390ccc51f46ce0a4baa60422a62530c7c3c29bd Mon Sep 17 00:00:00 2001
> From: Andrew Butterfield <mailto:andrew.butterfi...@scss.tcd.ie>>
> Date: Wed, 21 Dec 2022 18:03:47 +
> Subject: [PATCH 00/18] Adds Formal Verification Material
> 
> This patch-set adds in the Promela/SPIN models and tools developed as part of
> the ESA-sponsored activity "Qualification of RTEMS Symmetric Multiprocessing
> (SMP)" as well as result of ongoing contributions by students at Trinity 
> College
> Dublin to improve and extend them.
> 
> It is a subset of the material contained at
> https://github.com/andrewbutterfield/RTEMS-SMP-Formal 
> <https://github.com/andrewbutterfield/RTEMS-SMP-Formal>
> 
> It focusses in the main on what currently produces RTEMS test code.


thanks for the patch set. I was about to review it and noticed that not 
all patches did show up on the mailing list probably due to the mailing 
list size limit.


I added the rtems-central repository to the Github site:


https://github.com/RTEMS/rtems-central <https://github.com/RTEMS/rtems-central>


Could you please fork this repository, add a branch with your patches to 
your fork, and then open a pull request?


-- 
embedded brains GmbH
Herr Sebastian HUBER
Dornierstr. 4
82178 Puchheim
Germany
email: sebastian.hu...@embedded-brains.de 
<mailto:sebastian.hu...@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/>



___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: Add Formal Verification chapter v2

2023-01-20 Thread andrew.butterfi...@scss.tcd.ie 
> On 25/11/2022 07:46, Sebastian Huber  
> wrote:
>>  On 24/11/2022 14:41, andrew.butterfi...@scss.tcd.ie wrote:
>>>  On 16/11/2022 16:44, Gedare Bloom  wrote:
>>>Section 9.7 "RTEMS Formal Model Guide" seems like it includes both
>>>some aspects of a How-To but also a lot of details that might be
>>>better as a separate document specific to the Promela/Verification
>>>detailed implementation. The point of the RTEMS Software Engineering
>>>manual is to provide developers with the guidelines of how to work
>>>with RTEMS. This section is very detailed about the implementation of
>>>specific models and feels unbalanced with the rest of the new section.
>>>For example, this section is about 3/5 of the entire "Formal
>>>Verification" section.
>> 
>> I agree - this was what struck me after I had sent the patch set. In a 
>> sense I think we need a new top-level document, analagous to the Classic 
>> API and POSIX API guides.
>
> I am not sure if a new top-level document is really the best option. 
> From my point of view, the RTEMS Software Engineering manual should 
> cover everything useful for the general RTEMS maintainer. The models 
>  cover core services of RTEMS. With different documents you just have to 
> open more documents and cross referencing will be more difficult. I am 
> more in favour of a top-level chapter in the manual or some sort of an 
> appendix chapter.

Now that the integration of the formal models and tools is in progress, I want 
to revisit this issue. Yes, the models cover core services, but those are
described in other documents like the Classic API guide (and POSIX). It would
seem that a better place to put any model documentation would be in those 
guides.

However, the formal verification/qualification is something very new, and I’m 
not sure how regular users would feel about that kind of extra material, at
least at this early stage of adopting qual/FV techniques.

For now, I am going fixup all the other issues raised by Gedare, 
and submit a v2 patch set.

Regards,
   Andrew


Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
Lero@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/


___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

formal: Fixes Licenses

2023-01-23 Thread andrew.butterfi...@scss.tcd.ie 
Patches to fix licenses for formal material are attached.
The main issue was missing/wrong SPDX identifiers

Best regards,
  Andrew Butterfield






-cover-letter.patch
Description: -cover-letter.patch


0001-formal-fix-licenses.patch
Description: 0001-formal-fix-licenses.patch
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: Add Formal Verification chapter v3

2023-03-09 Thread andrew.butterfi...@scss.tcd.ie 
ping


From: devel  on behalf of 
"andrew.butterfi...@scss.tcd.ie" 
Date: Friday 10 February 2023 at 16:10
To: "rtems-de...@rtems.org" 
Subject: eng: Add Formal Verification chapter v3

Dear RTEMS Developers,
Here is a 3rd version of the proposed Formal Verification chapter
 to be added to the Software Engineering Manual.

The patch-set is attached here, as I cannot use git-mail.

Best Regards,
  Andrew


___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: Add Formal Verification chapter v3

2023-03-10 Thread andrew.butterfi...@scss.tcd.ie 
Hi Gedare,
 the quick and easy way is to visit 
https://github.com/andrewbutterfield/rtems-docs/commit/8165814471402d56c480b1400b121715ad507c58

That's a fork of RTEMS/rtems-docs on Github - and is the top of my 
`new-eng-chapter` branch.

The commits are those I had developing it and do not match the patch-set I sent.

Will that do?

Regards,
  Andrew



On 09/03/2023, 20:22, "Gedare Bloom" mailto:ged...@rtems.org>> wrote:


Hi Andrew,


In this case, since the patches are attachments, would you happen to
have a hosted git (github?) repo that I could examine to facilitate a
review. I can only review inline patches efficiently by email.


Gedare


On Thu, Mar 9, 2023 at 6:52 AM andrew.butterfi...@scss.tcd.ie 
<mailto:andrew.butterfi...@scss.tcd.ie>
mailto:andrew.butterfi...@scss.tcd.ie>> wrote:
>
> ping
>
>
>
>
>
> From: devel mailto:devel-boun...@rtems.org>> on 
> behalf of "andrew.butterfi...@scss.tcd.ie 
> <mailto:andrew.butterfi...@scss.tcd.ie>"  <mailto:andrew.butterfi...@scss.tcd.ie>>
> Date: Friday 10 February 2023 at 16:10
> To: "rtems-de...@rtems.org <mailto:rtems-de...@rtems.org>" 
> mailto:rtems-de...@rtems.org>>
> Subject: eng: Add Formal Verification chapter v3
>
>
>
> Dear RTEMS Developers,
>
> Here is a 3rd version of the proposed Formal Verification chapter
>
> to be added to the Software Engineering Manual.
>
>
>
> The patch-set is attached here, as I cannot use git-mail.
>
>
>
> Best Regards,
>
> Andrew
>
>
>
>
>
> ___
> devel mailing list
> devel@rtems.org <mailto:devel@rtems.org>
> http://lists.rtems.org/mailman/listinfo/devel 
> <http://lists.rtems.org/mailman/listinfo/devel>



___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: Add Formal Verification chapter v3

2023-03-13 Thread andrew.butterfi...@scss.tcd.ie 
Hi Gedare,
 pull request done

Regards,
 Andrew



On 10/03/2023, 21:23, "Gedare Bloom" mailto:ged...@rtems.org>> wrote:


On Fri, Mar 10, 2023 at 8:19 AM andrew.butterfi...@scss.tcd.ie 
<mailto:andrew.butterfi...@scss.tcd.ie>
mailto:andrew.butterfi...@scss.tcd.ie>> wrote:
>
> Hi Gedare,
> the quick and easy way is to visit 
> https://github.com/andrewbutterfield/rtems-docs/commit/8165814471402d56c480b1400b121715ad507c58
>  
> <https://github.com/andrewbutterfield/rtems-docs/commit/8165814471402d56c480b1400b121715ad507c58>
>
Yes, In this case, can you (or I can) create a Pull Request from your
new-eng-chapter branch to the `master` branch on your fork of
rtems-docs? then I can review your code changes for you there pretty
easily.


> That's a fork of RTEMS/rtems-docs on Github - and is the top of my 
> `new-eng-chapter` branch.
>
> The commits are those I had developing it and do not match the patch-set I 
> sent.
>
> Will that do?
>
> Regards,
> Andrew
>
>
>
> On 09/03/2023, 20:22, "Gedare Bloom"  <mailto:ged...@rtems.org> <mailto:ged...@rtems.org 
> <mailto:ged...@rtems.org>>> wrote:
>
>
> Hi Andrew,
>
>
> In this case, since the patches are attachments, would you happen to
> have a hosted git (github?) repo that I could examine to facilitate a
> review. I can only review inline patches efficiently by email.
>
>
> Gedare
>
>
> On Thu, Mar 9, 2023 at 6:52 AM andrew.butterfi...@scss.tcd.ie 
> <mailto:andrew.butterfi...@scss.tcd.ie> 
> <mailto:andrew.butterfi...@scss.tcd.ie 
> <mailto:andrew.butterfi...@scss.tcd.ie>>
> mailto:andrew.butterfi...@scss.tcd.ie> 
> <mailto:andrew.butterfi...@scss.tcd.ie 
> <mailto:andrew.butterfi...@scss.tcd.ie>>> wrote:
> >
> > ping
> >
> >
> >
> >
> >
> > From: devel mailto:devel-boun...@rtems.org> 
> > <mailto:devel-boun...@rtems.org <mailto:devel-boun...@rtems.org>>> on 
> > behalf of "andrew.butterfi...@scss.tcd.ie 
> > <mailto:andrew.butterfi...@scss.tcd.ie> 
> > <mailto:andrew.butterfi...@scss.tcd.ie 
> > <mailto:andrew.butterfi...@scss.tcd.ie>>"  > <mailto:andrew.butterfi...@scss.tcd.ie> 
> > <mailto:andrew.butterfi...@scss.tcd.ie 
> > <mailto:andrew.butterfi...@scss.tcd.ie>>>
> > Date: Friday 10 February 2023 at 16:10
> > To: "rtems-de...@rtems.org <mailto:rtems-de...@rtems.org> 
> > <mailto:rtems-de...@rtems.org <mailto:rtems-de...@rtems.org>>" 
> > mailto:rtems-de...@rtems.org> 
> > <mailto:rtems-de...@rtems.org <mailto:rtems-de...@rtems.org>>>
> > Subject: eng: Add Formal Verification chapter v3
> >
> >
> >
> > Dear RTEMS Developers,
> >
> > Here is a 3rd version of the proposed Formal Verification chapter
> >
> > to be added to the Software Engineering Manual.
> >
> >
> >
> > The patch-set is attached here, as I cannot use git-mail.
> >
> >
> >
> > Best Regards,
> >
> > Andrew
> >
> >
> >
> >
> >
> > ___
> > devel mailing list
> > devel@rtems.org <mailto:devel@rtems.org> <mailto:devel@rtems.org 
> > <mailto:devel@rtems.org>>
> > http://lists.rtems.org/mailman/listinfo/devel 
> > <http://lists.rtems.org/mailman/listinfo/devel> 
> > <http://lists.rtems.org/mailman/listinfo/devel> 
> > <http://lists.rtems.org/mailman/listinfo/devel>;>
>
>
>



___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

FW: Change build specification files from YAML to JSON?

2023-04-24 Thread andrew.butterfi...@scss.tcd.ie 

Hi Sebastian,
would this also affect the specification item YAML files in RTEMS Central? 


I have no strong opinions about this either way.


Regards,
Andrew

 
Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 
Lero@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/ 
 
 
;> 
 


On 24/04/2023, 10:32, "devel on behalf of Sebastian Huber" 
mailto:devel-boun...@rtems.org> 
> on behalf of 
sebastian.hu...@embedded-brains.de  
>> wrote:




Hello,




I would like to change the build specification files from YAML to JSON 
to get rid of the complicated caching mechanism. Python has a built in 
JSON loader which is quite fast compared to the YAML loader. For the 
configure/build steps we have to load all items currently due to the 
item pickle cache (about 2000 files). With the built in JSON support we 
can optimize this to only load the required files (probably less than 
100 if the test suite is disabled).




-- 
embedded brains GmbH
Herr Sebastian HUBER
Dornierstr. 4
82178 Puchheim
Germany
email: sebastian.hu...@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/ 
 
 
;>
___
devel mailing list
devel@rtems.org  >
http://lists.rtems.org/mailman/listinfo/devel 
 
 
;>





___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Integrating the Formal Methods part of Qualification

2022-06-28 Thread andrew.butterfi...@scss.tcd.ie 
Dear RTEMS Developers,

While the validation tests from the RTEMS pre-qualification activity are
now merged into the RTEMS master, the work done in investigating and 
deploying formal methods techniques is not yet merged.

The activity had two main phases: a planning phase (Nov 2018-Oct 2019) 
that explored various formal techniques, followed by an execution phase 
(Oct 2019-Nov 2021) that then applied selected techniques to selected 
parts of RTEMS. Some discussions occurred with the RTEMS community 
via the mailings lists over this time. A short third phase (Nov 2021 - Dec 
2021) 
then reported on the outcomes. Each phase resulted in a technical report.

The key decision made was to use Promela/SPIN for test generation, and 
to apply it to the Chains API, the Event Manager, and the SMP scheduler
thread queues. This involved developing models in the Promela language 
and using the SPIN model-checker tool to both check their correctness
and to generate execution scenarios that could be used to generate tests.
Tools were developed using Python 3.8 to support this. Initial documentation 
about tools and how to use them was put into the 2nd phase report.

We now come to the part where we explore the best way to integrate this
into RTEMS. I am proposing to do this under the guidance of Sebastian Huber.

The first suggested step is adding in new documentation to the RTEMS 
Software Engineering manual, as a new Formal Methods chapter. This would 
provide some motivation, as well as a "howto".

I assume that I would initially describe the proposed changes using the patch 
review process described in the section on Preparing and Sending Patches in 
the User Manual.

How do you feel I should best proceed?

Best regards,
  Andrew Butterfield,


Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
Lero@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/

 

___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: Integrating the Formal Methods part of Qualification

2022-07-01 Thread andrew.butterfi...@scss.tcd.ie 

On 1 Jul 2022, at 00:59, Chris Johns 
mailto:chr...@rtems.org>> wrote:

On 28/6/2022 11:09 pm, 
andrew.butterfi...@scss.tcd.ie<mailto:andrew.butterfi...@scss.tcd.ie> wrote:

Dear RTEMS Developers,

While the validation tests from the RTEMS pre-qualification activity are
now merged into the RTEMS master, the work done in investigating and
deploying formal methods techniques is not yet merged.

The activity had two main phases: a planning phase (Nov 2018-Oct 2019)
that explored various formal techniques, followed by an execution phase
(Oct 2019-Nov 2021) that then applied selected techniques to selected
parts of RTEMS. Some discussions occurred with the RTEMS community
via the mailings lists over this time. A short third phase (Nov 2021 - Dec 2021)
then reported on the outcomes. Each phase resulted in a technical report.

The key decision made was to use Promela/SPIN for test generation, and
to apply it to the Chains API, the Event Manager, and the SMP scheduler
thread queues. This involved developing models in the Promela language
and using the SPIN model-checker tool to both check their correctness
and to generate execution scenarios that could be used to generate tests.
Tools were developed using Python 3.8 to support this. Initial documentation
about tools and how to use them was put into the 2nd phase report.

Congratulations for the work and results you and others have managed to achieve.
It is exciting to see this happening with RTEMS and being made public.


We now come to the part where we explore the best way to integrate this
into RTEMS. I am proposing to do this under the guidance of Sebastian Huber.

The first suggested step is adding in new documentation to the RTEMS
Software Engineering manual, as a new Formal Methods chapter. This would
provide some motivation, as well as a "howto".

I assume that I would initially describe the proposed changes using the patch
review process described in the section on Preparing and Sending Patches in
the User Manual.

How do you feel I should best proceed?

It is hard for me to answer until I understand what is being submitted and who
maintains it? I am sure you understand this due to the specialised nature of the
work.

Indeed, I quite agree.  I have some short answers below, with suggestions.



What will be submitted, ie SPIN files, scripts, etc?

Promela/SPIN model files (ASCII text, C-like syntax)
C template files (.h,.c) to assist test code generation
YAML files to provide a mapping from model concepts to RTEMS C test code
python scripts to automate the test generation
Documentation - largely RTEMS compliant sphinx sources (.rst)


Where are you looking to add these pieces?

Everything except the documentation could live in a top-level folder ('formal') 
in rtems-central.
In fact there is no particular constraint from my perspective for where they 
can go.

The plan would be to add the pertinent parts of our project documentation into 
new chapters
in the RTEMS software engineering manual. So that would be eng/ in the 
rtems-docs repo.



How is the verification run against the code? Do we manage regression testing
and is that even possible?

The python scripts basically run SPIN in such a way as to generate scenarios 
that model
correct behaviour which then get turned into standard RTEMS test programs. 
These all
get added into a new testsuite in the rtems repo (testsuites/models, say).
They are properly integrated into the RTEMS test system, so get built and run 
by waf.
This is similar to how the tests generated by Sebastian in 
testsuites/validation are handled.

From the perspective of a user that works out of 
git.rtems.org/rtems<http://git.rtems.org/rtems>,
there will be no obvious impact - just some extra tests in among the ones that 
already exist.


I hope my simple questions highlight a lack of understand on how this works and
how we maintain it and use it once integrated.

I intend to continue to work and maintain this for the foreseeable future. I 
would hope as this beds in that other Promela/SPIN users out there will also 
get more involved over time.

It is expected that Promela models will be as static as the corresponding APIs. 
They capture the specified behaviour of API calls, not their detailed 
implementation.

The python scripts should also be fairly stable, although I can see some 
tweaking for a while to improve workflow issues that might arise.

There are some extra python libraries that are required over and above what is 
currently specified in rtems-central/requirements.txt


Thanks
Chris

Thanks,
  Andrew



___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: Integrating the Formal Methods part of Qualification

2022-07-01 Thread andrew.butterfi...@scss.tcd.ie 
-Original Message-
From: Chris Johns 


On 28/6/2022 11:09 pm, andrew.butterfi...@scss.tcd.ie wrote:
> Dear RTEMS Developers,
> 
> While the validation tests from the RTEMS pre-qualification activity are
> now merged into the RTEMS master, the work done in investigating and 
> deploying formal methods techniques is not yet merged.
> 
> The activity had two main phases: a planning phase (Nov 2018-Oct 2019) 
> that explored various formal techniques, followed by an execution phase 
> (Oct 2019-Nov 2021) that then applied selected techniques to selected 
> parts of RTEMS. Some discussions occurred with the RTEMS community 
> via the mailings lists over this time. A short third phase (Nov 2021 - 
Dec 2021) 
> then reported on the outcomes. Each phase resulted in a technical report.
> 
> The key decision made was to use Promela/SPIN for test generation, and 
> to apply it to the Chains API, the Event Manager, and the SMP scheduler
> thread queues. This involved developing models in the Promela language 
> and using the SPIN model-checker tool to both check their correctness
> and to generate execution scenarios that could be used to generate tests.
> Tools were developed using Python 3.8 to support this. Initial 
documentation 
> about tools and how to use them was put into the 2nd phase report.

Congratulations for the work and results you and others have managed to 
achieve.
It is exciting to see this happening with RTEMS and being made public.

> We now come to the part where we explore the best way to integrate this
> into RTEMS. I am proposing to do this under the guidance of Sebastian 
Huber.
> 
> The first suggested step is adding in new documentation to the RTEMS 
> Software Engineering manual, as a new Formal Methods chapter. This would 
> provide some motivation, as well as a "howto".
> 
> I assume that I would initially describe the proposed changes using the 
patch 
> review process described in the section on Preparing and Sending Patches 
in 
> the User Manual.
> 
> How do you feel I should best proceed?

It is hard for me to answer until I understand what is being submitted and 
who
maintains it? I am sure you understand this due to the specialised nature 
of the
work.

Indeed, I quite agree.  I have some short answers below, with suggestions.

What will be submitted, ie SPIN files, scripts, etc?

Promela/SPIN model files (ASCII text, C-like syntax)
C template files (.h,.c) to assist test code generation
YAML files to provide a mapping from model concepts to RTEMS C test code 
python scripts to automate the test generation
Documentation - largely RTEMS compliant sphinx sources (.rst)

Where are you looking to add these pieces?

Everything except the documentation could live in a top-level folder ('formal') 
in rtems-central.
In fact there is no particular constraint from my perspective for where they 
can go.
 
The plan would be to add the pertinent parts of our project documentation into 
new chapters
in the RTEMS software engineering manual. So that would be eng/ in the 
rtems-docs repo.

How is the verification run against the code? Do we manage regression 
testing
and is that even possible?

The python scripts basically run SPIN in such a way as to generate scenarios 
that model
correct behaviour which then get turned into standard RTEMS test programs. 
These all
get added into a new testsuite in the rtems repo (testsuites/models, say).
They are properly integrated into the RTEMS test system, so get built and run 
by waf.
This is similar to how the tests generated by Sebastian in 
testsuites/validation are handled.
 
>From the perspective of a user that works out of git.rtems.org/rtems, 
there will be no obvious impact - just some extra tests in among the ones that 
already exist.

I hope my simple questions highlight a lack of understand on how this works 
and
how we maintain it and use it once integrated.

I intend to continue to work and maintain this for the foreseeable future. I 
would hope as this beds in that other Promela/SPIN users out there will also 
get more involved over time.
 
It is expected that Promela models will be as static as the corresponding APIs. 
They capture the specified behaviour of API calls, not their detailed 
implementation.
 
The python scripts should also be fairly stable, although I can see some 
tweaking for a while to improve workflow issues that might arise.
 
There are some extra python libraries that are required over and above what is 
currently specified in rtems-central/requirements.txt

Thanks
Chris

Thanks,
  Andrew

___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: Integrating the Formal Methods part of Qualification

2022-07-11 Thread andrew.butterfi...@scss.tcd.ie 
On 6 Jul 2022, at 20:07, Gedare Bloom  wrote:

On Sun, Jul 3, 2022 at 7:49 PM Chris Johns  wrote:


On 2/7/2022 12:59 am, Andrew Butterfield wrote:

On 1 Jul 2022, at 00:59, Chris Johns mailto:chr...@rtems.org>> wrote:


On 28/6/2022 11:09 pm, andrew.butterfi...@scss.tcd.ie
<mailto:andrew.butterfi...@scss.tcd.ie> wrote:

Dear RTEMS Developers,

While the validation tests from the RTEMS pre-qualification activity are
now merged into the RTEMS master, the work done in investigating and
deploying formal methods techniques is not yet merged.

The activity had two main phases: a planning phase (Nov 2018-Oct 2019)
that explored various formal techniques, followed by an execution phase
(Oct 2019-Nov 2021) that then applied selected techniques to selected
parts of RTEMS. Some discussions occurred with the RTEMS community
via the mailings lists over this time. A short third phase (Nov 2021 - Dec 2021)
then reported on the outcomes. Each phase resulted in a technical report.

The key decision made was to use Promela/SPIN for test generation, and
to apply it to the Chains API, the Event Manager, and the SMP scheduler
thread queues. This involved developing models in the Promela language
and using the SPIN model-checker tool to both check their correctness
and to generate execution scenarios that could be used to generate tests.
Tools were developed using Python 3.8 to support this. Initial documentation
about tools and how to use them was put into the 2nd phase report.

Congratulations for the work and results you and others have managed to achieve.
It is exciting to see this happening with RTEMS and being made public.


We now come to the part where we explore the best way to integrate this
into RTEMS. I am proposing to do this under the guidance of Sebastian Huber.

The first suggested step is adding in new documentation to the RTEMS
Software Engineering manual, as a new Formal Methods chapter. This would
provide some motivation, as well as a "howto".

I assume that I would initially describe the proposed changes using the patch
review process described in the section on Preparing and Sending Patches in
the User Manual.

How do you feel I should best proceed?

It is hard for me to answer until I understand what is being submitted and who
maintains it? I am sure you understand this due to the specialised nature of the
work.

Indeed, I quite agree.  I have some short answers below, with suggestions.

Thanks.
+1





What will be submitted, ie SPIN files, scripts, etc?

Promela/SPIN model files (ASCII text, C-like syntax)
C template files (.h,.c) to assist test code generation
YAML files to provide a mapping from model concepts to RTEMS C test code
python scripts to automate the test generation
Documentation - largely RTEMS compliant sphinx sources (.rst)



Where are you looking to add these pieces?

Everything except the documentation could live in a top-level folder ('formal')
in rtems-central.
In fact there is no particular constraint from my perspective for where they 
can go.

Using rtems-central is fine.
Do they require anything currently located in rtems-central? Are the
models or YAML files related to the current specification files? I
know I'm guilty of not spending the time yet to deeply learn
rtems-central, but I would like to know that these files will fit
within that repo as it currently is intended to operate.

At the moment there is nothing in rtems-central directly related to this. All 
the python
scripts there support the tools/specs that Sebastian and colleagues developed.
I can see a new top-level script being added here to support the formal stuff.

It is possible that we might introduce a new specification item that integrates
in with the spec system that is used to trigger the Spin test generations. I'll 
discuss the
best wat to do this with Sebastian.




RSB should be taught how to build the necessary host tools to run Promela/SPIN.

Spin is open source under a BSD 3-clause license, available from spinroot.com,
and also via https://github.com/nimble-code/Spin. It is written in C and has 
very few
dependencies. I'm not sure what is involved in adding it to the RSB, but I guess
Sebastian will know.


The plan would be to add the pertinent parts of our project documentation into
new chapters
in the RTEMS software engineering manual. So that would be eng/ in the
rtems-docs repo.

Great.
+1

A new section in the eng should be suitable. I would actually
recommend using
https://docs.rtems.org/branches/master/eng/test-framework.html# as a
good example.

Thanks - that very helpful. I think our section should immediately follow that 
one.
All we need now is a suitable title.  "Formal Test Framework"?




How is the verification run against the code? Do we manage regression testing
and is that even possible?

The python scripts basically run SPIN in such a way as to generate scenarios
that model
correct behaviour which then get turned into stan

Re: Integrating the Formal Methods part of Qualification

2022-07-22 Thread andrew.butterfi...@scss.tcd.ie 
Dear RTEMS developers,

thanks for the feedback below - I want to wrap this up and move to the next 
step.

I propose to produce a complete draft of a formal methods section for the 
Software Engineering manual in rtems-docs
This will add a "Formal Verification" section just after the existing "Test 
Framework" section.

This will allow developers to get a much better idea of what is proposed, and 
for me to get feedback.

For now, the section will state clearly at the start that this is a proposal 
and that the tooling and resources it describes
won't yet be available in RTEMS proper.

Files likely to be modified in rtems-docs:
eng/index.rst
common/refs.bib

I'll add in  eng/formal-verification.rst

I'll then submit patches for review in the usual way.

Regards,
  Andrew



Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
Lero@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/



On 11/07/2022, 12:43, "devel on behalf of 
andrew.butterfi...@scss.tcd.ie<mailto:andrew.butterfi...@scss.tcd.ie>" 
mailto:devel-boun...@rtems.org> on behalf of 
andrew.butterfi...@scss.tcd.ie<mailto:andrew.butterfi...@scss.tcd.ie>> wrote:

On 6 Jul 2022, at 20:07, Gedare Bloom  wrote:

On Sun, Jul 3, 2022 at 7:49 PM Chris Johns  wrote:

On 2/7/2022 12:59 am, Andrew Butterfield wrote:
On 1 Jul 2022, at 00:59, Chris Johns mailto:chr...@rtems.org>> wrote:

On 28/6/2022 11:09 pm, andrew.butterfi...@scss.tcd.ie
<mailto:andrew.butterfi...@scss.tcd.ie> wrote:
Dear RTEMS Developers,

While the validation tests from the RTEMS pre-qualification activity are
now merged into the RTEMS master, the work done in investigating and
deploying formal methods techniques is not yet merged.

The activity had two main phases: a planning phase (Nov 2018-Oct 2019)
that explored various formal techniques, followed by an execution phase
(Oct 2019-Nov 2021) that then applied selected techniques to selected
parts of RTEMS. Some discussions occurred with the RTEMS community
via the mailings lists over this time. A short third phase (Nov 2021 - Dec 2021)
then reported on the outcomes. Each phase resulted in a technical report.

The key decision made was to use Promela/SPIN for test generation, and
to apply it to the Chains API, the Event Manager, and the SMP scheduler
thread queues. This involved developing models in the Promela language
and using the SPIN model-checker tool to both check their correctness
and to generate execution scenarios that could be used to generate tests.
Tools were developed using Python 3.8 to support this. Initial documentation
about tools and how to use them was put into the 2nd phase report.

Congratulations for the work and results you and others have managed to achieve.
It is exciting to see this happening with RTEMS and being made public.

We now come to the part where we explore the best way to integrate this
into RTEMS. I am proposing to do this under the guidance of Sebastian Huber.

The first suggested step is adding in new documentation to the RTEMS
Software Engineering manual, as a new Formal Methods chapter. This would
provide some motivation, as well as a "howto".

I assume that I would initially describe the proposed changes using the patch
review process described in the section on Preparing and Sending Patches in
the User Manual.

How do you feel I should best proceed?

It is hard for me to answer until I understand what is being submitted and who
maintains it? I am sure you understand this due to the specialised nature of the
work.

Indeed, I quite agree.  I have some short answers below, with suggestions.

Thanks.
+1



What will be submitted, ie SPIN files, scripts, etc?

Promela/SPIN model files (ASCII text, C-like syntax)
C template files (.h,.c) to assist test code generation
YAML files to provide a mapping from model concepts to RTEMS C test code
python scripts to automate the test generation
Documentation - largely RTEMS compliant sphinx sources (.rst)


Where are you looking to add these pieces?

Everything except the documentation could live in a top-level folder ('formal')
in rtems-central.
In fact there is no particular constraint from my perspective for where they 
can go.

Using rtems-central is fine.
Do they require anything currently located in rtems-central? Are the
models or YAML files related to the current specification files? I
know I'm guilty of not spending the time yet to deeply learn
rtems-central, but I would like to know that these files will fit
within that repo as it currently is intended to operate.

At the moment there is nothing in rte

eng: Add Formal Verification chapter

2022-09-13 Thread andrew.butterfi...@scss.tcd.ie 
Dear RTEMS Developers,

  The attached patch file adds a new Formal Verification chapter as discussed 
in the previous email thread
regarding "Integrating the Formal Methods part of Qualification"
(see https://lists.rtems.org/pipermail/devel/2022-July/072167.html ).

This is just the documentation for what was done. None of the files or tools 
mentioned are contained
in the patch. Most of those would be deployed to rtems-central or the "main" 
rtems repo.

Best Regards,
  Andrew


Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
Lero@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/

 



0001-eng-Add-Formal-Verification-chapter.patch
Description: 0001-eng-Add-Formal-Verification-chapter.patch
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

eng: Add Formal Verification chapter v2

2022-09-13 Thread andrew.butterfi...@scss.tcd.ie 
Dear RTEMS Developers,

  The inlined patch file below adds a new Formal Verification chapter as 
discussed in the previous email thread
regarding "Integrating the Formal Methods part of Qualification"
(see https://lists.rtems.org/pipermail/devel/2022-July/072167.html ).

This is just the documentation for what was done. None of the files or tools 
mentioned are contained
in the patch. Most of those would be deployed to rtems-central or the "main" 
rtems repo.

Best Regards,
  Andrew

From ca8d303e7b25b02d9c4aad3b7f76dbdc1cdfa396 Mon Sep 17 00:00:00 2001
From: Andrew Butterfield 
Date: Mon, 23 May 2022 17:02:21 +0100
Subject: [PATCH] eng: Add Formal Verification chapter

---
 common/refs.bib|   56 ++
 eng/fv/index.rst   |   32 +
 eng/fv/maintenance.rst |   70 ++
 eng/fv/methodology.rst |  228 +++
 eng/fv/model-guide.rst | 1482 
 eng/fv/overview.rst|   33 +
 eng/fv/promela.rst |  320 +
 eng/fv/refinement.rst  |  359 ++
 eng/fv/tool-setup.rst  |   80 +++
 eng/index.rst  |2 +
 10 files changed, 2662 insertions(+)
 create mode 100644 eng/fv/index.rst
 create mode 100644 eng/fv/maintenance.rst
 create mode 100644 eng/fv/methodology.rst
 create mode 100644 eng/fv/model-guide.rst
 create mode 100644 eng/fv/overview.rst
 create mode 100644 eng/fv/promela.rst
 create mode 100644 eng/fv/refinement.rst
 create mode 100644 eng/fv/tool-setup.rst

diff --git a/common/refs.bib b/common/refs.bib
index 066d746..6b25fae 100644
--- a/common/refs.bib
+++ b/common/refs.bib
@@ -9,6 +9,25 @@
   year= {1973},
   pages   = {46-61},
 }
+@article{Djikstra:1975:GCL,
+author = {Dijkstra, Edsger W.},
+title = {Guarded Commands, Nondeterminacy and Formal Derivation of Programs},
+year = {1975},
+issue_date = {Aug. 1975},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {18},
+number = {8},
+issn = {0001-0782},
+url = {https://doi.org/10.1145/360933.360975},
+doi = {10.1145/360933.360975},
+abstract = {So-called “guarded commands” are introduced as a building block 
for alternative and repetitive constructs that allow nondeterministic program 
components for which at least the activity evoked, but possibly even the final 
state, is not necessarily uniquely determined by the initial state. For the 
formal derivation of programs expressed in terms of these constructs, a 
calculus will be be shown.},
+journal = {Commun. ACM},
+month = {aug},
+pages = {453–457},
+numpages = {5},
+keywords = {correctness proof, programming methodology, program semantics, 
case-construction, termination, nondeterminancy, programming languages, 
derivation of programs, sequencing primitives, repetition, programming language 
semantics}
+}
 @inproceedings{Varghese:1987:TimerWheel,
   author  = {Varghese, G. and Lauck, T.},
   title   = {{Hashed and Hierarchical Timing Wheels: Data Structures for 
the Efficient Implementation of a Timer Facility}},
@@ -95,6 +114,16 @@
   url   = {http://www.rfc-editor.org/rfc/rfc2119.txt},
   note  = {\url{http://www.rfc-editor.org/rfc/rfc2119.txt}},
 }
+@ARTICLE{Holzmann:1997:SPIN,
+  author={Holzmann, G.J.},
+  journal={IEEE Transactions on Software Engineering},
+  title={The model checker SPIN},
+  year={1997},
+  volume={23},
+  number={5},
+  pages={279-295},
+  doi={10.1109/32.588521}
+}
 @article{Blumofe:1999:WS,
   author  = {Blumofe, Robert D. and Leiserson, Charles E.},
   title   = {{Scheduling multithreaded computations by work stealing}},
@@ -373,6 +402,33 @@
   title = {{RTEMS CPU Architecture Supplement}},
   url   = {https://docs.rtems.org/branches/master/cpu-supplement.pdf},
 }
+@mastersthesis{Jennings:2021:FV,
+  author =   {Robert Jennings},
+  title ={{Formal Verification of a Real-Time Multithreaded Operating 
System}},
+  school =   {School of Computer Science and Statistics},
+  year = {2021},
+  type = {Master of Science in {Computer Science (MCS)}},
+  address =  {Trinity College, Dublin 2, Ireland},
+  month ={August},
+}
+@mastersthesis{Jaskuc:2022:TESTGEN,
+  author =   {Jerzy Ja{\'{s}}ku{\'{c}}},
+  title ={{SPIN/Promela-Based Test Generation Framework for RTEMS 
Barrier Manager}},
+  school =   {School of Computer Science and Statistics},
+  year = {2022},
+  type = {Master of Science in {Computer Science (MCS)}},
+  address =  {Trinity College, Dublin 2, Ireland},
+  month ={April},
+}
+@mastersthesis{Lynch:2022:TESTGEN,
+  author =   {Eoin Lynch},
+  title ={{Using Promela/SPIN to do Test Generation for RTEMS-SMP}},
+  school =   {School of Engineering},
+  year = {2022},
+  type = {Master of {Engineering (Computer Engineering)}},
+  address =  {Trinity College, Dublin 2, Ireland},
+  month ={April},
+}
 % ECSS
 % Sort lexicographically
 @manual{ECSS_E_ST_10_02C_R1,
diff --git a/eng

Re: Integrating the Formal Methods part of Qualification

2022-09-19 Thread andrew.butterfi...@scss.tcd.ie 
Dear Andrew,

> It's great to see a move toward formal verification for RTEMS.

Great to hear about other work in this space as well !

> From our side (TU Dortmund in Germany and the University of Twente in the 
> Netherlands), we recently adopted Frama-C to verify ICPP and MrsP. A 
> potential deadlock is successfully identified, and a remedy is provided. The 
> result will be presented in EMSOFT this year 
> (https://ieeexplore.ieee.org/document/9852753/), and the verification 
> framework is publicly released here: 
> https://github.com/tu-dortmund-ls12-rt/Resource-Synchronization-Protocols-Verification-RTEMS

Thanks for posting this - I have already  looked at and your paper pre-print - 
I like it a lot.

It complements our work very well - for example, one of the current pieces of 
our on-going work is looking at thread queues. You assume they
are implemented correctly, while we are exploring the use of model-based 
techniques to corroborate this.


> Due to the double-blind review process, I cannot chime in earlier in this 
> thread. Today earlier I have seen your patches regarding the chapter you 
> proposed. I wonder if you could take our contribution into account when you 
> organize the chapter? 
A preprint can be found 
https://www.researchgate.net/publication/362599165_Formal_Verification_of_Resource_Synchronization_Protocol_Implementations_A_Case_Study_in_RTEMS.
 (The corresponding ticket will be prepared, and the patch together with a test 
case will be submitted)

I modelled the draft formal verification chapter on the immediately preceding 
one on the Software Testing Framework.
Like it, it currently lacks much of a background/literature survey - I am 
awaiting feedback on it.
In any case, your work will be added in to anything I write about this area.

Best Regards,
  Andrew


Best,
Kuan-Hsun

On Fri, Jul 22, 2022 at 12:37 PM 
mailto:andrew.butterfi...@scss.tcd.ie 
wrote:
Dear RTEMS developers,
 
thanks for the feedback below - I want to wrap this up and move to the next 
step.
 
I propose to produce a complete draft of a formal methods section for the 
Software Engineering manual in rtems-docs
This will add a "Formal Verification" section just after the existing "Test 
Framework" section.
 
This will allow developers to get a much better idea of what is proposed, and 
for me to get feedback.
 
For now, the section will state clearly at the start that this is a proposal 
and that the tooling and resources it describes
won't yet be available in RTEMS proper. 
 
Files likely to be modified in rtems-docs:
eng/index.rst
common/refs.bib
 
I'll add in  eng/formal-verification.rst
 
I'll then submit patches for review in the usual way.
 
Regards,
  Andrew
 
 

Andrew Butterfield     Tel: +353-1-896-2517     Fax: +353-1-677-2204
Lero@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/

 
 
On 11/07/2022, 12:43, "devel on behalf of 
mailto:andrew.butterfi...@scss.tcd.ie";  wrote:
 
On 6 Jul 2022, at 20:07, Gedare Bloom  wrote:
 
On Sun, Jul 3, 2022 at 7:49 PM Chris Johns  wrote:

On 2/7/2022 12:59 am, Andrew Butterfield wrote:
On 1 Jul 2022, at 00:59, Chris Johns > wrote:

On 28/6/2022 11:09 pm, mailto:andrew.butterfi...@scss.tcd.ie
 wrote:
Dear RTEMS Developers,

While the validation tests from the RTEMS pre-qualification activity are
now merged into the RTEMS master, the work done in investigating and
deploying formal methods techniques is not yet merged.

The activity had two main phases: a planning phase (Nov 2018-Oct 2019)
that explored various formal techniques, followed by an execution phase
(Oct 2019-Nov 2021) that then applied selected techniques to selected
parts of RTEMS. Some discussions occurred with the RTEMS community
via the mailings lists over this time. A short third phase (Nov 2021 - Dec 2021)
then reported on the outcomes. Each phase resulted in a technical report.

The key decision made was to use Promela/SPIN for test generation, and
to apply it to the Chains API, the Event Manager, and the SMP scheduler
thread queues. This involved developing models in the Promela language
and using the SPIN model-checker tool to both check their correctness
and to generate execution scenarios that could be used to generate tests.
Tools were developed using Python 3.8 to support this. Initial documentation
about tools and how to use them was put into the 2nd phase report.

Congratulations for the wo

Re: Add Formal Verification chapter v4

2023-09-06 Thread andrew.butterfi...@scss.tcd.ie 
Ping

(I've let this sit a while  - time to wake it up!)


Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
Lero@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/>
 








-Original Message-
From: devel mailto:devel-boun...@rtems.org>> on 
behalf of "andrew.butterfi...@scss.tcd.ie 
<mailto:andrew.butterfi...@scss.tcd.ie>" mailto:andrew.butterfi...@scss.tcd.ie>>
Date: Tuesday 18 July 2023 at 13:54
To: "rtems-de...@rtems.org <mailto:rtems-de...@rtems.org>" 
mailto:rtems-de...@rtems.org>>
Subject: Add Formal Verification chapter v4


Dear all,
I've attached a patch-set for v4 of the proposal to add a formal verification 
chapter to the Software Engineering manual.
(I can’t do git-mail)


I've setup a pull-request at https://github.com/RTEMS/rtems-docs/pull/6 
<https://github.com/RTEMS/rtems-docs/pull/6> for review purposes.


Regards,
Andrew
 
Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 
Lero@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/>;> 
 













___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: Add Formal Verification chapter v4

2023-09-21 Thread andrew.butterfi...@scss.tcd.ie 
Hi Gedare,
 I've made some changes and raised some further queries - I don't know if you 
get any notifications from github

PR: (https://github.com/RTEMS/rtems-docs/pull/6)

Regards,
  Andrew



 
Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 
Lero@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/> 
 





On 14/09/2023, 20:17, "Gedare Bloom" mailto:ged...@rtems.org>> wrote:


Thanks, I left comments on your pull request.


On Wed, Sep 6, 2023 at 7:26 AM andrew.butterfi...@scss.tcd.ie 
<mailto:andrew.butterfi...@scss.tcd.ie>
mailto:andrew.butterfi...@scss.tcd.ie>> wrote:
>
> Ping
>
> (I've let this sit a while - time to wake it up!)
>
> 
> Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
> Lero@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/>;>
> 
>
>
>
>
>
>
>
>
> -Original Message-
> From: devel mailto:devel-boun...@rtems.org> 
> <mailto:devel-boun...@rtems.org <mailto:devel-boun...@rtems.org>>> on behalf 
> of "andrew.butterfi...@scss.tcd.ie <mailto:andrew.butterfi...@scss.tcd.ie> 
> <mailto:andrew.butterfi...@scss.tcd.ie 
> <mailto:andrew.butterfi...@scss.tcd.ie>>"  <mailto:andrew.butterfi...@scss.tcd.ie> 
> <mailto:andrew.butterfi...@scss.tcd.ie 
> <mailto:andrew.butterfi...@scss.tcd.ie>>>
> Date: Tuesday 18 July 2023 at 13:54
> To: "rtems-de...@rtems.org <mailto:rtems-de...@rtems.org> 
> <mailto:rtems-de...@rtems.org <mailto:rtems-de...@rtems.org>>" 
> mailto:rtems-de...@rtems.org> 
> <mailto:rtems-de...@rtems.org <mailto:rtems-de...@rtems.org>>>
> Subject: Add Formal Verification chapter v4
>
>
> Dear all,
> I've attached a patch-set for v4 of the proposal to add a formal verification 
> chapter to the Software Engineering manual.
> (I can’t do git-mail)
>
>
> I've setup a pull-request at https://github.com/RTEMS/rtems-docs/pull/6 
> <https://github.com/RTEMS/rtems-docs/pull/6> 
> <https://github.com/RTEMS/rtems-docs/pull/6> 
> <https://github.com/RTEMS/rtems-docs/pull/6>;> for review purposes.
>
>
> Regards,
> Andrew
> 
> Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
> Lero@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/>;> 
> <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/&gt;>;>
> 
>
>
>
>
>
>
>
>
>
>
>
>
>



___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: Add Formal Verification chapter v4

2023-09-21 Thread andrew.butterfi...@scss.tcd.ie 

On 21/09/2023, 16:42, "Sebastian Huber" mailto:sebastian.hu...@embedded-brains.de>> wrote:
On 21.09.23 17:41, Gedare Bloom wrote:
>> On Thu, Sep 21, 2023 at 9:36 AM Sebastian Huber
>> > > 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.

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

-- 
embedded brains GmbH
Herr Sebastian HUBER
Dornierstr. 4
82178 Puchheim
Germany
email: sebastian.hu...@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/ 




___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: Add Formal Verification chapter v4

2023-09-22 Thread andrew.butterfi...@scss.tcd.ie 



Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
Lero@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.butterfi...@scss.tcd.ie <mailto:andrew.butterfi...@scss.tcd.ie>" 
mailto:andrew.butterfi...@scss.tcd.ie>>
Date: Thursday 21 September 2023 at 17:02

>On 21/09/2023, 16:42, "Sebastian Huber" <mailto:sebastian.hu...@embedded-brains.de> 
>><mailto:sebastian.hu...@embedded-brains.de 
><mailto:sebastian.hu...@embedded-brains.de>>> wrote:
>On 21.09.23 17:41, Gedare Bloom wrote:
>>> On Thu, Sep 21, 2023 at 9:36 AM Sebastian Huber
>>> >> <mailto:sebastian.hu...@embedded-brains.de> 
>>> <mailto:sebastian.hu...@embedded-brains.de 
>>> <mailto:sebastian.hu...@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: 
>/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@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.hu...@embedded-brains.de 
<mailto:sebastian.hu...@embedded-brains.de> 
<mailto:sebastian.hu...@embedded-brains.de 
<mailto:sebastian.hu...@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/>;>









___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: Add Formal Verification chapter v4

2023-10-09 Thread andrew.butterfi...@scss.tcd.ie 
Eliding some stuff
>On 05/10/2023, 16:02, "Gedare Bloom" mailto:ged...@rtems.org>> wrote:
>>On Fri, Sep 22, 2023 at 4:50 AM andrew.butterfi...@scss.tcd.ie 
>><mailto:andrew.butterfi...@scss.tcd.ie> wrote:
>>On 21/09/2023, 16:42, "Sebastian Huber" >>>> wrote:
>>>On 21.09.23 17:41, Gedare Bloom wrote:
>>>> On Thu, Sep 21, 2023 at 9:36 AM Sebastian Huber
>>>> 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: 
>>>/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.

Is it now worthwhile my preparing a v5 set of patches for committing into 
rtems-docs master,
Or are there more edits that need doing?

Rergards, Andrew




___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

rtems-docs README.txt: how to specify a particular sphinx version

2023-11-09 Thread andrew.butterfi...@scss.tcd.ie 
Adds some lines to indicate how to install a specific sphinx version
Patches are attached.

Regards, Andrew


 
Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 
Lero@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/ 
 
 







-cover-letter.patch
Description: -cover-letter.patch


0001-README.txt-addresses-need-to-specify-a-particular-sp.patch
Description: 0001-README.txt-addresses-need-to-specify-a-particular-sp.patch
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: add Formal Verification chapter v5

2023-11-09 Thread andrew.butterfi...@scss.tcd.ie 
Hello Sebastian,
 Thanks for that, and the  fixes !

Regards, Andrew

 
Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 
Lero@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/ 
 
 





On 09/11/2023, 12:47, "Sebastian Huber" mailto:sebastian.hu...@embedded-brains.de>> wrote:


Hello Andrew,


thanks for your patience. I checked in the patch set as a single patch. 
I removed all white space at the end of lines and added the TCD 
copyright to the index.


https://git.rtems.org/rtems-docs/commit/?id=2c88912893ebbcc3b9fa14d4fcc100c42252d0df
 



Kind regards,
Sebastian


-- 
embedded brains GmbH
Herr Sebastian HUBER
Dornierstr. 4
82178 Puchheim
Germany
email: sebastian.hu...@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/ 




___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: add Formal Verification chapter v5

2023-11-13 Thread andrew.butterfi...@scss.tcd.ie 
 Gedare, Sebastian,
Thanks for all you help  and good feedback.

Is there a timeline for when the document will be rebuilt to show the new 
chapter?

Regards, Andrew


 
Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 
Lero@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/> 
 



On 09/11/2023, 15:27, "Gedare Bloom" mailto:ged...@rtems.org>> wrote:


Andrew,


Thanks for working through this.


Gedare


On Thu, Nov 9, 2023 at 7:19 AM andrew.butterfi...@scss.tcd.ie 
<mailto:andrew.butterfi...@scss.tcd.ie>
mailto:andrew.butterfi...@scss.tcd.ie>> wrote:
>
> Hello Sebastian,
> Thanks for that, and the fixes !
>
> Regards, Andrew
>
> 
> Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204
> Lero@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/>;>
> 
>
>
>
>
>
> On 09/11/2023, 12:47, "Sebastian Huber"  <mailto:sebastian.hu...@embedded-brains.de> 
> <mailto:sebastian.hu...@embedded-brains.de 
> <mailto:sebastian.hu...@embedded-brains.de>>> wrote:
>
>
> Hello Andrew,
>
>
> thanks for your patience. I checked in the patch set as a single patch.
> I removed all white space at the end of lines and added the TCD
> copyright to the index.
>
>
> https://git.rtems.org/rtems-docs/commit/?id=2c88912893ebbcc3b9fa14d4fcc100c42252d0df
>  
> <https://git.rtems.org/rtems-docs/commit/?id=2c88912893ebbcc3b9fa14d4fcc100c42252d0df>
>  
> <https://git.rtems.org/rtems-docs/commit/?id=2c88912893ebbcc3b9fa14d4fcc100c42252d0df>
>  
> <https://git.rtems.org/rtems-docs/commit/?id=2c88912893ebbcc3b9fa14d4fcc100c42252d0df>;>
>
>
> Kind regards,
> Sebastian
>
>
> --
> embedded brains GmbH
> Herr Sebastian HUBER
> Dornierstr. 4
> 82178 Puchheim
> Germany
> email: sebastian.hu...@embedded-brains.de 
> <mailto:sebastian.hu...@embedded-brains.de> 
> <mailto:sebastian.hu...@embedded-brains.de 
> <mailto:sebastian.hu...@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/>;>
>
>
>
> ___
> devel mailing list
> devel@rtems.org <mailto:devel@rtems.org>
> http://lists.rtems.org/mailman/listinfo/devel 
> <http://lists.rtems.org/mailman/listinfo/devel>





___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: add Formal Verification chapter v5

2023-11-14 Thread andrew.butterfi...@scss.tcd.ie 
Hi Chris,
 It looks fine - no major issues.

Thanks for the update

Andrew

 
Andrew Butterfield Tel: +353-1-896-2517 Fax: +353-1-677-2204 
Lero@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/> 
 





On 14/11/2023, 05:02, "Chris Johns" mailto:chr...@rtems.org>> wrote:


On 14/11/2023 7:29 am, Chris Johns wrote:
> On 14/11/2023 3:42 am, andrew.butterfi...@scss.tcd.ie 
> <mailto:andrew.butterfi...@scss.tcd.ie> wrote:
>> Is there a timeline for when the document will be rebuilt to show the new 
>> chapter?
> 
> I need to run this manually at the moment. I will take a look today.
> 


Updated. Please check.


Thanks
Chris



___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel

Re: [PATCH] glossary: Add terms

2023-11-28 Thread andrew.butterfi...@scss.tcd.ie 


From: devel  on behalf of Joel Sherrill 

Reply to: "j...@rtems.org" 
Date: Tuesday 28 November 2023 at 19:31
To: Sebastian Huber 
Cc: "devel@rtems.org" 
Subject: Re: [PATCH] glossary: Add terms



On Tue, Nov 28, 2023 at 10:27 AM Sebastian Huber 
mailto:sebastian.hu...@embedded-brains.de>> 
wrote:
---
 c-user/glossary.rst   | 50 +++
 eng/fv/approaches.rst |  2 +-
 eng/fv/overview.rst   |  6 +++---
 eng/glossary.rst  | 26 +-
 4 files changed, 75 insertions(+), 9 deletions(-)

diff --git a/c-user/glossary.rst b/c-user/glossary.rst
index 82aedcd..9a9d12c 100644
--- a/c-user/glossary.rst
+++ b/c-user/glossary.rst
@@ -1,5 +1,6 @@
 .. SPDX-License-Identifier: CC-BY-SA-4.0

+.. Copyright (C) 2022, 2023 Trinity College Dublin
 .. Copyright (C) 2020 Richi Dubey 
(richidu...@gmail.com)
 .. Copyright (C) 2015, 2023 embedded brains GmbH & Co. KG
 .. Copyright (C) 1988, 1998 On-Line Applications Research Corporation (OAR)
@@ -17,6 +18,9 @@ Glossary
 A term used to describe an object which has been created by an
 application.

+AMP
+This term is an acronym for Asymmetric Multiprocessing.
+
 APA
 This term is an acronym for Arbitrary Processor Affinity.  APA 
schedulers
 allow a thread to have an arbitrary affinity to a processor set, 
rather than
@@ -357,6 +361,10 @@ Glossary
 mathematically intensive situations.  It is typically viewed as a 
logical
 extension of the primary processor.

+formal model
+A model of a computing component (hardware or software) that has a
+mathematically based :term:`semantics`.

This is in the neighborhood of the definitions I found but is missing a word
like rigorous.

For me "mathematically based" implies "rigorous", but I think you are right to 
emphasise this

How about: "A rigorous model of " ?


+
 freed
 A resource that has been released by the application to RTEMS.

@@ -386,6 +394,14 @@ Glossary
 GNU
 This term is an acronym for `GNU's Not Unix `_.

+GPL
+This term is an acronym for
+`GNU General Public License `__.
+
+GPLv3
+This term is an acronym for
+`GNU General Public License Version 3 
`__.
+

Do we need to include an entry for the GPLv2 w/exception that is actually used 
by some RTEMS code.

 GR712RC
 The
 `GR712RC 
`_
@@ -511,6 +527,10 @@ Glossary
 LIFO
 This term is an acronym for :term:`Last In First Out`.

+Linear Temporal Logic
+This is a logic that states properties about (possibly infinite) 
sequences of
+states.
+
 list
 A data structure which allows for dynamic addition and removal of
 entries.  It is not statically limited to a particular size.
@@ -520,6 +540,12 @@ Glossary
 are arranged such that the least significant byte is at the lowest
 address.

+LLVM
+This term is an acronym for
+`Low Level Virtual Machine `__.
+The LLVM Project is a collection of modular and reusable compiler and
+toolchain technologies.
+
 local
 An object which was created with the LOCAL attribute and is accessible
 only on the node it was created and resides upon.  In a single 
processor
@@ -541,6 +567,9 @@ Glossary
 A :term:`task` ``L`` has a lower :term:`priority` than a task ``H``, if
 task ``L`` is less important than task ``H``.

+LTL
+This term is an acronym for :term:`Linear Temporal Logic`.
+
 major number
 The index of a device driver in the Device Driver Table.

@@ -632,6 +661,9 @@ Glossary
 mathematically intensive situations.  It is typically viewed as a 
logical
 extension of the primary processor.

+OBC
+This term is an acronym for On-Board Computer.
+
 object
 In this document, this term is used to refer collectively to tasks,
 timers, message queues, partitions, regions, semaphores, ports, and 
rate
@@ -806,6 +838,10 @@ Glossary
 A term used to describe routines which do not modify themselves or 
global
 variables.

+refinement
+A *refinement* is a relationship between a specification and its
+implementation as code.
+
 region
 An RTEMS object which is used to allocate and deallocate variable size
 blocks of memory from a dynamically specified area of memory.
@@ -818,6 +854,9 @@ Glossary
 Registers are locations physically located within a component, 
typically
 used for device control or general purpose storage.

+reification
+Another term used to denote :term:`refinement`.
+
 remote
 Any object that does not reside on the local

Re: RSB format changes to meet coding standard

2024-04-19 Thread andrew.butterfi...@scss.tcd.ie 
Hi Chris,
Will you also do this with the formal code in rtems-central/formal ?

I do remember using yapf at some point – I have no problem in your doing this 
here.

I expect to be proposing an update to the formal stuff  
(models,code,documentation) over the Summer period as well.

Regards, Andrew



From: devel  on behalf of Joel Sherrill 

Date: Friday, 19 April 2024 at 03:09
To: Chris Johns 
Cc: Development 
Subject: Re: RSB format changes to meet coding standard

On Thu, Apr 18, 2024, 7:31 PM Chris Johns 
mailto:chr...@rtems.org>> wrote:
Hi,

I would like to run the python code we own through yapf and it's default to
standardise the formatting and to being it inline with the coding standards. It
would be good to do this before we branch for RTEMS 6.

I can crate a patch and post if required but it will be noise and doubt anyone
will review it, I would not. I will run builds etc to make sure the conversion
is clean.

Do I have permission to make the format change as a single commit and push it?

I'm certainly ok with this.

Thanks
Chris
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel
___
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel