---
c-user/glossary.rst | 50 +++++++++++++++++++++++++++++++++++++++++++
eng/fv/approaches.rst | 2 +-
eng/fv/overview.rst | 6 +++---
eng/glossary.rst | 26 +++++++++++++++++-----
4 files changed, 75 insertions(+), 9 deletions(-)
diff --git a/c-user/glossary.rst b/c-user/glossary.rst
index 82aedcd..9a9d12c 100644
--- a/c-user/glossary.rst
+++ b/c-user/glossary.rst
@@ -1,5 +1,6 @@
.. SPDX-License-Identifier: CC-BY-SA-4.0
+.. Copyright (C) 2022, 2023 Trinity College Dublin
.. Copyright (C) 2020 Richi Dubey (richidu...@gmail.com)
.. Copyright (C) 2015, 2023 embedded brains GmbH & Co. KG
.. Copyright (C) 1988, 1998 On-Line Applications Research Corporation (OAR)
@@ -17,6 +18,9 @@ Glossary
A term used to describe an object which has been created by an
application.
+ AMP
+ This term is an acronym for Asymmetric Multiprocessing.
+
APA
This term is an acronym for Arbitrary Processor Affinity. APA
schedulers
allow a thread to have an arbitrary affinity to a processor set,
rather than
@@ -357,6 +361,10 @@ Glossary
mathematically intensive situations. It is typically viewed as a
logical
extension of the primary processor.
+ formal model
+ A model of a computing component (hardware or software) that has a
+ mathematically based :term:`semantics`.
+
freed
A resource that has been released by the application to RTEMS.
@@ -386,6 +394,14 @@ Glossary
GNU
This term is an acronym for `GNU's Not Unix <https://www.gnu.org/>`_.
+ GPL
+ This term is an acronym for
+ `GNU General Public License <https://www.gnu.org/licenses>`__.
+
+ GPLv3
+ This term is an acronym for
+ `GNU General Public License Version 3
<https://www.gnu.org/licenses/gpl-3.0.html>`__.
+
GR712RC
The
`GR712RC
<https://www.gaisler.com/index.php/products/components/gr712rc>`_
@@ -511,6 +527,10 @@ Glossary
LIFO
This term is an acronym for :term:`Last In First Out`.
+ Linear Temporal Logic
+ This is a logic that states properties about (possibly infinite)
sequences of
+ states.
+
list
A data structure which allows for dynamic addition and removal of
entries. It is not statically limited to a particular size.
@@ -520,6 +540,12 @@ Glossary
are arranged such that the least significant byte is at the lowest
address.
+ LLVM
+ This term is an acronym for
+ `Low Level Virtual Machine <https://www.llvm.org>`__.
+ The LLVM Project is a collection of modular and reusable compiler and
+ toolchain technologies.
+
local
An object which was created with the LOCAL attribute and is accessible
only on the node it was created and resides upon. In a single
processor
@@ -541,6 +567,9 @@ Glossary
A :term:`task` ``L`` has a lower :term:`priority` than a task ``H``, if
task ``L`` is less important than task ``H``.
+ LTL
+ This term is an acronym for :term:`Linear Temporal Logic`.
+
major number
The index of a device driver in the Device Driver Table.
@@ -632,6 +661,9 @@ Glossary
mathematically intensive situations. It is typically viewed as a
logical
extension of the primary processor.
+ OBC
+ This term is an acronym for On-Board Computer.
+
object
In this document, this term is used to refer collectively to tasks,
timers, message queues, partitions, regions, semaphores, ports, and
rate
@@ -806,6 +838,10 @@ Glossary
A term used to describe routines which do not modify themselves or
global
variables.
+ refinement
+ A *refinement* is a relationship between a specification and its
+ implementation as code.
+
region
An RTEMS object which is used to allocate and deallocate variable size
blocks of memory from a dynamically specified area of memory.
@@ -818,6 +854,9 @@ Glossary
Registers are locations physically located within a component,
typically
used for device control or general purpose storage.
+ reification
+ Another term used to denote :term:`refinement`.
+
remote
Any object that does not reside on the local node.
@@ -865,6 +904,12 @@ Glossary
The state of a rate monotonic timer while it is being used to
delineate a
period. The timer exits this state by either expiring or being
canceled.
+ scenario
+ In a setting that involves many concurrent tasks that interleave in
arbitrary
+ ways, a scenario describes a single specific possible interleaving.
One
+ interpretation of the behaviour of a concurrent system is the set of
all its
+ scenarios.
+
schedulable
A set of tasks which can be guaranteed to meet their deadlines based
upon
a specific scheduling algorithm.
@@ -901,6 +946,11 @@ Glossary
segments
Variable sized memory blocks allocated from a region.
+ semantics
+ This term refers to the meaning of text or utterances in some
language. In a
+ software engineering context these will be programming, modelling or
+ specification languages.
+
semaphore
An RTEMS object which is used to synchronize tasks and provide mutually
exclusive access to resources.
diff --git a/eng/fv/approaches.rst b/eng/fv/approaches.rst
index 6bbac20..fe58a06 100644
--- a/eng/fv/approaches.rst
+++ b/eng/fv/approaches.rst
@@ -168,7 +168,7 @@ in such a way that tests can be generated using the SPIN
model checker
Promela is quite a low-level modelling language that makes it easy to get close
to code level, and is specifically targeted to modelling software. It is one of
the most widely used model-checkers, both in industry and education. It uses
-assertions, and :term:`Linear Temporal Logic` (LTL) to express properties of
+assertions, and :term:`Linear Temporal Logic` (:term:`LTL`) to express
properties of
interest.
Given a Promela model that checks key properties successfully,
diff --git a/eng/fv/overview.rst b/eng/fv/overview.rst
index 15ce7d8..da981f2 100755
--- a/eng/fv/overview.rst
+++ b/eng/fv/overview.rst
@@ -30,9 +30,9 @@ such as a specification. This relationship is commonly
referred to as a
Often it is quite difficult to get a useful formal model of real code. Some
formal modelling approaches are capable of generating machine-readable
-:term:`scenarios` that describe possible correct behaviors of the system at the
-relevant level of abstraction. A refinement for these can be defined by
-using them to generate test code.
+:term:`scenarios <scenario>` that describe possible correct behaviors of the
+system at the relevant level of abstraction. A refinement for these can be
+defined by using them to generate test code.
This is the technique that is used in :ref:`FormalVerifMethodology` to
verify parts of RTEMS. Formal models are constructed based on requirements
documentation, and are used as a basis for test generation.
diff --git a/eng/glossary.rst b/eng/glossary.rst
index 0e0b708..42cadc4 100644
--- a/eng/glossary.rst
+++ b/eng/glossary.rst
@@ -1,5 +1,6 @@
.. SPDX-License-Identifier: CC-BY-SA-4.0
+.. Copyright (C) 2022, 2023 Trinity College Dublin
.. Copyright (C) 2017, 2019 embedded brains GmbH & Co. KG
.. Copyright (C) 1988, 1998 On-Line Applications Research Corporation (OAR)
@@ -39,6 +40,10 @@ Glossary
This term is an acronym for
`Executable and Linkable Format
<https://en.wikipedia.org/wiki/Executable_and_Linkable_Format>`_.
+ formal model
+ A model of a computing component (hardware or software) that has a
+ mathematically based :term:`semantics`.
+
GCC
This term is an acronym for `GNU Compiler Collection
<https://gcc.gnu.org/>`_.
@@ -64,15 +69,15 @@ Glossary
This term is an acronym for Independent Software Verification and
Validation.
Linear Temporal Logic
- This is a logic that states properties about
- (possibly infinite) sequences of states.
+ This is a logic that states properties about (possibly infinite)
sequences of
+ states.
LTL
- This term is an acronym for Linear Temporal Logic.
+ This term is an acronym for :term:`Linear Temporal Logic`.
refinement
- A *refinement* is a relationship between a specification
- and its implementation as code.
+ A *refinement* is a relationship between a specification and its
+ implementation as code.
reification
Another term used to denote :term:`refinement`.
@@ -84,6 +89,17 @@ Glossary
RTEMS
This term is an acronym for Real-Time Executive for Multiprocessor
Systems.
+ scenario
+ In a setting that involves many concurrent tasks that interleave in
arbitrary
+ ways, a scenario describes a single specific possible interleaving.
One
+ interpretation of the behaviour of a concurrent system is the set of
all its
+ scenarios.
+
+ semantics
+ This term refers to the meaning of text or utterances in some
language. In a
+ software engineering context these will be programming, modelling or
+ specification languages.
+
software component
This term is defined by ECSS-E-ST-40C 3.2.28 as a "part of a software
system". For this project a *software component* shall be any of the
--
2.35.3
_______________________________________________
devel mailing list
devel@rtems.org
http://lists.rtems.org/mailman/listinfo/devel
