[rtems-central commit] glossary: Add formal methods terms

[Sebastian Huber]

Module:    rtems-central
Branch:    master
Commit:    9a339d9ca421861e910d9e89c3ae76f7062d2f8f
Changeset: http://git.rtems.org/rtems-central/commit/?id=9a339d9ca421861e910d9e89c3ae76f7062d2f8f

Author:    Andrew Butterfield <andrew.butterfield at scss.tcd.ie>
Date:      Tue Nov 28 14:43:41 2023 +0100

glossary: Add formal methods terms

---

 spec-glossary/glossary/formal-model.yml          | 13 +++++++++++++
 spec-glossary/glossary/linear-temporal-logic.yml | 13 +++++++++++++
 spec-glossary/glossary/ltl.yml                   | 12 ++++++++++++
 spec-glossary/glossary/refinement.yml            | 13 +++++++++++++
 spec-glossary/glossary/reification.yml           | 12 ++++++++++++
 spec-glossary/glossary/scenario.yml              | 15 +++++++++++++++
 spec-glossary/glossary/semantics.yml             | 14 ++++++++++++++
 7 files changed, 92 insertions(+)

diff --git a/spec-glossary/glossary/formal-model.yml b/spec-glossary/glossary/formal-model.yml
new file mode 100644
index 00000000..da208631
--- /dev/null
+++ b/spec-glossary/glossary/formal-model.yml
@@ -0,0 +1,13 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+copyrights:
+- Copyright (C) 2023 Trinity College Dublin
+enabled-by: true
+glossary-type: term
+links:
+- role: glossary-member
+  uid: ../glossary-general
+term: formal model
+text: |
+  A model of a computing component (hardware or software) that has a
+  mathematically based ${semantics:/term}.
+type: glossary
diff --git a/spec-glossary/glossary/linear-temporal-logic.yml b/spec-glossary/glossary/linear-temporal-logic.yml
new file mode 100644
index 00000000..5dc67f55
--- /dev/null
+++ b/spec-glossary/glossary/linear-temporal-logic.yml
@@ -0,0 +1,13 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+copyrights:
+- Copyright (C) 2022 Trinity College Dublin
+enabled-by: true
+glossary-type: term
+links:
+- role: glossary-member
+  uid: ../glossary-general
+term: Linear Temporal Logic
+text: |
+  This is a logic that states properties about (possibly infinite) sequences of
+  states.
+type: glossary
diff --git a/spec-glossary/glossary/ltl.yml b/spec-glossary/glossary/ltl.yml
new file mode 100644
index 00000000..7536fd9a
--- /dev/null
+++ b/spec-glossary/glossary/ltl.yml
@@ -0,0 +1,12 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+copyrights:
+- Copyright (C) 2022 Trinity College Dublin
+enabled-by: true
+glossary-type: term
+links:
+- role: glossary-member
+  uid: ../glossary-general
+term: LTL
+text: |
+  This term is an acronym for ${linear-temporal-logic:/term}.
+type: glossary
diff --git a/spec-glossary/glossary/refinement.yml b/spec-glossary/glossary/refinement.yml
new file mode 100644
index 00000000..e0cc4281
--- /dev/null
+++ b/spec-glossary/glossary/refinement.yml
@@ -0,0 +1,13 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+copyrights:
+- Copyright (C) 2022 Trinity College Dublin
+enabled-by: true
+glossary-type: term
+links:
+- role: glossary-member
+  uid: ../glossary-general
+term: refinement
+text: |
+  A *refinement* is a relationship between a specification and its
+  implementation as code.
+type: glossary
diff --git a/spec-glossary/glossary/reification.yml b/spec-glossary/glossary/reification.yml
new file mode 100644
index 00000000..1c36ab4c
--- /dev/null
+++ b/spec-glossary/glossary/reification.yml
@@ -0,0 +1,12 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+copyrights:
+- Copyright (C) 2022 Trinity College Dublin
+enabled-by: true
+glossary-type: term
+links:
+- role: glossary-member
+  uid: ../glossary-general
+term: reification
+text: |
+  Another term used to denote ${refinement:/term}.
+type: glossary
diff --git a/spec-glossary/glossary/scenario.yml b/spec-glossary/glossary/scenario.yml
new file mode 100644
index 00000000..6db3cd86
--- /dev/null
+++ b/spec-glossary/glossary/scenario.yml
@@ -0,0 +1,15 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+copyrights:
+- Copyright (C) 2023 Trinity College Dublin
+enabled-by: true
+glossary-type: term
+links:
+- role: glossary-member
+  uid: ../glossary-general
+term: scenario
+text: |
+  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.
+type: glossary
diff --git a/spec-glossary/glossary/semantics.yml b/spec-glossary/glossary/semantics.yml
new file mode 100644
index 00000000..b3442349
--- /dev/null
+++ b/spec-glossary/glossary/semantics.yml
@@ -0,0 +1,14 @@
+SPDX-License-Identifier: CC-BY-SA-4.0 OR BSD-2-Clause
+copyrights:
+- Copyright (C) 2023 Trinity College Dublin
+enabled-by: true
+glossary-type: term
+links:
+- role: glossary-member
+  uid: ../glossary-general
+term: semantics
+text: |
+  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.
+type: glossary