<html xmlns:o="urn:schemas-microsoft-com:office:office" xmlns:w="urn:schemas-microsoft-com:office:word" xmlns:m="http://schemas.microsoft.com/office/2004/12/omml" xmlns="http://www.w3.org/TR/REC-html40">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
<meta name="Generator" content="Microsoft Word 15 (filtered medium)">
<style><!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
@font-face
{font-family:"Andale Mono";
panose-1:2 11 5 9 0 0 0 0 0 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0cm;
font-size:11.0pt;
font-family:"Calibri",sans-serif;}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
span.EmailStyle18
{mso-style-type:personal-reply;
font-family:"Calibri",sans-serif;
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;
font-size:10.0pt;
mso-ligatures:none;}
@page WordSection1
{size:612.0pt 792.0pt;
margin:72.0pt 72.0pt 72.0pt 72.0pt;}
div.WordSection1
{page:WordSection1;}
--></style>
</head>
<body lang="EN-IE" link="blue" vlink="purple" style="word-wrap:break-word">
<div class="WordSection1">
<div>
<p class="MsoNormal"><span style="font-family:"Andale Mono";color:black"> </span><span style="color:black"><o:p></o:p></span></p>
</div>
<p class="MsoNormal"><o:p> </o:p></p>
<div style="border:none;border-top:solid #B5C4DF 1.0pt;padding:3.0pt 0cm 0cm 0cm">
<p class="MsoNormal" style="margin-left:36.0pt"><b><span style="font-size:12.0pt;color:black">From:
</span></b><span style="font-size:12.0pt;color:black">devel <devel-bounces@rtems.org> on behalf of Joel Sherrill <joel@rtems.org><br>
<b>Reply to: </b>"joel@rtems.org" <joel@rtems.org><br>
<b>Date: </b>Tuesday 28 November 2023 at 19:31<br>
<b>To: </b>Sebastian Huber <sebastian.huber@embedded-brains.de><br>
<b>Cc: </b>"devel@rtems.org" <devel@rtems.org><br>
<b>Subject: </b>Re: [PATCH] glossary: Add terms<o:p></o:p></span></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
<div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">On Tue, Nov 28, 2023 at 10:27 AM Sebastian Huber <<a href="mailto:sebastian.huber@embedded-brains.de">sebastian.huber@embedded-brains.de</a>> wrote:<o:p></o:p></p>
</div>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<p class="MsoNormal" style="margin-left:36.0pt">---<br>
c-user/glossary.rst | 50 +++++++++++++++++++++++++++++++++++++++++++<br>
eng/fv/approaches.rst | 2 +-<br>
eng/fv/overview.rst | 6 +++---<br>
eng/glossary.rst | 26 +++++++++++++++++-----<br>
4 files changed, 75 insertions(+), 9 deletions(-)<br>
<br>
diff --git a/c-user/glossary.rst b/c-user/glossary.rst<br>
index 82aedcd..9a9d12c 100644<br>
--- a/c-user/glossary.rst<br>
+++ b/c-user/glossary.rst<br>
@@ -1,5 +1,6 @@<br>
.. SPDX-License-Identifier: CC-BY-SA-4.0<br>
<br>
+.. Copyright (C) 2022, 2023 Trinity College Dublin<br>
.. Copyright (C) 2020 Richi Dubey (<a href="mailto:richidubey@gmail.com" target="_blank">richidubey@gmail.com</a>)<br>
.. Copyright (C) 2015, 2023 embedded brains GmbH & Co. KG<br>
.. Copyright (C) 1988, 1998 On-Line Applications Research Corporation (OAR)<br>
@@ -17,6 +18,9 @@ Glossary<br>
A term used to describe an object which has been created by an<br>
application.<br>
<br>
+ AMP<br>
+ This term is an acronym for Asymmetric Multiprocessing.<br>
+<br>
APA<br>
This term is an acronym for Arbitrary Processor Affinity. APA schedulers<br>
allow a thread to have an arbitrary affinity to a processor set, rather than<br>
@@ -357,6 +361,10 @@ Glossary<br>
mathematically intensive situations. It is typically viewed as a logical<br>
extension of the primary processor.<br>
<br>
+ formal model<br>
+ A model of a computing component (hardware or software) that has a<br>
+ mathematically based :term:`semantics`.<o:p></o:p></p>
</blockquote>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">This is in the neighborhood of the definitions I found but is missing a word<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">like rigorous.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">For me "mathematically based" implies "rigorous", but I think you are right to emphasise this<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">How about: "A rigorous model of ...." ?<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<p class="MsoNormal" style="margin-left:36.0pt">+<br>
freed<br>
A resource that has been released by the application to RTEMS.<br>
<br>
@@ -386,6 +394,14 @@ Glossary<br>
GNU<br>
This term is an acronym for `GNU's Not Unix <<a href="https://www.gnu.org/" target="_blank">https://www.gnu.org/</a>>`_.<br>
<br>
+ GPL<br>
+ This term is an acronym for<br>
+ `GNU General Public License <<a href="https://www.gnu.org/licenses" target="_blank">https://www.gnu.org/licenses</a>>`__.<br>
+<br>
+ GPLv3<br>
+ This term is an acronym for<br>
+ `GNU General Public License Version 3 <<a href="https://www.gnu.org/licenses/gpl-3.0.html" target="_blank">https://www.gnu.org/licenses/gpl-3.0.html</a>>`__.<br>
+<o:p></o:p></p>
</blockquote>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Do we need to include an entry for the GPLv2 w/exception that is actually used by some RTEMS code.<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<p class="MsoNormal" style="margin-left:36.0pt"> GR712RC<br>
The<br>
`GR712RC <<a href="https://www.gaisler.com/index.php/products/components/gr712rc" target="_blank">https://www.gaisler.com/index.php/products/components/gr712rc</a>>`_<br>
@@ -511,6 +527,10 @@ Glossary<br>
LIFO<br>
This term is an acronym for :term:`Last In First Out`.<br>
<br>
+ Linear Temporal Logic<br>
+ This is a logic that states properties about (possibly infinite) sequences of<br>
+ states.<br>
+<br>
list<br>
A data structure which allows for dynamic addition and removal of<br>
entries. It is not statically limited to a particular size.<br>
@@ -520,6 +540,12 @@ Glossary<br>
are arranged such that the least significant byte is at the lowest<br>
address.<br>
<br>
+ LLVM<br>
+ This term is an acronym for<br>
+ `Low Level Virtual Machine <<a href="https://www.llvm.org" target="_blank">https://www.llvm.org</a>>`__.<br>
+ The LLVM Project is a collection of modular and reusable compiler and<br>
+ toolchain technologies.<br>
+<br>
local<br>
An object which was created with the LOCAL attribute and is accessible<br>
only on the node it was created and resides upon. In a single processor<br>
@@ -541,6 +567,9 @@ Glossary<br>
A :term:`task` ``L`` has a lower :term:`priority` than a task ``H``, if<br>
task ``L`` is less important than task ``H``.<br>
<br>
+ LTL<br>
+ This term is an acronym for :term:`Linear Temporal Logic`.<br>
+<br>
major number<br>
The index of a device driver in the Device Driver Table.<br>
<br>
@@ -632,6 +661,9 @@ Glossary<br>
mathematically intensive situations. It is typically viewed as a logical<br>
extension of the primary processor.<br>
<br>
+ OBC<br>
+ This term is an acronym for On-Board Computer.<br>
+<br>
object<br>
In this document, this term is used to refer collectively to tasks,<br>
timers, message queues, partitions, regions, semaphores, ports, and rate<br>
@@ -806,6 +838,10 @@ Glossary<br>
A term used to describe routines which do not modify themselves or global<br>
variables.<br>
<br>
+ refinement<br>
+ A *refinement* is a relationship between a specification and its<br>
+ implementation as code.<br>
+<br>
region<br>
An RTEMS object which is used to allocate and deallocate variable size<br>
blocks of memory from a dynamically specified area of memory.<br>
@@ -818,6 +854,9 @@ Glossary<br>
Registers are locations physically located within a component, typically<br>
used for device control or general purpose storage.<br>
<br>
+ reification<br>
+ Another term used to denote :term:`refinement`.<br>
+<br>
remote<br>
Any object that does not reside on the local node.<br>
<br>
@@ -865,6 +904,12 @@ Glossary<br>
The state of a rate monotonic timer while it is being used to delineate a<br>
period. The timer exits this state by either expiring or being canceled.<br>
<br>
+ scenario<br>
+ In a setting that involves many concurrent tasks that interleave in arbitrary<br>
+ ways, a scenario describes a single specific possible interleaving. One<br>
+ interpretation of the behaviour of a concurrent system is the set of all its<br>
+ scenarios.<br>
+<o:p></o:p></p>
</blockquote>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">This doesn't cover the common use case of a test scenario which is usually <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">less about threading and more about values and using a set of methods in<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">a particular manner. <o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">In the context in which Sebastian asked me for this entry, the term `scenario` is used as described above.<o:p></o:p></p>
<p class="MsoNormal">But you are right that there are nuances here. In the Promela/SPIN based test-generation work, each<br>
counter example we get from SPIN describes a scenario as defined above, and we generate C test code<br>
that reproduces that scenario, including the precise interleaving of the tasks as per that scenario.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<p class="MsoNormal" style="margin-left:36.0pt"> schedulable<br>
A set of tasks which can be guaranteed to meet their deadlines based upon<br>
a specific scheduling algorithm.<br>
@@ -901,6 +946,11 @@ Glossary<br>
segments<br>
Variable sized memory blocks allocated from a region.<br>
<br>
+ semantics<br>
+ This term refers to the meaning of text or utterances in some language. In a<br>
+ software engineering context these will be programming, modelling or<br>
+ specification languages.<br>
+<br>
semaphore<br>
An RTEMS object which is used to synchronize tasks and provide mutually<br>
exclusive access to resources.<br>
diff --git a/eng/fv/approaches.rst b/eng/fv/approaches.rst<br>
index 6bbac20..fe58a06 100644<br>
--- a/eng/fv/approaches.rst<br>
+++ b/eng/fv/approaches.rst<br>
@@ -168,7 +168,7 @@ in such a way that tests can be generated using the SPIN model checker<br>
Promela is quite a low-level modelling language that makes it easy to get close<br>
to code level, and is specifically targeted to modelling software. It is one of<br>
the most widely used model-checkers, both in industry and education. It uses<br>
-assertions, and :term:`Linear Temporal Logic` (LTL) to express properties of<br>
+assertions, and :term:`Linear Temporal Logic` (:term:`LTL`) to express properties of<br>
interest.<br>
<br>
Given a Promela model that checks key properties successfully,<br>
diff --git a/eng/fv/overview.rst b/eng/fv/overview.rst<br>
index 15ce7d8..da981f2 100755<br>
--- a/eng/fv/overview.rst<br>
+++ b/eng/fv/overview.rst<br>
@@ -30,9 +30,9 @@ such as a specification. This relationship is commonly referred to as a<br>
<br>
Often it is quite difficult to get a useful formal model of real code. Some<br>
formal modelling approaches are capable of generating machine-readable<br>
-:term:`scenarios` that describe possible correct behaviors of the system at the<br>
-relevant level of abstraction. A refinement for these can be defined by<br>
-using them to generate test code.<br>
+:term:`scenarios <scenario>` that describe possible correct behaviors of the<br>
+system at the relevant level of abstraction. A refinement for these can be<br>
+defined by using them to generate test code.<o:p></o:p></p>
</blockquote>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">This definition of scenario is different from the one in the glossary. It<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">is more inline with what I expected.<o:p></o:p></p>
<p class="MsoNormal"><o:p> </o:p></p>
<p class="MsoNormal">Hmmm. For me, the use of scenarios up above is precisely the same as per the scenario glossary entry!<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"> <o:p></o:p></p>
</div>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<p class="MsoNormal" style="margin-left:36.0pt"> This is the technique that is used in :ref:`FormalVerifMethodology` to<br>
verify parts of RTEMS. Formal models are constructed based on requirements<br>
documentation, and are used as a basis for test generation.<br>
diff --git a/eng/glossary.rst b/eng/glossary.rst<br>
index 0e0b708..42cadc4 100644<br>
--- a/eng/glossary.rst<br>
+++ b/eng/glossary.rst<br>
@@ -1,5 +1,6 @@<br>
.. SPDX-License-Identifier: CC-BY-SA-4.0<br>
<br>
+.. Copyright (C) 2022, 2023 Trinity College Dublin<br>
.. Copyright (C) 2017, 2019 embedded brains GmbH & Co. KG<br>
.. Copyright (C) 1988, 1998 On-Line Applications Research Corporation (OAR)<br>
<br>
@@ -39,6 +40,10 @@ Glossary<br>
This term is an acronym for<br>
`Executable and Linkable Format <<a href="https://en.wikipedia.org/wiki/Executable_and_Linkable_Format" target="_blank">https://en.wikipedia.org/wiki/Executable_and_Linkable_Format</a>>`_.<br>
<br>
+ formal model<br>
+ A model of a computing component (hardware or software) that has a<br>
+ mathematically based :term:`semantics`.<o:p></o:p></p>
</blockquote>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">Why is this duplicated? Don't we have a single glossary file? <o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt">There are other duplicates below. Can we have a single source of truth?<o:p></o:p></p>
</div>
<div>
<p class="MsoNormal" style="margin-left:36.0pt"><o:p> </o:p></p>
</div>
<blockquote style="border:none;border-left:solid #CCCCCC 1.0pt;padding:0cm 0cm 0cm 6.0pt;margin-left:4.8pt;margin-right:0cm">
<p class="MsoNormal" style="margin-left:36.0pt"> +<br>
GCC<br>
This term is an acronym for `GNU Compiler Collection <<a href="https://gcc.gnu.org/" target="_blank">https://gcc.gnu.org/</a>>`_.<br>
<br>
@@ -64,15 +69,15 @@ Glossary<br>
This term is an acronym for Independent Software Verification and Validation.<br>
<br>
Linear Temporal Logic<br>
- This is a logic that states properties about<br>
- (possibly infinite) sequences of states.<br>
+ This is a logic that states properties about (possibly infinite) sequences of<br>
+ states.<br>
<br>
LTL<br>
- This term is an acronym for Linear Temporal Logic.<br>
+ This term is an acronym for :term:`Linear Temporal Logic`.<br>
<br>
refinement<br>
- A *refinement* is a relationship between a specification<br>
- and its implementation as code.<br>
+ A *refinement* is a relationship between a specification and its<br>
+ implementation as code.<br>
<br>
reification<br>
Another term used to denote :term:`refinement`.<br>
@@ -84,6 +89,17 @@ Glossary<br>
RTEMS<br>
This term is an acronym for Real-Time Executive for Multiprocessor Systems.<br>
<br>
+ scenario<br>
+ In a setting that involves many concurrent tasks that interleave in arbitrary<br>
+ ways, a scenario describes a single specific possible interleaving. One<br>
+ interpretation of the behaviour of a concurrent system is the set of all its<br>
+ scenarios.<br>
+<br>
+ semantics<br>
+ This term refers to the meaning of text or utterances in some language. In a<br>
+ software engineering context these will be programming, modelling or<br>
+ specification languages.<br>
+<br>
software component<br>
This term is defined by ECSS-E-ST-40C 3.2.28 as a "part of a software<br>
system". For this project a *software component* shall be any of the<br>
-- <br>
2.35.3<br>
<br>
_______________________________________________<br>
devel mailing list<br>
<a href="mailto:devel@rtems.org" target="_blank">devel@rtems.org</a><br>
<a href="http://lists.rtems.org/mailman/listinfo/devel" target="_blank">http://lists.rtems.org/mailman/listinfo/devel</a><o:p></o:p></p>
</blockquote>
</div>
</div>
</div>
</body>
</html>