diff options
author | Andrew Butterfield <andrew.butterfield@scss.tcd.ie> | 2023-11-28 14:43:41 +0100 |
---|---|---|
committer | Sebastian Huber <sebastian.huber@embedded-brains.de> | 2023-11-28 17:24:53 +0100 |
commit | 9a339d9ca421861e910d9e89c3ae76f7062d2f8f (patch) | |
tree | c4428f11c50c1c4d41b35c235ceaaa0f6e2f8504 | |
parent | modules: Update rtems (diff) | |
download | rtems-central-9a339d9ca421861e910d9e89c3ae76f7062d2f8f.tar.bz2 |
glossary: Add formal methods terms
-rw-r--r-- | spec-glossary/glossary/formal-model.yml | 13 | ||||
-rw-r--r-- | spec-glossary/glossary/linear-temporal-logic.yml | 13 | ||||
-rw-r--r-- | spec-glossary/glossary/ltl.yml | 12 | ||||
-rw-r--r-- | spec-glossary/glossary/refinement.yml | 13 | ||||
-rw-r--r-- | spec-glossary/glossary/reification.yml | 12 | ||||
-rw-r--r-- | spec-glossary/glossary/scenario.yml | 15 | ||||
-rw-r--r-- | spec-glossary/glossary/semantics.yml | 14 |
7 files changed, 92 insertions, 0 deletions
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 |