<div dir="ltr"><div dir="ltr"><br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">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:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">---<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`.<br></blockquote><div><br></div><div>This is in the neighborhood of the definitions I found but is missing a word</div><div>like rigorous.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
+<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/" rel="noreferrer" 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" rel="noreferrer" 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" rel="noreferrer" target="_blank">https://www.gnu.org/licenses/gpl-3.0.html</a>>`__.<br>
+<br></blockquote><div><br></div><div>Do we need to include an entry for the GPLv2 w/exception that is actually used by some RTEMS code.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
GR712RC<br>
The<br>
`GR712RC <<a href="https://www.gaisler.com/index.php/products/components/gr712rc" rel="noreferrer" 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" rel="noreferrer" 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>
+<br></blockquote><div><br></div><div>This doesn't cover the common use case of a test scenario which is usually </div><div>less about threading and more about values and using a set of methods in</div><div>a particular manner. </div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
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.<br></blockquote><div><br></div><div>This definition of scenario is different from the one in the glossary. It</div><div>is more inline with what I expected.</div><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
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" rel="noreferrer" 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`.<br></blockquote><div><br></div><div>Why is this duplicated? Don't we have a single glossary file? </div><div><br></div><div>There are other duplicates below. Can we have a single source of truth?</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"> +<br>
GCC<br>
This term is an acronym for `GNU Compiler Collection <<a href="https://gcc.gnu.org/" rel="noreferrer" 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" rel="noreferrer" target="_blank">http://lists.rtems.org/mailman/listinfo/devel</a><br>
</blockquote></div></div>