[PATCH 00/18] Adds Formal Verification Material

[Andrew.Butterfield at 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" <sebastian.huber at embedded-brains.de <mailto:sebastian.huber at embedded-brains.de>> wrote:


Hello Andrew,


On 22/12/2022 12:29, Andrew.Butterfield at scss.tcd.ie <mailto:Andrew.Butterfield at scss.tcd.ie> wrote:
> From 3390ccc51f46ce0a4baa60422a62530c7c3c29bd Mon Sep 17 00:00:00 2001
> From: Andrew Butterfield<Andrew.Butterfield at scss.tcd.ie <mailto:Andrew.Butterfield at scss.tcd.ie>>
> Date: Wed, 21 Dec 2022 18:03:47 +0000
> 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.huber at embedded-brains.de <mailto:sebastian.huber at embedded-brains.de>
phone: +49-89-18 94 741 - 16
fax: +49-89-18 94 741 - 08


Registergericht: Amtsgericht München
Registernummer: HRB 157899
Vertretungsberechtigte Geschäftsführer: Peter Rasmussen, Thomas Dörfler
Unsere Datenschutzerklärung finden Sie hier:
https://embedded-brains.de/datenschutzerklaerung/ <https://embedded-brains.de/datenschutzerklaerung/>