mirror of
https://git.rtems.org/rtems-docs/
synced 2025-05-14 15:19:22 +08:00
glossary: Add terms
This commit is contained in:
Sebastian Huber
parent
6744793931
commit
ef49c4692b
@ -1,5 +1,6 @@
|
||||
.. SPDX-License-Identifier: CC-BY-SA-4.0
|
||||
|
||||
.. Copyright (C) 2022, 2023 Trinity College Dublin
|
||||
.. Copyright (C) 2020 Richi Dubey (richidubey@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,18 @@ 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>`__.
|
||||
|
||||
GPLv2
|
||||
This term is an acronym for
|
||||
`GNU General Public License Version 2 <https://www.gnu.org/licenses/old-licenses/gpl-2.0.html>`__.
|
||||
|
||||
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 +531,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 +544,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 +571,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 +665,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 +842,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 +858,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 +908,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 the context of formal verification, 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 +950,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.
|
||||
|
||||
@ -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,
|
||||
|
||||
@ -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.
|
||||
|
||||
@ -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 the context of formal verification, 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
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user