Re: Add Formal Verification chapter v2

[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

Re: Add Formal Verification chapter v2

[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

Re: Add Formal Verification chapter v2

[Gedare Bloom]

On Fri, Nov 25, 2022 at 12:45 AM Sebastian Huber
 wrote:
>
> On 24/11/2022 14:41, andrew.butterfi...@scss.tcd.ie 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.
>

My intuition here is that with suitable How-To's written and the code
pushed, we don't need such detailed implementation notes. Just point
the interested reader to the implementation, and to more general
documentation/reports about Promela or even a tech report published by
the group that did this work.

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

[Sebastian Huber]

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

Re: Add Formal Verification chapter v2

[Sebastian Huber]

On 24/11/2022 14:41, andrew.butterfi...@scss.tcd.ie 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.


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

[andrew.butterfi...@scss.tcd.ie]

n.

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

[Gedare Bloom]

Hi Andrew,

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?

We probably need to rearrange this section slightly to accommodate the
possibility (extant) of other formal verification approaches. I think
I'd like to see Sections "9.2 Formal Tools Setup" and 9.4 through the
end of the section become nested beneath "9.3 Modelling RTEMS with
Promela". Add a new section 9.2 to introduce the different approaches
that have/are/might be used to formally verify RTEMS. This will allow
alternatives to be documented and acknowledged by the RTEMS Project.

There's a bunch of terminology that is introduced in this chapter
without additions to the glossary/index. I think we need some
definitions added there to complement the new material. At the very
least I would like to see definitions added for the keywords that are
defined especially in the introduction:
* semantics, formal model, artifact, refinement, LTL
Once those are defined, the terms should be linked to the glossary.
You can see how this is done for example in Section 5.3.4 Traceability
between Software Requirements, Architecture and Design. Glossary
definitions can/should link to each other as relevant.

"To avoid using (long) absolute pathnames to the tools directory" ...
--> maybe it makes sense for you to provide these as part of the env?
Is this stuff using venv or something else?

incomplete section header? "need to explain how to configure testbuilder"
RTMES typo in that section

In section "9.2.2 Running Test Generation" please add some notion of
what is the expected output that one would be checking in the step
"use a simulator to run ts-model-0.exe directly."

There is overuse of double quotations throughout. Sometimes double
quotes are being used to introduce terminology, avoid that. Sometimes
double quotes appear in section headings, avoid that. Prefer to use
double quotes only for quoting (e.g., from references or tool output).
Most cases of the double quotes use in this document should be
eliminated.

In section "9.4 Promela to C Refinement" what is the name of the YAML
file? Is there more than one, or is it unique.

Some of the text that provides examples of how to do some of this
might be suited to a new How-To subsection such as in the end of the
"BSP Build System" section.

In Section "9.6 Test Generation Maintenance" please refer to Section
"Software Development Management" instead of hard-coding the patch
submission process.

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.

Gedare

On Wed, Nov 16, 2022 at 3:57 AM 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 
> 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 

Re: Add Formal Verification chapter v2

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

[Gedare Bloom]

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

[Chris Johns]

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

eng: Add Formal Verification chapter v2

[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