Re: RSB format changes to meet coding standard

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,

Re: [PATCH] glossary: Add terms

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

Re: add Formal Verification chapter v5

uot;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

Re: add Formal Verification chapter v5

erfield/> 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.t

Re: add Formal Verification chapter v5

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

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

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

Re: Add Formal Verification chapter v4

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

Re: Add Formal Verification chapter v4

lege, 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:andr

Re: Add Formal Verification chapter v4

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

Re: Add Formal Verification chapter v4

erfield/> 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.i

Re: Add Formal Verification chapter v4

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:rt

FW: Change build specification files from YAML to JSON?

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

Re: Add Formal Verification chapter v3

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&

Re: Add Formal Verification chapter v3

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:

Re: Add Formal Verification chapter v3

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

formal: Fixes Licenses

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

Re: Add Formal Verification chapter v2

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

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

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 Butterf

[PATCH 18/18] adds automatic testgen examples

--- 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(+)

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

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

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

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 +

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

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

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

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 +

[PATCH 10/18] adds weak memory models

--- .../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(+)

[PATCH 08/18] adds message manager model

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

[PATCH 06/18] adds event manager model

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

[PATCH 04/18] adds chains API model

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

[PATCH 02/18] adds barrier manager model

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

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

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

[PATCH 00/18] Adds Formal Verification Material

>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

Re: Add Formal Verification chapter v2

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

Re: Add Formal Verification chapter v2

h-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.tc

Re: Add Formal Verification chapter v2

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

Re: Integrating the Formal Methods part of Qualification

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

eng: Add Formal Verification chapter v2

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

eng: Add Formal Verification chapter

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

Re: Integrating the Formal Methods part of Qualification

cd.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.b

Re: Integrating the Formal Methods part of Qualification

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

Re: Integrating the Formal Methods part of Qualification

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

Re: Integrating the Formal Methods part of Qualification

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 in

Integrating the Formal Methods part of Qualification

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)