diff options
author | Sebastian Huber <sebastian.huber@embedded-brains.de> | 2023-11-21 11:32:41 +0100 |
---|---|---|
committer | Sebastian Huber <sebastian.huber@embedded-brains.de> | 2023-12-19 08:30:54 +0100 |
commit | ef49c4692b80f5476bceb8d1c587a9600c04febe (patch) | |
tree | d4f713e4dc3e88afd93a4ccd3cd5ef796965a6b4 /eng | |
parent | bsps/imxrt: Document GPIO CS pins for LPSPI (diff) | |
download | rtems-docs-ef49c4692b80f5476bceb8d1c587a9600c04febe.tar.bz2 |
glossary: Add terms
Diffstat (limited to 'eng')
-rw-r--r-- | eng/fv/approaches.rst | 2 | ||||
-rwxr-xr-x | eng/fv/overview.rst | 6 | ||||
-rw-r--r-- | eng/glossary.rst | 26 |
3 files changed, 25 insertions, 9 deletions
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..a015eda 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 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 |