summaryrefslogtreecommitdiffstats
path: root/eng/glossary.rst
diff options
context:
space:
mode:
authorAndrew Butterfield <andrew.butterfield@scss.tcd.ie>2023-11-09 11:26:56 +0000
committerSebastian Huber <sebastian.huber@embedded-brains.de>2023-11-09 13:44:36 +0100
commit2c88912893ebbcc3b9fa14d4fcc100c42252d0df (patch)
treeb4c31ddb99acab7aed836fbfaef1557bdc12fce3 /eng/glossary.rst
parentuser/exe: Add MicroBlaze to Dynamic Loader architecture list (diff)
downloadrtems-docs-2c88912893ebbcc3b9fa14d4fcc100c42252d0df.tar.bz2
eng: Add formal verification chapter
Diffstat (limited to 'eng/glossary.rst')
-rw-r--r--eng/glossary.rst14
1 files changed, 14 insertions, 0 deletions
diff --git a/eng/glossary.rst b/eng/glossary.rst
index da23fea..0e0b708 100644
--- a/eng/glossary.rst
+++ b/eng/glossary.rst
@@ -63,6 +63,20 @@ Glossary
ISVV
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.
+
+ LTL
+ This term is an acronym for Linear Temporal Logic.
+
+ refinement
+ A *refinement* is a relationship between a specification
+ and its implementation as code.
+
+ reification
+ Another term used to denote :term:`refinement`.
+
ReqIF
This term is an acronym for
`Requirements Interchange Format <https://www.omg.org/spec/ReqIF/About-ReqIF/>`_.