On Tue, Nov 28, 2023 at 10:27 AM Sebastian Huber < 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) > .. 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. > + > 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. > 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. > 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 > http://lists.rtems.org/mailman/listinfo/devel >
_______________________________________________ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel
