From: devel <devel-boun...@rtems.org> on behalf of Joel Sherrill <j...@rtems.org> Reply to: "j...@rtems.org" <j...@rtems.org> Date: Tuesday 28 November 2023 at 19:31 To: Sebastian Huber <sebastian.hu...@embedded-brains.de> Cc: "devel@rtems.org" <devel@rtems.org> Subject: Re: [PATCH] glossary: Add terms
On Tue, Nov 28, 2023 at 10:27 AM Sebastian Huber <sebastian.hu...@embedded-brains.de<mailto:sebastian.hu...@embedded-brains.de>> wrote: --- 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<mailto: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`. This is in the neighborhood of the definitions I found but is missing a word like rigorous. For me "mathematically based" implies "rigorous", but I think you are right to emphasise this How about: "A rigorous model of ...." ? + 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>`__. + Do we need to include an entry for the GPLv2 w/exception that is actually used by some RTEMS code. 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. + This doesn't cover the common use case of a test scenario which is usually less about threading and more about values and using a set of methods in a particular manner. In the context in which Sebastian asked me for this entry, the term `scenario` is used as described above. But you are right that there are nuances here. In the Promela/SPIN based test-generation work, each counter example we get from SPIN describes a scenario as defined above, and we generate C test code that reproduces that scenario, including the precise interleaving of the tasks as per that scenario. 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 definition of scenario is different from the one in the glossary. It is more inline with what I expected. Hmmm. For me, the use of scenarios up above is precisely the same as per the scenario glossary entry! 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`. Why is this duplicated? Don't we have a single glossary file? There are other duplicates below. Can we have a single source of truth? + 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<mailto:devel@rtems.org> http://lists.rtems.org/mailman/listinfo/devel
_______________________________________________ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
