[rtems-docs commit] eng: Add formal verification chapter
Sebastian Huber
sebh at rtems.org
Thu Nov 9 12:18:36 UTC 2023
Module: rtems-docs
Branch: master
Commit: 2c88912893ebbcc3b9fa14d4fcc100c42252d0df
Changeset: http://git.rtems.org/rtems-docs/commit/?id=2c88912893ebbcc3b9fa14d4fcc100c42252d0df
Author: Andrew Butterfield <andrew.butterfield at scss.tcd.ie>
Date: Thu Nov 9 11:26:56 2023 +0000
eng: Add formal verification chapter
---
common/refs.bib | 75 ++
eng/fv/appendix-fv.rst | 1749 ++++++++++++++++++++++++++++++++++++++++++++++
eng/fv/approaches.rst | 178 +++++
eng/fv/index.rst | 16 +
eng/fv/methodology.rst | 62 ++
eng/fv/overview.rst | 38 +
eng/fv/promela-index.rst | 9 +
eng/fv/promela.rst | 323 +++++++++
eng/fv/refinement.rst | 559 +++++++++++++++
eng/fv/tool-setup.rst | 317 +++++++++
eng/glossary.rst | 14 +
eng/index.rst | 3 +
12 files changed, 3343 insertions(+)
diff --git a/common/refs.bib b/common/refs.bib
index 066d746..e22dd6d 100644
--- a/common/refs.bib
+++ b/common/refs.bib
@@ -9,6 +9,23 @@
year = {1973},
pages = {46-61},
}
+ at article{Djikstra:1975:GCL,
+author = {Dijkstra, Edsger W.},
+title = {Guarded Commands, Nondeterminacy and Formal Derivation of Programs},
+year = {1975},
+issue_date = {Aug. 1975},
+publisher = {Association for Computing Machinery},
+address = {New York, NY, USA},
+volume = {18},
+number = {8},
+issn = {0001-0782},
+url = {https://doi.org/10.1145/360933.360975},
+doi = {10.1145/360933.360975},
+journal = {Commun. ACM},
+month = {aug},
+pages = {453–457},
+numpages = {5},
+}
@inproceedings{Varghese:1987:TimerWheel,
author = {Varghese, G. and Lauck, T.},
title = {{Hashed and Hierarchical Timing Wheels: Data Structures for the Efficient Implementation of a Timer Facility}},
@@ -159,6 +176,31 @@
year = {2007},
url = {http://www.akkadia.org/drepper/cpumemory.pdf},
}
+ at article{Hierons:2009:FMT,
+ author = {Robert M. Hierons and
+ Kirill Bogdanov and
+ Jonathan P. Bowen and
+ Rance Cleaveland and
+ John Derrick and
+ Jeremy Dick and
+ Marian Gheorghe and
+ Mark Harman and
+ Kalpesh Kapoor and
+ Paul J. Krause and
+ Gerald L{\"{u}}ttgen and
+ Anthony J. H. Simons and
+ Sergiy A. Vilkomir and
+ Martin R. Woodward and
+ Hussein Zedan},
+ title = {Using formal specifications to support testing},
+ journal = {{ACM} Comput. Surv.},
+ volume = {41},
+ number = {2},
+ pages = {9:1--9:76},
+ year = {2009},
+ url = {https://doi.org/10.1145/1459352.1459354},
+ doi = {10.1145/1459352.1459354},
+}
@inproceedings{Mavin:2009:EARS,
author = {Mavin, Alistair and Wilkinson, Philip and Harwood, Adrian and Novak, Mark},
title = {{Easy approach to requirements syntax (EARS)}},
@@ -369,6 +411,39 @@
doi = {10.1109/RE.2016.38},
url = {https://www.researchgate.net/profile/Alistair_Mavin/publication/308970788_Listens_Learned_8_Lessons_Learned_Applying_EARS/links/5ab0d42caca2721710fe5017/Listens-Learned-8-Lessons-Learned-Applying-EARS.pdf},
}
+ at manual{Butterfield:2021:FV1-200,
+ author = {Andrew Butterfield and Mike Hinchey},
+ organization = {Lero -- the Irish Software Research Centre},
+ title = {FV1-200: Formal Verification Plan},
+ year = {2021}
+}
+ at mastersthesis{Jennings:2021:FV,
+ author = {Robert Jennings},
+ title = {{Formal Verification of a Real-Time Multithreaded Operating System}},
+ school = {School of Computer Science and Statistics},
+ year = {2021},
+ type = {Master of Science in {Computer Science (MCS)}},
+ address = {Trinity College, Dublin 2, Ireland},
+ month = {August},
+}
+ at mastersthesis{Jaskuc:2022:TESTGEN,
+ author = {Jerzy Ja{\'{s}}ku{\'{c}}},
+ title = {{SPIN/Promela-Based Test Generation Framework for RTEMS Barrier Manager}},
+ school = {School of Computer Science and Statistics},
+ year = {2022},
+ type = {Master of Science in {Computer Science (MCS)}},
+ address = {Trinity College, Dublin 2, Ireland},
+ month = {April},
+}
+ at mastersthesis{Lynch:2022:TESTGEN,
+ author = {Eoin Lynch},
+ title = {{Using Promela/SPIN to do Test Generation for RTEMS-SMP}},
+ school = {School of Engineering},
+ year = {2022},
+ type = {Master of {Engineering (Computer Engineering)}},
+ address = {Trinity College, Dublin 2, Ireland},
+ month = {April},
+}
@misc{RTEMS:CPU,
title = {{RTEMS CPU Architecture Supplement}},
url = {https://docs.rtems.org/branches/master/cpu-supplement.pdf},
diff --git a/eng/fv/appendix-fv.rst b/eng/fv/appendix-fv.rst
new file mode 100755
index 0000000..687679a
--- /dev/null
+++ b/eng/fv/appendix-fv.rst
@@ -0,0 +1,1749 @@
+.. SPDX-License-Identifier: CC-BY-SA-4.0
+
+.. Copyright (C) 2022 Trinity College Dublin
+
+Appendix: RTEMS Formal Model Guide
+**********************************
+
+This appendix covers the various formal models of RTEMS that are currently in
+existence. It serves two purposes:
+one is to provide detailed documentation of each model,
+while the other is provide a guide into how to go about developing and deploying such models.
+
+The general approach followed here is to start by looking at the API documentation and identifying the key data-structures and function prototypes.
+These are then modelled appropriately in Promela.
+Then, general behavior patterns of interest are identified,
+and the Promela model is extended to provide those patterns.
+A key aspect here is exploiting the fact that Promela allows non-deterministic choices to be specified, which gives the effect of producing arbitrary orderings of model behavior.
+All of this leads to a situation were the SPIN model-checker can effectively generate scenarios for all possible interleavings.
+The final stage is mapping those scenarios to RTEMS C test code,
+which has two parts: generating machine-readable output from SPIN, and developing the refinement mapping from that output to C test code.
+
+Some familiarity is assumed here with the Software Test Framework section in this document.
+
+The following models are included in the directory ``formal/promela/models/``
+at the top-level in ``rtems-central``:
+
+Chains API (``chains/``)
+ Models the unprotected chain append and get API calls in the Classic
+ Chains API Guide. This was an early model to develop the basic methodology.
+
+Events Manager (``events/``)
+ Models the behaviour of all the API calls in the Classic Events Manager API
+ Guide. This had to tackle real concurrency and deal with multiple CPUs and priority
+ issues.
+
+Barrier Manager (``barriers/``)
+ Models the behaviour of all the API calls in then Classic Barrier Manager API.
+
+Message Manager (``messages/``)
+ Models the create, send and receive API calls in the Classic Message Manager API.
+
+At the end of this guide is a section that discusses various issues that should be tackled in future work.
+
+Testing Chains
+--------------
+
+Documentation: Chains section in the RTEMS Classic API Guide.
+
+Model Directory: ``formal/promela/models/chains``.
+
+Model Name: ``chains-api-model``.
+
+The Chains API provides a doubly-linked list data-structure, optimised for fast
+operations in an SMP setting. It was used as proof of concept exercise,
+and focussed on just two API calls: ``rtems-chain-append-unprotected``
+and ``rtems-chain-get-unprotected`` (hereinafter just ``append`` and ``get``).
+
+
+API Model
+^^^^^^^^^
+
+File: ``chains-api-model.pml``
+
+While smart code optimization techniques are very important for RTEMS code,
+the focus when constructing formal models is on functional correctness,
+not performance. What is required is the simplest, most obviously correct model.
+
+The ``append`` operation adds new nodes on the end of the list,
+while ``get`` removes and returns the node at the start of the list.
+The Chains API has many other operations that can add/remove nodes at either end, or somewhere in the middle, but these are considered out of scope.
+
+Data Structures
+~~~~~~~~~~~~~~~
+
+There are no pointers in Promela, so we have to use arrays,
+with array indices modelling pointers.
+With just ``append`` and ``get``, an array can be used to implement a collection
+of nodes in memory.
+A ``Node`` type is defined that has next and previous indices,
+plus an item payload.
+Access to the node list is via a special control node with head and tail pointers.
+In the model, an explicit size value is added to this control node,
+to allow the writing of properties about chain length,
+and to prevent array out-of-bound errors in the model itself.
+We assume a single ``chain``,
+with list node storage statically allocated in ``memory``.
+
+.. code:: c
+
+ #define PTR_SIZE 3
+ #define MEM_SIZE 8
+
+ typedef Node {
+ unsigned nxt : PTR_SIZE
+ ; unsigned prv : PTR_SIZE
+ ; byte itm
+ }
+ Node memory[MEM_SIZE] ;
+
+ typedef Control {
+ unsigned head : PTR_SIZE;
+ unsigned tail : PTR_SIZE;
+ unsigned size : PTR_SIZE
+ }
+ Control chain ;
+
+While there are 8 memory elements, element 0 is inaccessible,
+as the index 0 is treated like a ``NULL`` pointer.
+
+Function Calls
+~~~~~~~~~~~~~~
+
+The RTEMS prototype for ``append`` is:
+
+.. code:: c
+
+ void rtems_chain_append_unprotected(
+ rtems_chain_control *the_chain,
+ rtems_chain_node *the_node
+ );
+
+Its implementation starts by checking that the node to be appended is "off
+chain", before performing the append.
+The model is designed to satisfy this property so the check is not modelled.
+Also, the Chains documentation is not clear about certain error cases.
+As this is a proof of concept exercise, these details are not modelled.
+
+A Promela inline definition ``append`` models the desired behavior,
+simulating C pointers with array addresses. Here ``ch`` is the chain argument,
+while ``np`` is a node index.
+The model starts by checking that the node pointer is not ``NULL``,
+and that there is room in ``memory`` for another node.
+These are to ensure that the model does not have any runtime errors.
+Doing a standard model-check of this model finds no errors,
+which indicates that those assertions are never false.
+
+.. code:: c
+
+ inline append(ch,np) {
+ assert(np!=0); assert(ch.size < (MEM_SIZE-1));
+ if
+ :: (ch.head == 0) -> ch.head = np; ch.tail = np; ch.size = 1;
+ memory[np].nxt = 0; memory[np].prv = 0;
+ :: (ch.head != 0) -> memory[ch.tail].nxt = np; memory[np].prv = ch.tail;
+ ch.tail = np; ch.size = ch.size + 1;
+ fi
+ }
+
+The RTEMS prototype for ``get`` is:
+
+.. code:: c
+
+ rtems_chain_node *rtems_chain_get_unprotected(
+ rtems_chain_control *the_chain
+ );
+
+It returns a pointer to the node, with ``NULL`` returned if the chain is empty.
+
+Promela inlines involve textual substitution,
+so the concept of returning a value makes no sense.
+For ``get``, the model is that of a statement that assigns the return value to
+a variable. Both the function argument and return variable name are passed as parameters:
+
+.. code:: c
+
+ /* np = get(ch); */
+ inline get(ch,np) {
+ np = ch.head ;
+ if
+ :: (np != 0) ->
+ ch.head = memory[np].nxt;
+ ch.size = ch.size - 1;
+ // memory[np].nxt = 0
+ :: (np == 0) -> skip
+ fi
+ if
+ :: (ch.head == 0) -> ch.tail = 0
+ :: (ch.head != 0) -> skip
+ fi
+ }
+
+Behavior patterns
+^^^^^^^^^^^^^^^^^
+
+File: ``chains-api-model.pml``
+
+A key feature of using a modelling language like Promela is that it has both
+explicit and implicit non-determinism. This can be exploited so that SPIN will
+find all possible interleavings of behavior.
+
+The Chains API model consists of six processes, three which perform ``append``,
+and three that perform ``get``, waiting if the chain is empty. This model relies
+on implicit non-determinism, in that the SPIN scheduler can choose and switch
+between any unblocked process at any point. There is no explicit non-determinism
+in this model.
+
+Promela process ``doAppend`` takes node index ``addr`` and a value ``val`` as
+parameters. It puts ``val`` into the node indexed by ``addr``,
+then calls ``append``, and terminates.
+It is all made atomic to avoid unnecessary internal interleaving of operations because unprotected versions of API calls should only be used when interrupts
+are disabled.
+
+.. code:: c
+
+ proctype doAppend(int addr; int val) {
+ atomic{ memory[addr].itm = val;
+ append(chain,addr); } ;
+ }
+
+The ``doNonNullGet`` process waits for the chain to be non-empty before attempting to ``get`` an element. The first statement inside the atomic
+construct is an expression, as a statements, that blocks while it evaluates to
+zero. That only happens if ``head`` is in fact zero. The model also has an
+assertion that checks that a non-null node is returned.
+
+.. code:: c
+
+ proctype doNonNullGet() {
+ atomic{
+ chain.head != 0;
+ get(chain,nptr);
+ assert(nptr != 0);
+ } ;
+ }
+
+All processes terminate after they have performed their (sole) action.
+
+The top-level of a Promela model is an initial process declared by the ``init`` construct. This initializes the chain as empty and then runs all six processes concurrently. It then uses the special ``_nr_pr`` variable to wait for all six
+processes to terminate. A final assertion checks that the chain is empty.
+
+.. code:: c
+
+ init {
+ pid nr;
+ chain.head = 0; chain.tail = 0; chain.size = 0 ;
+ nr = _nr_pr; // assignment, sets `nr` to current number of procs
+ run doAppend(6,21);
+ run doAppend(3,22);
+ run doAppend(4,23);
+ run doNonNullGet();
+ run doNonNullGet();
+ run doNonNullGet();
+ nr == _nr_pr; // expression, waits until number of procs equals `nr`
+ assert (chain.size == 0);
+ }
+
+Simulation of this model will show some execution sequence in which the appends
+happen in a random order, and the gets also occur in a random order, whenever
+the chain is not empty. All assertions are always satisfied, including the last
+one above. Model checking this model explores all possible interleavings and reports no errors of any kind. In particular, when the model reaches the last
+assert statement, the chain size is always zero.
+
+SPIN uses the C pre-processor, and generates the model as a C program. This
+model has a simple flow of control: basically execute each process once in an
+almost arbitrary order, assert that the chain is empty, and terminate. Test
+generation here just requires the negation of the final assertion to get all
+possible interleavings. The special C pre-processor definition ``TEST_GEN`` is
+used to switch between the two uses of the model. The last line above is
+replaced by:
+
+.. code:: c
+
+ #ifdef TEST_GEN
+ assert (chain.size != 0);
+ #else
+ assert (chain.size == 0);
+ #endif
+
+A test generation run can then be invoked by passing in ``-DTEST_GEN`` as a
+command-line argument.
+
+Annotations
+^^^^^^^^^^^
+
+File: ``chains-api-model.pml``
+
+The model needs to have ``printf`` statements added to generation the
+annotations used to perform the test generation.
+
+This model wraps each of six API calls in its own process, so that model
+checking can generate all feasible interleavings. However, the plan for the test code is that it will be just one RTEMS Task, that executes all the API
+calls in the order determined by the scenario under consideration. All the
+annotations in this model specify ``0`` as the Promela process identifier.
+
+Data Structures
+~~~~~~~~~~~~~~~
+
+Annotations have to be provided for any variable or datastructure declarations
+that will need to have corresponding code in the test program.
+These have to be printed out as the model starts to run.
+For this model, the ``MAX_SIZE`` parameter is important,
+as are the variables ``memory``, ``nptr``, and ``chain``:
+
+.. code:: c
+
+ printf("@@@ 0 NAME Chain_AutoGen\n")
+ printf("@@@ 0 DEF MAX_SIZE 8\n");
+ printf("@@@ 0 DCLARRAY Node memory MAX_SIZE\n");
+ printf("@@@ 0 DECL unsigned nptr NULL\n")
+ printf("@@@ 0 DECL Control chain\n");
+
+At this point, a parameter-free initialization annotation is issued. This should
+be refined to C code that initializes the above variables.
+
+.. code:: c
+
+ printf("@@@INIT\n");
+
+Function Calls
+~~~~~~~~~~~~~~
+
+For ``append``, two forms of annotation are produced. One uses the ``CALL``
+format to report the function being called along with its arguments. The other
+form reports the resulting contents of the chain.
+
+.. code:: c
+
+ proctype doAppend(int addr; int val) {
+ atomic{ memory[addr].itm = val; append(chain,addr);
+ printf("@@@ 0 CALL append %d %d\n",val,addr);
+ show_chain();
+ } ;
+ }
+
+The statement ``show_chain()`` is an inline function that prints the
+contents of the chain after append returns.
+The resulting output is multi-line,
+starting with ``@@@ 0 SEQ chain``,
+ending with ``@@@ 0 END chain``,
+and with entries in between of the form ``@@@ 0 SCALAR _ val``
+displaying chain elements, line by line.
+
+Something similar is done for ``get``, with the addition of a third annotation
+``show_node()`` that shows the node that was got:
+
+.. code:: c
+
+ proctype doNonNullGet() {
+ atomic{
+ chain.head != 0;
+ get(chain,nptr);
+ printf("@@@ 0 CALL getNonNull %d\n",nptr);
+ show_chain();
+ assert(nptr != 0);
+ show_node();
+ } ;
+ }
+
+The statement ``show_node()`` is defined as follows:
+
+.. code:: c
+
+ inline show_node (){
+ atomic{
+ printf("@@@ 0 PTR nptr %d\n",nptr);
+ if
+ :: nptr -> printf("@@@ 0 STRUCT nptr\n");
+ printf("@@@ 0 SCALAR itm %d\n", memory[nptr].itm);
+ printf("@@@ 0 END nptr\n")
+ :: else -> skip
+ fi
+ }
+ }
+
+It prints out the value of ``nptr``, which is an array index. If it is not zero,
+it prints out some details of the indexed node structure.
+
+Annotations are also added to the ``init`` process to show the chain and node.
+
+.. code:: c
+
+ chain.head = 0; chain.tail = 0; chain.size = 0;
+ show_chain();
+ show_node();
+
+Refinement
+^^^^^^^^^^
+
+Files:
+
+ ``chains-api-model-rfn.yml``
+
+ ``chains-api-model-pre.h``
+
+ ``tr-chains-api-model.c``
+
+Model annotations are converted to C test code using a YAML file that maps
+single names to test code snippets into which parameters can be substituted.
+Parameters are numbered from zero, and the ``n`` th parameter will be substituted
+wherever ``{n}`` occurs in the snippet.
+
+Refinement is more than just the above mapping from annotations to code. Some of
+this code will refer to C variables, structures, and functions that are needed
+to support the test. Some of these are declared ``chains-api-model-pre.h`` and implemented in ``tr-chains-api-model.c``.
+
+Data Structures
+~~~~~~~~~~~~~~~
+
+The initialization generates one each of ``NAME``, ``DEF``, ``DCLARRAY``, and
+``INIT`` annotations, and two ``DECL`` annotations.
+
+The ``DEF`` entry is currently not looked up as it is automatically converted to a ``#define``.
+
+The ``NAME`` annotation is used to declare the test case name, which is
+stored in the global variable ``rtems_test_name``. The current
+refinement entry is:
+
+.. code:: python
+
+ NAME: |
+ const char rtems_test_name[] = "Model_Chain_API";
+
+In this case, the name is fixed and ignores what is declared in the model.
+
+The ``DCLARRAY Node memory MAX_SIZE`` annotation looks up ``memory_DCL`` in the
+refinement file, passing in ``memory`` and ``MAX_SIZE`` as arguments. The entry in the refinement file is:
+
+.. code:: python
+
+ memory_DCL: item {0}[{1}];
+
+Here ``item`` is the type of the chains nodes used in the test code. It is
+declared in ``chains-api-model.pre.h`` as:
+
+.. code:: c
+
+ typedef struct item
+ {
+ rtems_chain_node node;
+ int val;
+ } item;
+
+Substituting the arguments gives:
+
+.. code:: c
+
+ item memory[MAX_SIZE];
+
+The two ``DECL`` annotations have two or three parameters. The first is the
+type, the second is the variable name, and the optional third is an initial
+value. The lookup key is the variable name with ``_DCL`` added on.
+In the refinement file, the entry only provides the C type, and the other parts of the declaration are added in.
+The entries are:
+
+.. code:: python
+
+ nptr_DCL: item *
+ chain_DCL: rtems_chain_control
+
+Annotation ``DECL unsigned nptr NULL`` results in:
+
+.. code:: c
+
+ item * nptr = NULL ;
+
+Annotation ``DECL Control chain`` results in:
+
+.. code:: c
+
+ rtems_chain_control chain ;
+
+The ``INIT`` annotation is looked up as ``INIT`` itself. It should be mapped to
+code that does all necessary initialization. The refinement entry for chains is:
+
+.. code:: python
+
+ INIT: rtems_chain_initialize_empty( &chain );
+
+In addition to all the above dealing with declarations and initialization,
+there are the annotations, already described above, that are used to display
+composite values, such as structure contents, and chain contents.
+
+In the model, all accesses to individual chain nodes are via index ``nptr``,
+which occurs in two types of annotations, ``PTR`` and ``STRUCT``. The ``PTR``
+annotation is refined by looking up ``nptr_PTR`` with the value of ``nptr`` as the sole argument. The refinement entry is:
+
+.. code:: python
+
+ nptr_PTR: |
+ T_eq_ptr( nptr, NULL );
+ T_eq_ptr( nptr, &memory[{0}] );
+
+The first line is used if the value of ``nptr`` is zero, otherwise the second
+line is used.
+
+The use of ``STRUCT`` requires three annotation lines in a row, *e.g.*:
+
+.. code:: c
+
+ @@@ 0 STRUCT nptr
+ @@@ 0 SCALAR itm 21
+ @@@ 0 END nptr
+
+The ``STRUCT`` and ``END`` annotations do not generate any code, but open and
+close a scope in which ``nptr`` is noted as the "name" of the struct. The
+``SCALAR`` annotation is used to observe simple values such as numbers or booleans. However, within a ``STRUCT`` it belongs to a C ``struct``, so the
+relevant field needs to be used to access the value.
+Within this scope, the scalar variable ``itm`` is looked up as a field name,
+by searching for ``itm_FSCALAR`` with arguments``nptr`` and ``21``, which returns the entry:
+
+.. code:: python
+
+ itm_FSCALAR: T_eq_int( {0}->val, {1} );
+
+This gets turned into the following test:
+
+.. code:: c
+
+ T_eq_int( nptr->val, 21 );
+
+A similar idea is used to test the contents of a chain. The annotations produced
+start with a ``SEQ`` annotation, followed by a ``SCALAR`` annotation for each
+item in the chain, and then ending with an ``END`` annotation. Again, there is
+a scope defined where the ``SEQ`` argument is the "name" of the sequence.
+The ``SCALAR`` entries have no name here (indicated by ``_``), and their values
+are accumulated in a string, separated by spaces. Test code generation is
+triggered this time by the ``END`` annotation, that looks up the "name" with ``_SEQ`` appended, and the accumulated string as an argument. The corresponding entry for chain sequences is:
+
+.. code:: python
+
+ chain_SEQ: |
+ show_chain( &chain, ctx->buffer );
+ T_eq_str( ctx->buffer, "{0} 0" );
+
+So, the following chain annotation sequence:
+
+.. code:: c
+
+ @@@ 0 SEQ chain
+ @@@ 0 SCALAR _ 21
+ @@@ 0 SCALAR _ 22
+ @@@ 0 END chain
+
+becomes the following C code:
+
+.. code:: C
+
+ show_chain( &chain, ctx->buffer );
+ T_eq_str( ctx->buffer, " 21 22 0" );
+
+C function ``show_chain()`` is defined in ``tr-chains-api-model.c`` and
+generates a string with exactly the same format as that produced above. These
+are then compared for equality.
+
+.. note::
+
+ The Promela/SPIN model checker's prime focus is modelling and verifying
+ concurrency related properties. It is not intended for verifying sequential
+ code or data transformations. This is why some of the ``STRUCT``/``SEQ``
+ material here is so clumsy. It plays virtually no role in the other models.
+
+Function Calls
+~~~~~~~~~~~~~~
+
+For ``@@@ 0 CALL append 22 3`` lookup ``append`` to get
+
+.. code-block:: c
+
+ memory[{1}].val = {0};
+ rtems_chain_append_unprotected( &chain, (rtems_chain_node*)&memory[{1}] );
+
+Substitute ``22`` and ``3`` in to produce
+
+.. code-block:: c
+
+ memory[3].val = 22;
+ rtems_chain_append_unprotected( &chain, (rtems_chain_node*)&memory[3] );
+
+For ``@@@ 0 CALL getNonNull 3`` lookup ``getNonNull`` to obtain
+
+.. code:: c
+
+ nptr = get_item( &chain );
+ T_eq_ptr( nptr, &memory[{0}] );
+
+Function ``get_item()`` is defined in ``tc-chains-api-model.c`` and calls ``rtems_chain_get_unprotected()``. Substitute ``3`` to produce:
+
+.. code:: c
+
+ nptr = get_item( &chain );
+ T_eq_ptr( nptr, &memory[3] );
+
+Testing Concurrent Managers
+---------------------------
+
+All the other models are of Managers that provide some form of communication
+between multiple RTEMS Tasks. This introduces a number of issues regarding
+the timing and control of tasks, particularly when developing *reproducible*
+tests, where the sequencing of behavior is the same every time the test runs.
+The tests are generated by following the schemes already in use for regular
+RTEMS handwritten tests.
+In particular the pre-existing tests for Send and Receive in the Event Manager
+where used as a guide.
+
+Testing Strategy
+^^^^^^^^^^^^^^^^
+
+The tests are organized as follows:
+
+1. A designated Task, the Runner, is responsible for initializing,
+ coordinating and tearing down a test run.
+ Coordination involves starting other Worker Tasks that perform tests,
+ and waiting for them to complete.
+ It may also run some tests itself.
+
+1. One or more Worker Tasks are used to perform test actions.
+
+1. Each RTEMS Task (Runner/Worker) is modelled by one Promela process.
+
+1. Simple Binary Semaphores
+ are used to coordinate all the tasks to ensure
+ that the interleaving is always the same
+ (See Semaphore Manager section in Classic API Manual).
+
+1. Two other Promela processes are required:
+ One, called ``Clock()`` is used to model timing and timeouts;
+ The other, called ``System()`` models relevant behavior of the RTEMS scheduler.
+
+Model Structure
+^^^^^^^^^^^^^^^
+
+All the models developed so far are based on this framework.
+The structure of these models takes the following form:
+
+ Constant Declarations
+ Mainly ``#define``\ s that define important constants.
+
+ Datastructure Definitions
+ Promela ``typedef``\ s that describe key forms of data.
+ In particular there is a type ``Task`` that models RTEMS Tasks.
+ The Simple Binary Semaphores are modelled as boolean variables.
+
+ Global Variable Declarations
+ Typically these are arrays of data-structures,
+ representing objects such as tasks or semaphores.
+
+ Supporting Models
+ These are ``inline`` definitions that capture common behavior.
+ In all models this includes ``Obtain()`` and ``Release()`` to model semaphores,
+ and ``waitUntilReady()`` that models a blocked task waiting to be unblocked.
+ Included here are other definitions specific to the particular Manager being
+ modelled.
+
+ API Models
+ These are ``inline`` definitions that model the behavior of each API call.
+ All behavior must be modelled, including bad calls that (should) result in
+ an error code being returned.
+ The parameter lists used in the Promela models will differ from those
+ of the actual API calls.
+ Consider a hypothetical RTEMS API call:
+
+ .. code:: c
+
+ rc = rtems_some_api(arg1,arg2,...,argN);
+
+ One reason, common to all calls, is that the ``inline`` construct has
+ no concept of returning a value,
+ so a variable parameter has to be added to represent it,
+ and it has to be ensured the appropriate return code is assigned to it.
+
+ .. code:: promela
+
+ inline some_api(arg1,arg2,...,argN,rc) {
+ ...
+ rc = RC_some_code
+ }
+
+ Another reason is that some RTEMS types encode a number of different
+ concepts in a single machine word.
+ The most notable of these is the ``rtems_options`` type,
+ that specifies various options, usually for calls that may block.
+ In some models, some options are modelled individually, for clarity.
+ So the API model may have two or more parameters where the RTEMS call has one.
+
+ .. code:: promela
+
+ inline some_api(arg1,arg2feat1,arg2feat2,...,argN,rc) {
+ ...
+ rc = RC_some_code
+ }
+
+ The refinement of this will pass the multiple feature arguments to
+ a C function that will assemble the single RTEMS argument.
+
+ A third reason is that sometimes it is important to also provide
+ the process id of the *calling* task. This can be important where
+ priority and preemption are involved.
+
+ Scenario Generation
+ A Testsuite that exercises *all* the API code is highly desirable.
+ This requires running tests that explore a wide range of scenarios,
+ normally devised by hand when writing a testsuite.
+ With Promela/SPIN, the model-checker can generate all of these simplify
+ as a result of its exhaustive search of the model.
+ In practice, scenarios fall into a number of high-level categories,
+ so the first step is make a random choice of such a category.
+ Within a category there may be further choices to be done.
+ A collection of global scenario variables are used to records the choices made.
+ This is all managed by inline ``chooseScenario()``.
+
+ RTEMS Test Task Modelling
+ This is a series of Promela ``proctype``\ s, one for the Runner Task,
+ and one for each of the Worker Tasks.
+ Their behavior is controlled by the global scenario variables.
+
+ System Modelling
+ These are Promela processes that model relevant underlying RTEMS behavior,
+ such as the scheduler (``System()``) and timers (``Clock()``).
+
+ Model Main Process
+ Called ``init``, this initialises variables, invokes ``chooseScenario()``,
+ runs all the processes, waits for them to terminate,
+ and then terminates itself.
+
+The Promela models developed so far for these Managers always terminate.
+The last few lines of each are of the form:
+
+.. code:: promela
+
+ #ifdef TEST_GEN
+ assert(false);
+ #endif
+
+If these models are run in the usual way (simulation or verification),
+then a correct verified model is observed.
+If ``-DTEST_GEN`` is provided as the first command-line argument,
+in verification mode configured to find *all* counterexamples,
+then all the possible (correct) behaviours of the system will be generated.
+
+Transforming Model Behavior to C Code
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+As described earlier, ``printf`` statements are used
+to produce easy to parse output that makes
+model events and outcomes easy to identify and process.
+The YAML file used to define the refinement from model to code
+provides a way of looking up an observation with arguments,
+and then obtaining a C template that can be populated with those arguments.
+
+This refinement is a bridge between two distinct worlds:
+
+ Model World:
+ where the key focus is on correctness and clarity.
+
+ Code World:
+ where clarity is often sacrificed for efficiency.
+
+This means that the model-to-code relationship
+need not be a simple one-to-one mapping.
+This has already been alluded to above when the need for extra parameters
+in API call models was discussed.
+It can also be helpful when the model is better treating various attributes
+separately, while the code handles those attributes packed into machine words.
+
+It is always reasonable to add test support code to the C test sources,
+and this can include C functions that map distinct attribute values
+down into some compact merged representation.
+
+
+Testing the Event Manager
+-------------------------
+
+Documentation: Event Manager section in the RTEMS Classic API Guide.
+
+Model Directory: ``formal/promela/models/events``.
+
+Model Name: ``event-mgr-model``.
+
+The Event Manager allows tasks to send events to,
+and receive events from, other tasks.
+From the perspective of the Event Manager,
+events are just uninterpreted numbers in the range 0..31,
+encoded as a 32-bit bitset.
+
+``rtems_event_send(id,event_in)``
+ allows a task to send a bitset to a designated task
+
+``rtems_event_receive(event_in,option_set,ticks,event_out)``
+ allows a task to specify a desired bitset
+ with options on what to do if it is not present.
+
+Most of the requirements are pretty straightforward,
+but two were a little more complex,
+and drove the more complex parts of the modelling.
+
+1. If a task was blocked waiting to receive events,
+ and a lower priority task then sent the events that would wake that
+ blocked task,
+ then the sending task would be immediately preempted by the receiver task.
+
+2. There was a requirement that explicitly discussed the situation
+ where the two tasks involved were running on different processors.
+
+A preliminary incomplete model of the Event Manager was originally developed
+by the consortium early in the project. The model was then completed during
+the rest of the activity by a Masters student: :cite:`Jennings:2021:FV`.
+They also developed the first iteration of the ``testbuilder`` program.
+
+API Model
+^^^^^^^^^
+
+File: ``event-mgr-model.pml``
+
+The RTEMS Event set contains 32 values, but in the model limits this to
+just four, which is enough for test purposes.
+Some inline definitions are provided to encode (``events``), display
+(``printevents``), and subtract (``setminus``) events.
+
+The ``rtems_option_set`` is simplifiedto just two relevant bits: the timeout
+setting (``Wait``, ``NoWait``), and how much of the desired event set will
+satisfy the receiver (``All``, ``Any``).
+These are passed in as two separate arguments to the model of the receive call.
+
+Event Send
+~~~~~~~~~~
+
+An RTEMS call ``rc = rtems_event_send(tid,evts)`` is modelled by an inline of
+the form:
+
+.. code-block:: c
+
+ event_send(self,tid,evts,rc)
+
+The four arguments are:
+ | ``self`` : id of process modelling the task/IDR making call.
+ | ``tid`` : id of process modelling the target task of the call.
+ | ``evts`` : event set being sent.
+ | ``rc`` : updated with the return code when the send completes.
+
+The main complication in the otherwise straightforward model is the requirement
+to preempt under certain circumstances.
+
+.. code-block:: c
+
+ inline event_send(self,tid,evts,rc) {
+ atomic{
+ if
+ :: tid >= BAD_ID -> rc = RC_InvId
+ :: tid < BAD_ID ->
+ tasks[tid].pending = tasks[tid].pending | evts
+ // at this point, have we woken the target task?
+ unsigned got : NO_OF_EVENTS;
+ bool sat;
+ satisfied(tasks[tid],got,sat);
+ if
+ :: sat ->
+ tasks[tid].state = Ready;
+ printf("@@@ %d STATE %d Ready\n",_pid,tid)
+ preemptIfRequired(self,tid) ;
+ // tasks[self].state may now be OtherWait !
+ waitUntilReady(self);
+ :: else -> skip
+ fi
+ rc = RC_OK;
+ fi
+ }
+ }
+
+Three inline abstractions are used:
+
+``satisfied(task,out,sat)``
+ updates ``out`` with the wanted events received so far, and then checks if a receive has been satisfied. It
+ updates its ``sat`` argument to reflect the check outcome.
+
+``preemptIfRequired(self,tid)``
+ forces the sending process to enter the ``OtherWait``,
+ if circumstances require it.
+
+``waitUntilReady(self)``
+ basically waits for the process state to become ``Ready``.
+
+Event Receive
+~~~~~~~~~~~~~
+
+An RTEMS call ``rc = rtems_event_receive(evts,opts,interval,out)`` is modelled
+by an inline of
+the form:
+
+.. code-block:: c
+
+ event_receive(self,evts,wait,wantall,interval,out,rc)
+
+The seven arguments are:
+ | ``self`` : id of process modelling the task making call
+ | ``evts`` : input event set
+ | ``wait`` : true if receive should wait
+ | ``what`` : all, or some?
+ | ``interval`` : wait interval (0 waits forever)
+ | ``out`` : pointer to location for satisfying events when the receive
+ completes.
+ | ``rc`` : updated with the return code when the receive completes.
+
+
+There is a small complication, in that there are distinct variables in the model
+for receiver options that are combined into a single RTEMS option set. The
+actual calling sequence in C test code will be:
+
+.. code-block:: c
+
+ opts = mergeopts(wait,wantall);
+ rc = rtems_event_receive(evts,opts,interval,out);
+
+Here ``mergeopts`` is a C function defined in the C Preamble.
+
+.. code-block:: c
+
+ inline event_receive(self,evts,wait,wantall,interval,out,rc){
+ atomic{
+ printf("@@@ %d LOG pending[%d] = ",_pid,self);
+ printevents(tasks[self].pending); nl();
+ tasks[self].wanted = evts;
+ tasks[self].all = wantall
+ if
+ :: out == 0 ->
+ printf("@@@ %d LOG Receive NULL out.\n",_pid);
+ rc = RC_InvAddr ;
+ :: evts == EVTS_PENDING ->
+ printf("@@@ %d LOG Receive Pending.\n",_pid);
+ recout[out] = tasks[self].pending;
+ rc = RC_OK
+ :: else ->
+ bool sat;
+ retry: satisfied(tasks[self],recout[out],sat);
+ if
+ :: sat ->
+ printf("@@@ %d LOG Receive Satisfied!\n",_pid);
+ setminus(tasks[self].pending,tasks[self].pending,recout[out]);
+ printf("@@@ %d LOG pending'[%d] = ",_pid,self);
+ printevents(tasks[self].pending); nl();
+ rc = RC_OK;
+ :: !sat && !wait ->
+ printf("@@@ %d LOG Receive Not Satisfied (no wait)\n",_pid);
+ rc = RC_Unsat;
+ :: !sat && wait && interval > 0 ->
+ printf("@@@ %d LOG Receive Not Satisfied (timeout %d)\n",_pid,interval);
+ tasks[self].ticks = interval;
+ tasks[self].tout = false;
+ tasks[self].state = TimeWait;
+ printf("@@@ %d STATE %d TimeWait %d\n",_pid,self,interval)
+ waitUntilReady(self);
+ if
+ :: tasks[self].tout -> rc = RC_Timeout
+ :: else -> goto retry
+ fi
+ :: else -> // !sat && wait && interval <= 0
+ printf("@@@ %d LOG Receive Not Satisfied (wait).\n",_pid);
+ tasks[self].state = EventWait;
+ printf("@@@ %d STATE %d EventWait\n",_pid,self)
+ if
+ :: sendTwice && !sentFirst -> Released(sendSema);
+ :: else
+ fi
+ waitUntilReady(self);
+ goto retry
+ fi
+ fi
+ printf("@@@ %d LOG pending'[%d] = ",_pid,self);
+ printevents(tasks[self].pending); nl();
+ }
+ }
+
+Here ``satisfied()`` and ``waitUntilReady()`` are also used.
+
+Behaviour Patterns
+^^^^^^^^^^^^^^^^^^
+
+File: ``event-mgr-model.pml``
+
+The Event Manager model consists of
+five Promela processes:
+
+``init``
+ The first top-level Promela process that performs initialisation,
+ starts the other processes, waits for them to terminate, and finishes.
+
+``System``
+ A Promela process that models the behaviour of the operating system,
+ in particular that of the scheduler.
+
+``Clock``
+ A Promela process used to facilitate modelling timeouts.
+
+``Receiver``
+ The Promela process modelling the test Runner,
+ that also invokes the receive API call.
+
+``Sender``
+ A Promela process modelling a singe test Worker
+ that invokes the send API call.
+
+
+Two simple binary semaphores are used to synchronise the tasks.
+
+The Task model only looks at an abstracted version of RTEMS Task states:
+
+``Zombie``
+ used to model a task that has just terminated. It can only be deleted.
+
+``Ready``
+ same as the RTEMS notion of ``Ready``.
+
+``EventWait``
+ is ``Blocked`` inside a call of ``event_receive()`` with no timeout.
+
+``TimeWait``
+ is ``Blocked`` inside a call of ``event_receive()`` with a timeout.
+
+``OtherWait``
+ is ``Blocked`` for some other reason, which arises in this model when a
+ sender gets pre-empted by a higher priority receiver it has just satisfied.
+
+
+Tasks are represented using a datastructure array.
+As array indices are proxies here for C pointers,
+the zeroth array entry is always unused,
+as index value 0 is used to model a NULL C pointer.
+
+.. code-block:: c
+
+ typedef Task {
+ byte nodeid; // So we can spot remote calls
+ byte pmlid; // Promela process id
+ mtype state ; // {Ready,EventWait,TickWait,OtherWait}
+ bool preemptable ;
+ byte prio ; // lower number is higher priority
+ int ticks; //
+ bool tout; // true if woken by a timeout
+ unsigned wanted : NO_OF_EVENTS ; // EvtSet, those expected by receiver
+ unsigned pending : NO_OF_EVENTS ; // EvtSet, those already received
+ bool all; // Do we want All?
+ };
+ Task tasks[TASK_MAX]; // tasks[0] models a NULL dereference
+
+.. code-block:: c
+
+ byte sendrc; // Sender global variable
+ byte recrc; // Receiver global variable
+ byte recout[TASK_MAX] ; // models receive 'out' location.
+
+Task Scheduling
+~~~~~~~~~~~~~~~
+
+In order to produce a model that captures real RTEMS Task behaviour,
+there need to be mechanisms that mimic the behaviour of the scheduler and other
+activities that can modify the execution state of these Tasks. Given a scenario
+generated by such a model, synchronisation needs to be added to the generated C
+code to ensure test has the same execution patterns.
+
+Relevant scheduling behavior is modelled by two inlines that have already
+been mentioned: ``waitUntilReady()`` and ``preemptIfRequired()``.
+
+For synchronisation, simple boolean semaphores are used, where True means
+available, and False means the semaphore has been acquired.
+
+.. code-block:: c
+
+ bool semaphore[SEMA_MAX]; // Semaphore
+
+The synchronisation mechanisms are:
+
+
+``Obtain(sem_id)``
+ call that waits to obtain semaphore ``sem_id``.
+
+``Release(sem_id)``
+ call that releases semaphore ``sem_id``
+
+``Released(sem_id)``
+ simulates ecosystem behaviour that releases ``sem_id``.
+
+The difference between ``Release`` and ``Released`` is that the first issues
+a ``SIGNAL`` annotation, while the second does not.
+
+
+Scenarios
+~~~~~~~~~
+
+A number of different scenario schemes were defined
+that cover various aspects of
+Event Manager behaviour. Some schemes involve only one task, and are usually
+used to test error-handling or abnormal situations. Other schemes involve two
+tasks, with some mixture of event sending and receiving, with varying task
+priorities.
+
+For example, an event send operation can involve a target identifier that
+is invalid (``BAD_ID``), correctly identifies a receiver task (``RCV_ID``), or
+is sending events to itself (``SEND_ID``).
+
+.. code-block:: c
+
+ typedef SendInputs {
+ byte target_id ;
+ unsigned send_evts : NO_OF_EVENTS ;
+ } ;
+ SendInputs send_in[MAX_STEPS];
+
+An event receive operation will be determined by values for desired events,
+and the relevant to bits of the option-set parameter.
+
+.. code-block:: c
+
+ typedef ReceiveInputs {
+ unsigned receive_evts : NO_OF_EVENTS ;
+ bool will_wait;
+ bool everything;
+ byte wait_length;
+ };
+ ReceiveInputs receive_in[MAX_STEPS];
+
+There is a range of global variables that define scenarios for both send and
+receive. This defines a two-step process for choosing a scenario.
+The first step is to select a scenario scheme. The possible schemes are
+defined by the following ``mtype``:
+
+.. code-block:: c
+
+ mtype = {Send,Receive,SndRcv,RcvSnd,SndRcvSnd,SndPre,MultiCore};
+ mtype scenario;
+
+One of these is chosen by using a conditional where all alternatives are
+executable, so behaving as a non-deterministic choice of one of them.
+
+.. code-block:: c
+
+ if
+ :: scenario = Send;
+ :: scenario = Receive;
+ :: scenario = SndRcv;
+ :: scenario = SndPre;
+ :: scenario = SndRcvSnd;
+ :: scenario = MultiCore;
+ fi
+
+
+Once the value of ``scenario`` is chosen, it is used in another conditional
+to select a non-deterministic choice of the finer details of that scenario.
+
+.. code-block:: c
+
+ if
+ :: scenario == Send ->
+ doReceive = false;
+ sendTarget = BAD_ID;
+ :: scenario == Receive ->
+ doSend = false
+ if
+ :: rcvWait = false
+ :: rcvWait = true; rcvInterval = 4
+ :: rcvOut = 0;
+ fi
+ printf( "@@@ %d LOG sub-senario wait:%d interval:%d, out:%d\n",
+ _pid, rcvWait, rcvInterval, rcvOut )
+ :: scenario == SndRcv ->
+ if
+ :: sendEvents = 14; // {1,1,1,0}
+ :: sendEvents = 11; // {1,0,1,1}
+ fi
+ printf( "@@@ %d LOG sub-senario send-receive events:%d\n",
+ _pid, sendEvents )
+ :: scenario == SndPre ->
+ sendPrio = 3;
+ sendPreempt = true;
+ startSema = rcvSema;
+ printf( "@@@ %d LOG sub-senario send-preemptable events:%d\n",
+ _pid, sendEvents )
+ :: scenario == SndRcvSnd ->
+ sendEvents1 = 2; // {0,0,1,0}
+ sendEvents2 = 8; // {1,0,0,0}
+ sendEvents = sendEvents1;
+ sendTwice = true;
+ printf( "@@@ %d LOG sub-senario send-receive-send events:%d\n",
+ _pid, sendEvents )
+ :: scenario == MultiCore ->
+ multicore = true;
+ sendCore = 1;
+ printf( "@@@ %d LOG sub-senario multicore send-receive events:%d\n",
+ _pid, sendEvents )
+ :: else // go with defaults
+ fi
+
+Ddefault values are defined for all the global scenario variables so that the
+above code focusses on what differs. The default scenario is a receiver waiting
+for a sender of the same priority which sends exactly what was requested.
+
+Sender Process (Worker Task)
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The sender process then uses the scenario configuration to determine its
+behaviour. A key feature is the way it acquires its semaphore before doing a
+send, and releases the receiver semaphore when it has just finished sending.
+Both these semaphores are initialised in the unavailable state.
+
+.. code-block:: c
+
+ proctype Sender (byte nid, taskid) {
+
+ tasks[taskid].nodeid = nid;
+ tasks[taskid].pmlid = _pid;
+ tasks[taskid].prio = sendPrio;
+ tasks[taskid].preemptable = sendPreempt;
+ tasks[taskid].state = Ready;
+ printf("@@@ %d TASK Worker\n",_pid);
+ if
+ :: multicore ->
+ // printf("@@@ %d CALL OtherScheduler %d\n", _pid, sendCore);
+ printf("@@@ %d CALL SetProcessor %d\n", _pid, sendCore);
+ :: else
+ fi
+ if
+ :: sendPrio > rcvPrio -> printf("@@@ %d CALL LowerPriority\n", _pid);
+ :: sendPrio == rcvPrio -> printf("@@@ %d CALL EqualPriority\n", _pid);
+ :: sendPrio < rcvPrio -> printf("@@@ %d CALL HigherPriority\n", _pid);
+ :: else
+ fi
+ repeat:
+ Obtain(sendSema);
+ if
+ :: doSend ->
+ if
+ :: !sentFirst -> printf("@@@ %d CALL StartLog\n",_pid);
+ :: else
+ fi
+ printf("@@@ %d CALL event_send %d %d %d sendrc\n",_pid,taskid,sendTarget,sendEvents);
+ if
+ :: sendPreempt && !sentFirst -> printf("@@@ %d CALL CheckPreemption\n",_pid);
+ :: !sendPreempt && !sentFirst -> printf("@@@ %d CALL CheckNoPreemption\n",_pid);
+ :: else
+ fi
+ event_send(taskid,sendTarget,sendEvents,sendrc);
+ printf("@@@ %d SCALAR sendrc %d\n",_pid,sendrc);
+ :: else
+ fi
+ Release(rcvSema);
+ if
+ :: sendTwice && !sentFirst ->
+ sentFirst = true;
+ sendEvents = sendEvents2;
+ goto repeat;
+ :: else
+ fi
+ printf("@@@ %d LOG Sender %d finished\n",_pid,taskid);
+ tasks[taskid].state = Zombie;
+ printf("@@@ %d STATE %d Zombie\n",_pid,taskid)
+ }
+
+Receiver Process (Runner Task)
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The receiver process uses the scenario configuration to determine its
+behaviour. It has the responsibility to trigger the start semaphore to allow
+either itself or the sender to start. The start semaphore corresponds to either
+the send or receive semaphore, depending on the scenario. The receiver acquires
+the receive semaphore before proceeding, and releases the send sempahore when
+done.
+
+.. code-block:: c
+
+ proctype Receiver (byte nid, taskid) {
+
+ tasks[taskid].nodeid = nid;
+ tasks[taskid].pmlid = _pid;
+ tasks[taskid].prio = rcvPrio;
+ tasks[taskid].preemptable = false;
+ tasks[taskid].state = Ready;
+ printf("@@@ %d TASK Runner\n",_pid,taskid);
+ if
+ :: multicore ->
+ printf("@@@ %d CALL SetProcessor %d\n", _pid, rcvCore);
+ :: else
+ fi
+ Release(startSema); // make sure stuff starts */
+ /* printf("@@@ %d LOG Receiver Task %d running on Node %d\n",_pid,taskid,nid); */
+ Obtain(rcvSema);
+
+ // If the receiver is higher priority then it will be running
+ // The sender is either blocked waiting for its semaphore
+ // or because it is lower priority.
+ // A high priority receiver needs to release the sender now, before it
+ // gets blocked on its own event receive.
+ if
+ :: rcvPrio < sendPrio -> Release(sendSema); // Release send semaphore for preemption
+ :: else
+ fi
+ if
+ :: doReceive ->
+ printf("@@@ %d SCALAR pending %d %d\n",_pid,taskid,tasks[taskid].pending);
+ if
+ :: sendTwice && !sentFirst -> Release(sendSema)
+ :: else
+ fi
+ printf("@@@ %d CALL event_receive %d %d %d %d %d recrc\n",
+ _pid,rcvEvents,rcvWait,rcvAll,rcvInterval,rcvOut);
+ /* (self, evts, when, what, ticks, out, rc) */
+ event_receive(taskid,rcvEvents,rcvWait,rcvAll,rcvInterval,rcvOut,recrc);
+ printf("@@@ %d SCALAR recrc %d\n",_pid,recrc);
+ if
+ :: rcvOut > 0 ->
+ printf("@@@ %d SCALAR recout %d %d\n",_pid,rcvOut,recout[rcvOut]);
+ :: else
+ fi
+ printf("@@@ %d SCALAR pending %d %d\n",_pid,taskid,tasks[taskid].pending);
+ :: else
+ fi
+ Release(sendSema);
+ printf("@@@ %d LOG Receiver %d finished\n",_pid,taskid);
+ tasks[taskid].state = Zombie;
+ printf("@@@ %d STATE %d Zombie\n",_pid,taskid)
+ }
+
+System Process
+~~~~~~~~~~~~~~
+
+ A process is needed that periodically wakes up blocked processes.
+ This is modelling background behaviour of the system,
+ such as ISRs and scheduling.
+ All tasks are visited in round-robin order (to prevent starvation)
+ and are made ready if waiting on other things. Tasks waiting for events or timeouts are not touched. This terminates when all tasks are zombies.
+
+.. code-block:: c
+
+ proctype System () {
+ byte taskid ;
+ bool liveSeen;
+ printf("@@@ %d LOG System running...\n",_pid);
+ loop:
+ taskid = 1;
+ liveSeen = false;
+ printf("@@@ %d LOG Loop through tasks...\n",_pid);
+ atomic {
+ printf("@@@ %d LOG Scenario is ",_pid);
+ printm(scenario); nl();
+ }
+ do // while taskid < TASK_MAX ....
+ :: taskid == TASK_MAX -> break;
+ :: else ->
+ atomic {
+ printf("@@@ %d LOG Task %d state is ",_pid,taskid);
+ printm(tasks[taskid].state); nl()
+ }
+ if
+ :: tasks[taskid].state == Zombie -> taskid++
+ :: else ->
+ if
+ :: tasks[taskid].state == OtherWait
+ -> tasks[taskid].state = Ready
+ printf("@@@ %d STATE %d Ready\n",_pid,taskid)
+ :: else -> skip
+ fi
+ liveSeen = true;
+ taskid++
+ fi
+ od
+ printf("@@@ %d LOG ...all visited, live:%d\n",_pid,liveSeen);
+ if
+ :: liveSeen -> goto loop
+ :: else
+ fi
+ printf("@@@ %d LOG All are Zombies, game over.\n",_pid);
+ stopclock = true;
+ }
+
+Clock Process
+~~~~~~~~~~~~~
+
+A process is needed that handles a clock tick,
+by decrementing the tick count for tasks waiting on a timeout.
+Such a task whose ticks become zero is then made ``Ready``,
+and its timer status is flagged as a timeout. This terminates when all
+tasks are zombies (as signalled by ``System()`` via ``stopclock``).
+
+.. code-block:: c
+
+ proctype Clock () {
+ int tid, tix;
+ printf("@@@ %d LOG Clock Started\n",_pid)
+ do
+ :: stopclock -> goto stopped
+ :: !stopclock ->
+ printf(" (tick) \n");
+ tid = 1;
+ do
+ :: tid == TASK_MAX -> break
+ :: else ->
+ atomic{
+ printf("Clock: tid=%d, state=",tid);
+ printm(tasks[tid].state); nl()
+ };
+ if
+ :: tasks[tid].state == TimeWait ->
+ tix = tasks[tid].ticks - 1;
+ if
+ :: tix == 0
+ tasks[tid].tout = true
+ tasks[tid].state = Ready
+ printf("@@@ %d STATE %d Ready\n",_pid,tid)
+ :: else
+ tasks[tid].ticks = tix
+ fi
+ :: else // state != TimeWait
+ fi
+ tid = tid + 1
+ od
+ od
+ stopped:
+ printf("@@@ %d LOG Clock Stopped\n",_pid);
+ }
+
+
+init Process
+~~~~~~~~~~~~
+
+The initial process outputs annotations for defines and declarations,
+generates a scenario non-deterministically and then starts the system, clock
+and send and receive processes running. It then waits for those to complete,
+and them, if test generation is underway, asserts ``false`` to trigger a
+seach for counterexamples:
+
+.. code-block:: c
+
+ init {
+ pid nr;
+ printf("@@@ %d NAME Event_Manager_TestGen\n",_pid)
+ outputDefines();
+ outputDeclarations();
+ printf("@@@ %d INIT\n",_pid);
+ chooseScenario();
+ run System();
+ run Clock();
+ run Sender(THIS_NODE,SEND_ID);
+ run Receiver(THIS_NODE,RCV_ID);
+ _nr_pr == 1;
+ #ifdef TEST_GEN
+ assert(false);
+ #endif
+ }
+
+The information regarding when tasks should wait and/or restart
+can be obtained by tracking the process identifiers,
+and noting when they change.
+The ``spin2test`` program does this,
+and also produces separate test code segments for each Promela process.
+
+Annotations
+^^^^^^^^^^^
+
+File: ``event-mgr-model.pml``
+
+Nothing more to say here.
+
+Refinement
+^^^^^^^^^^
+
+File: ``event-mgr-model-rfn.yml``
+
+
+The test-code generated here is based on the test-code generated from the
+specification items used to describe the Event Manager in the main (non-formal)
+part of the new qualification material.
+
+The relevant specification item is ``spec/rtems/event/req/send-receive.yml``
+found in ``rtems-central``. The corresponding C test code is
+``tr-event-send-receive.c`` found in ``rtems`` at ``testsuites/validation``.
+That automatically generated C code is a single file that uses a set of deeply
+nested loops to iterate through the scenarios it generates.
+
+The approach here is to generate a stand-alone C code file for each scenario
+(``tr-event-mgr-model-N.c`` for ``N`` in range 0..8.)
+
+
+The ``TASK`` annotations issued by the ``Sender`` and ``Receiver`` processes
+lookup the following refinement entries, to get code that tests that the C
+code Task does correspond to what is being defined in the model.
+
+.. code-block:: yaml
+
+ Runner: |
+ checkTaskIs( ctx->runner_id );
+
+ Worker: |
+ checkTaskIs( ctx->worker_id );
+
+The ``WAIT`` and ``SIGNAL`` annotations produced by ``Obtain()`` and
+``Release()`` respectively, are mapped to the corresponding operations on
+RTEMS semaphores in the test code.
+
+.. code-block:: yaml
+
+ code content
+ SIGNAL: |
+ Wakeup( semaphore[{}] );
+
+ WAIT: |
+ Wait( semaphore[{}] );
+
+Some of the ``CALL`` annotations are used to do more complex test setup
+involving priorities, or other processors and schedulers. For example:
+
+.. code-block:: yaml
+
+ HigherPriority: |
+ SetSelfPriority( PRIO_HIGH );
+ rtems_task_priority prio;
+ rtems_status_code sc;
+ sc = rtems_task_set_priority( RTEMS_SELF, RTEMS_CURRENT_PRIORITY, &prio );
+ T_rsc_success( sc );
+ T_eq_u32( prio, PRIO_HIGH );
+
+ SetProcessor: |
+ T_ge_u32( rtems_scheduler_get_processor_maximum(), 2 );
+ uint32_t processor = {};
+ cpu_set_t cpuset;
+ CPU_ZERO(&cpuset);
+ CPU_SET(processor, &cpuset);
+
+Some handle more complicated test outcomes, such as observing context-switches:
+
+.. code-block:: yaml
+
+ CheckPreemption: |
+ log = &ctx->thread_switch_log;
+ T_eq_sz( log->header.recorded, 2 );
+ T_eq_u32( log->events[ 0 ].heir, ctx->runner_id );
+ T_eq_u32( log->events[ 1 ].heir, ctx->worker_id );
+
+Most of the other refinement entries are similar to those described above for
+the Chains API.
+
+Testing the Barrier Mananger
+----------------------------
+
+Documentation: Barrier Manager section in the RTEMS Classic API Guide.
+
+Model Directory: ``formal/promela/models/barriers``.
+
+Model Name: ``barrier-mgr-model``.
+
+The Barrier Manager is used to arrange for a number of tasks to wait on a
+designated barrier object, until either another task releases them, or a
+given number of tasks are waiting, at which point they are all released.
+
+All five directives were modelled:
+
+* ``rtems_barrier_create()``
+
+* ``rtems_barrier_ident()``
+
+* ``rtems_barrier_delete()``
+
+* ``rtems_barrier_wait()``
+
+* ``rtems_barrier_release()``
+
+Barriers can be manual (released only by a call to ``..release()``),
+or automatic (released by the call to ``..wait()`` that results in a wait count limit being reached.)
+There is no notion of queuing in this manager,
+only waiting for a barrier to be released.
+
+This model was developed by a Masters student :cite:`Jaskuc:2022:TESTGEN`,
+using the Event Manager as a model. It was added into the QDP produced by
+the follow-on IV&V activity.
+
+API Model
+^^^^^^^^^
+
+File: ``barrier-mgr-model.pml``
+
+Modelling waiting is much easier than modelling queueing.
+All that is required is an array of booleans (``waiters``), indexed by process id:
+
+.. code:: promela
+
+ typedef Barrier {
+ byte b_name; // barrier name
+ bool isAutomatic; // true for automatic, false for manual barrier
+ int maxWaiters; // maximum count of waiters for automatic barrier
+ int waiterCount; // current amount of tasks waiting on the barrier
+ bool waiters[TASK_MAX]; // waiters on the barrier
+ bool isInitialised; // indicated whenever this barrier was created
+ }
+
+The name ``satisfied`` is currently used here for an inline that checks when
+a barrier can be released.
+Other helper inlines include ``waitAtBarrier()`` and ``barrierRelease()``.
+
+Behaviour Patterns
+^^^^^^^^^^^^^^^^^^
+
+File: ``barrier-mgr-model.pml``
+
+The overall architecture in terms of Promela processes has processes ``init``, ``System``, ``Clock``, ``Runner``,
+and two workers: ``Worker1`` and ``Worker2``.
+The runner and workers each may perform one or more API calls,
+in the following order: create, ident, wait, release, delete.
+Scenarios mix and match which task does what.
+
+There are three top-level scenarios:
+
+.. code:: promela
+
+ mtype = {ManAcqRel,AutoAcq,AutoToutDel};
+
+In scenario ``ManAcqRel``, the runner will do create, release and delete,
+with sub-scenarios to check error cases as well as good behaviour,
+for manual barriers.
+Good behaviour involves one or more workers doing a wait.
+The ``AutoAcq`` and ``AutoToutDel``
+scenarios look at good and bad uses of automatic barriers.
+
+Annotations
+^^^^^^^^^^^
+
+File: ``barrier-mgr-model.pml``
+
+Similiar to those used in the Event Manager.
+
+Refinement
+^^^^^^^^^^
+
+File: ``barrier-mgr-model-rfn.yml``
+
+Similiar to those used in the Event Manager.
+
+Testing the Message Manager
+---------------------------
+
+Documentation: Message Manager section in the RTEMS Classic API Guide.
+
+Model Directory: ``formal/promela/models/messages``.
+
+Model Name: ``msg-mgr-model``.
+
+The Message Manager provides objects that act as message queues. Tasks can
+interact with these by enqueuing and/or dequeuing message objects.
+
+There are 11 directives in total, but only the following were modelled:
+
+ * ``rtems_message_queue_create()``
+
+ * ``rtems_message_queue_send()``
+
+ * ``rtems_message_queue_receive()``
+
+The manager supports two queuing protocols, FIFO and priority-based.
+Only the FIFO queueing was modelled.
+
+This model was developed by a Masters student :cite:`Lynch:2022:TESTGEN`,
+using the Event Manager as a model. It was added into the QDP produced by
+the follow-on IV&V activity.
+
+Below we focus on aspects of this model that differ from the Event Manager.
+
+API Model
+^^^^^^^^^
+
+File: ``msg-mgr-model.pml``
+
+A key feature of this manager is that not only are messages in a queue,
+but so are the tasks waiting for those messages.
+Both task and message queues are modelled as circular buffers,
+with inline definitions of enqueuing and dequeuing operations.
+
+While the Message Manager allows many queues to be created,
+the model only uses one.
+
+
+Behaviour Patterns
+^^^^^^^^^^^^^^^^^^
+
+File: ``msg-mgr-model.pml``
+
+The overall architecture in terms of Promela processes has processes ``init``, ``System``, ``Clock``, ``Sender``, and two receivers:
+``Receiver1`` and ``Receiver2``.
+The ``Sender`` is the test runner, which performs the queue creation,
+releases the start semaphore and then performs a send operation if needed.
+The receivers are worker processes.
+
+There are four top level scenarios:
+
+.. code:: promela
+
+ mtype = {Send,Receive,SndRcv, RcvSnd};
+
+Scenarios ``Send`` and ``Receive`` are used for testing erroneous calls.
+The ``SndRcv`` scenario fills up queues before the receivers run,
+while the ``RcvSnd`` has the receivers waiting before messages are sent.
+
+Annotations
+^^^^^^^^^^^
+
+File: ``msg-mgr-model.pml``
+
+Similiar to those used in the Event Manager.
+
+Refinement
+^^^^^^^^^^
+
+File: ``msg-mgr-model-rfn.yml``
+
+Similiar to those used in the Event Manager.
+
+Current State of Play
+---------------------
+
+The models developed here are the result of
+an ad-hoc incremental development process
+and have a lot of overlapping material.
+
+Model State
+^^^^^^^^^^^
+
+The models were developed by first focusing on simple behavior
+such as error handling, and then adding in simpler behaviors,
+until sufficient coverage was acheived.
+The basic philosophy at the time was not to fix anything not broken.
+
+This has led to the models being somewhat over-engineered,
+particularly when it comes to scenario generation.
+There is some conditional looping behaviour,
+implemented using labels and ``goto``,
+that should really be linearised, using conditionals to skip parts.
+It is harder than it should be to understand what each scenario does.
+
+Also the API call models have perhaps a bit too much code devoted
+to system behaviour.
+
+Model Refactoring
+^^^^^^^^^^^^^^^^^
+
+There is a case to be made to perform some model refactoring.
+Some of this would address the model state issues above.
+Other refactoring would extract the common model material out,
+to be put into files that could be included.
+This includes the binary semaphore models,
+and the parts modelling preemption and waiting while blocked.
+
+
+Test Code Refactoring
+^^^^^^^^^^^^^^^^^^^^^
+
+During the qualification activity,
+a new file ``tx-support.c`` was added to the RTEMS validation testsuite codebase.
+This gathers C test support functions used by most of the tests.
+The contents of the ``tr-<modelname>.h`` and ``tr-<modelname>.c``
+files in particular should be brought in line with ``tx-support.c``.
+
+Suitable Promela models should also be produced
+of relevant functions in ``tx-support.c``.
+
+
+
diff --git a/eng/fv/approaches.rst b/eng/fv/approaches.rst
new file mode 100644
index 0000000..6bbac20
--- /dev/null
+++ b/eng/fv/approaches.rst
@@ -0,0 +1,178 @@
+.. SPDX-License-Identifier: CC-BY-SA-4.0
+
+.. Copyright (C) 2022 Trinity College Dublin
+
+.. _FormalVerifApproaches:
+
+Formal Verification Approaches
+==============================
+
+This is an overview of a range of formal methods and tools
+that look feasible for use with RTEMS.
+
+A key criterion for any proposed tool is the ability to deploy it in a highly
+automated manner. This amounts to the tool having a command-line interface that
+covers all the required features.
+One such feature is that the tool generates output that can be
+easily transformed into the formats useful for qualification.
+Tools with GUI interfaces can be very helpful while developing
+and deploying formal models, as long as the models/tests/proofs
+can be re-run automatically via the command-line.
+
+Other important criteria concerns the support available
+for test generation support,
+and how close the connection is between the formalism and actual C code.
+
+The final key criteria is whatever techniques are proposed should fit in
+with the RTEMS Project Mission Statement,
+in the Software Engineering manual.
+This requires, among other things,
+that any tool added to the tool-chain needs to be open-source.
+
+A more detailed report regarding this can be found in
+:cite:`Butterfield:2021:FV1-200`.
+
+
+Next is a general overview of formal methods and testing,
+and discusses a number of formalisms and tools against the criteria above.
+
+Formal Methods Overview
+-----------------------
+
+Formal specification languages can be divided into the following groups:
+
+ Model-based: e.g., Z, VDM, B
+
+ These have a language that describes a system in terms of having an abstract
+ state and how it is modified by operations. Reasoning is typically based
+ around the notions of pre- and post-conditions and state invariants.
+ The usual method of reasoning is by using theorem-proving. The resulting
+ models often have an unbounded number of possible states, and are capable
+ of describing unbounded numbers of operation steps.
+
+ Finite State-based: e.g., finite-state machines (FSMs), SDL, Statecharts
+
+ These are a variant of model-based specification, with the added constraint
+ that the number of states are bounded. Desired model properties are often
+ expressed using some form of temporal logic. The languages used to describe
+ these are often more constrained than in more general model-based
+ approaches. The finiteness allows reasoning by searching the model,
+ including doing exhaustive searches, a.k.a. model-checking.
+
+ Process Algebras: e.g., CSP, CCS, pi-calculus, LOTOS
+
+ These model systems in terms of the sequence of externally observable
+ events that they perform. There is no explicit definition of the abstract
+ states, but their underlying semantics is given as a state machine,
+ where the states are deduced from the overall behavior of the system,
+ and events denote transitions between these states. In general both the
+ number of such states and length of observed event sequences are unbounded.
+ While temporal logics can be used to express properties, many process
+ algebras use their own notation to express desired properties by simpler
+ systems. A technique called bisimulation is used to reason about the
+ relationships between these.
+
+ Most of the methods above start with formal specifications/models. Also
+ needed is a way to bridge the gap to actual code. The relationship between
+ specification and code is often referred to as a :term:`refinement`
+ (some prefer the term :term:`reification`). Most model-based methods have refinement,
+ with the concept baked in as a key part of the methodology.
+
+ Theorem Provers: e.g., CoQ, HOL4, PVS, Isabelle/HOL
+
+ Many modern theorem provers are not only useful to help reason about the
+ formalisms mentioned above, but are often powerful enough to be used to
+ describe formal models in their own terms and then apply their proof
+ systems directly to those.
+
+ Model Checkers: e.g., SPIN, FDR
+
+ Model checkers are tools that do exhaustive searches over models with a
+ finite number of states. These are most commonly used with the finite-state
+ methods, as well as the process algebras where some bound is put on the
+ state-space. As model-checking is basically exhaustive testing, these are
+ often the easiest way to get test generation from formal techniques.
+
+ Formal Development frameworks: e.g. TLA+, Frama-C, KeY
+
+ There are also a number of frameworks that support a close connection
+ between a programming language, a formalism to specify desired behavior
+ for programs in that language, as well as tools to support the reasoning
+ (proof, simulation, test).
+
+Formal Methods actively considered
+----------------------------------
+
+Given the emphasis on verifying RTEMS C code,
+the focus is on freely available tools that could easily connect to C.
+These include: Frama-C, TLA+/PlusCal, Isabelle/HOL, and Promela/SPIN.
+Further investigation ruled out TLA+/PlusCal because it is Java-based,
+and requires installing a Java Runtime Environment.
+Frama-C, Isabelle/HOL, and Promela/SPIN are discussed below in more detail,
+
+Frama-C
+^^^^^^^
+
+Frama-C (frama-c.com) is a platform supporting a range of tools for analysing C
+code, including static analysers, support for functional specifications (ANSI-C
+Specification Language – ACSL), and links to theorem provers. Some of its
+analyses require code annotations, while others can extract useful information
+from un-annotated code. It has a plug-in architecture, which makes it easy to
+extend. It is used extensively by Airbus.
+
+Frama-C, and its plugins, are implemented in OCaml,
+and it is installed using the ``opam`` package manager.
+An issue here was that Frama-C has many quite large dependencies.
+There was support for test generation, but it was not freely available.
+Another issue was that Frama-C only supported C99, and not C11
+(the issue is how to handle C11 Atomics in terms of their semantics).
+
+Isabelle/HOL
+^^^^^^^^^^^^
+
+Isabelle/HOL is a wide-spectrum theorem-prover, implemented as an embedding of
+Higher-Order Logic (HOL) into the Isabelle generic proof assistant
+(isabelle.in.tum.de). It has a high degree of automation, including an ability
+to link to third-party verification tools, and a very large library of verified
+mathematical theorems, covering number and set theory, algebra, analysis. It is
+based on the idea of a small trusted code kernel that defines an encapsulated
+datatype representing a theorem, which can only be constructed using methods in
+the kernel for that datatype, but which also scales effectively regardless of
+how many theorems are so proven.
+It is implemented using `polyml`, with the IDE implemented using Scala,
+is open-source, and is easy to install.
+However, like Frama-C, it is also a very large software suite.
+
+Formal Method actually used
+---------------------------
+
+A good survey of formal techniques and testing
+is found in a 2009 ACM survey paper :cite:`Hierons:2009:FMT`.
+Here they clearly state:
+
+ "The most important role for formal verification in testing
+ is in the automated generation of test cases.
+ In this context,
+ model checking is the formal verification technology of choice;
+ this is due to the ability of model checkers
+ to produce counterexamples
+ in case a temporal property does not hold for a system model."
+
+Promela/SPIN
+^^^^^^^^^^^^
+
+The current use of formal methods in RTEMS is based on using the Promela
+language to model key RTEMS features,
+in such a way that tests can be generated using the SPIN model checker
+(spinroot.com).
+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
+interest.
+
+Given a Promela model that checks key properties successfully,
+tests can be generated for a property *P* by asking
+SPIN to check the negation of that property.
+There are ways to get SPIN to generate multiple/all possible counterexamples,
+as well as getting it to find the shortest.
diff --git a/eng/fv/index.rst b/eng/fv/index.rst
new file mode 100755
index 0000000..abeaa27
--- /dev/null
+++ b/eng/fv/index.rst
@@ -0,0 +1,16 @@
+.. SPDX-License-Identifier: CC-BY-SA-4.0
+
+.. Copyright (C) 2022 Trinity College Dublin
+
+.. _FormalVerif:
+
+Formal Verification
+*******************
+
+.. toctree::
+
+ overview
+ approaches
+ methodology
+ promela-index
+
diff --git a/eng/fv/methodology.rst b/eng/fv/methodology.rst
new file mode 100755
index 0000000..71430cd
--- /dev/null
+++ b/eng/fv/methodology.rst
@@ -0,0 +1,62 @@
+.. SPDX-License-Identifier: CC-BY-SA-4.0
+
+.. Copyright (C) 2022 Trinity College Dublin
+
+.. _FormalVerifMethodology:
+
+Test Generation Methodology
+===========================
+
+The general approach to using any model-checking technology for test generation
+has three major steps:
+
+Model desired behavior
+----------------------
+
+Construct a model that describes the desired properties (`P1`, ..., `PN`)
+and use the model-checker to verify those properties.
+
+Promela can specify properties using the ``assert()`` statement, to be
+true at the point where it gets executed,
+and can use :term:`Linear Temporal Logic`
+(LTL) to specify more complex properties over execution sequences. SPIN will
+also check generic correctness properties such as deadlock and
+livelock freedom.
+
+Make claims about undesired behavior
+------------------------------------
+
+Given a fully verified model, systematically negate each specified property.
+Given that each property was verified as true,
+then these negated properties will fail model-checking,
+and counter-examples will be
+generated. These counter-examples will in fact be scenarios describing correct
+behavior of the system, demonstrating the truth of each property.
+
+.. warning::
+
+ It is very important that the negations only apply to stated properties,
+ and do not alter the possible behaviors of the model in any way.
+ The behaviours of the model are determined by the control-flow constructs,
+ so any boolean-valued expression statements used in these,
+ or used in sequential code to wait for some some condition,
+ should not be altered.
+ What can be altered are the expressions in ``assert()`` statements,
+ and any LTL properties.
+
+With Promela, there are a number of different ways to do systematic
+negation. The precise approach adopted depends on the nature of the models, and
+more details can be found
+in the RTEMS Formal Models Guide Appendix in this document.
+
+Map good behavior scenarios to tests
+------------------------------------
+
+Define a mapping from counter-example output to test code,
+and use this in the process of constructing a test program.
+
+A YAML file is used to define a mapping from SPIN output to
+relevant fragments of RTEMS C test code, using the Test Framework section
+in this document.
+The process is automated by a python script called ``testbuilder``.
+
diff --git a/eng/fv/overview.rst b/eng/fv/overview.rst
new file mode 100755
index 0000000..15ce7d8
--- /dev/null
+++ b/eng/fv/overview.rst
@@ -0,0 +1,38 @@
+.. SPDX-License-Identifier: CC-BY-SA-4.0
+
+.. Copyright (C) 2022 Trinity College Dublin
+
+.. _FormalVerifOverview:
+
+Formal Verification Overview
+============================
+
+Formal Verification is a technique based on writing key design artifacts using
+notations that have a well-defined mathematical :term:`semantics`. This means
+that these descriptions can be rigorously analyzed using logic and other
+mathematical tools. The term :term:`formal model` is used to refer to any such
+description.
+
+Having a formal model of a software engineering artifact (requirements,
+specification, code) allows it to be analyzed to assess the behavior it
+describes. This means checks can be done that the model has desired properties,
+and that it lacks undesired ones. A key feature of having a formal description
+is that tools can be developed that parse the notation and perform much,
+if not most, of the analysis. An industrial-strength formalism is one that has
+very good tool support.
+
+Having two formal models of the same software object at different levels
+of abstraction (specification and code, say) allows their comparison. In
+particular, a formal analysis can establish if a lower level artifact like
+code satisfies the properties described by a higher level,
+such as a specification. This relationship is commonly referred to as a
+:term:`refinement`.
+
+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.
+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/fv/promela-index.rst b/eng/fv/promela-index.rst
new file mode 100644
index 0000000..6b32841
--- /dev/null
+++ b/eng/fv/promela-index.rst
@@ -0,0 +1,9 @@
+.. SPDX-License-Identifier: CC-BY-SA-4.0
+
+.. Copyright (C) 2022 Trinity College Dublin
+
+.. toctree::
+
+ tool-setup
+ promela
+ refinement
diff --git a/eng/fv/promela.rst b/eng/fv/promela.rst
new file mode 100755
index 0000000..6ebb3eb
--- /dev/null
+++ b/eng/fv/promela.rst
@@ -0,0 +1,323 @@
+.. SPDX-License-Identifier: CC-BY-SA-4.0
+
+.. Copyright (C) 2022 Trinity College Dublin
+
+.. _PromelaModelling:
+
+Modelling with Promela
+======================
+
+Promela is a large language with many features,
+but only a subset is used here for test generation.
+This is a short overview of that subset.
+The definitive documentation can be found at
+https://spinroot.com/spin/Man/promela.html.
+
+Promela Execution
+-----------------
+
+Promela is a *modelling* language, not a programming language. It is designed
+to describe the kind of runtime behaviors that make reasoning about low-level
+concurrency so difficult: namely shared mutable state and effectively
+non-deterministic interleaving of concurrent threads. This means that there are
+control constructs that specify non-deterministic outcomes,
+and an execution model that allows the specification of when threads should
+block.
+
+The execution model is based on the following concepts:
+
+Interleaving Concurrency
+ A running Promela system consists of one or more concurrent processes. Each
+ process is described by a segment of code that defines a sequence of
+ atomic steps. The scheduler looks at all the available next-steps and makes
+ a **non-deterministic choice** of which one will run. The scheduler is
+ invoked after every atomic step.
+
+Executability
+ At any point in time, a Promela process is either able to perform a step,
+ and is considered executable, or is unable to do so, and is considered
+ blocked. Whether a statement is executable or blocked may depend on the
+ global state of the model. The scheduler will only select from among the
+ executable processes.
+
+The Promela language is based loosely on C, and the SPIN model-checking tool
+converts a Promela model into a C program that has the specific model
+hard-coded and optimized for whatever analysis has been invoked. It also
+supports the use of the C pre-processor.
+
+Simulation vs. Verification
+^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+SPIN can run a model in several distinct modes:
+
+Simulation
+ SPIN simply makes random choices for the scheduler to produce a possible
+ execution sequence (a.k.a. scenario) allowed by the model. A readable
+ transcript is written to ``stdout`` as the simulation runs.
+
+ The simplest SPIN invocation does simulation by default:
+
+ .. code:: shell
+
+ spin model.pml
+
+Verification
+ SPIN does an analysis of the whole model by exploring all the possible
+ choices that the scheduler can make. This will continue until either all
+ possible choices have been covered, or some form of error is uncovered.
+ If verification ends successfully, then this is simply reported as ok.
+ If an error occurs, verification stops, and the sequence of steps that led
+ to that failure are output to a so-called trail file.
+
+ The simplest way to run a verification is to give the ``-run`` option:
+
+ .. code:: shell
+
+ spin -run model.pml
+
+Replaying
+ A trail file is an uninformative list of number-triples, but can be replayed
+ in simulation mode to produce human-readable output.
+
+ .. code:: shell
+
+ spin -t model.pml
+
+Promela Datatypes
+-----------------
+
+Promela supports a subset of C scalar types (``short``, ``int``), but also
+adds some of its own (``bit``, ``bool``, ``byte``, ``unsigned``).
+It has support for one-dimensional arrays,
+and its own variation of the C struct concept
+(confusingly called a ``typedef``!).
+It has a single enumeration type called ``mtype``.
+There are no pointers in Promela, which means that modelling pointer
+usage requires the use of arrays with their indices acting as proxies for
+pointers.
+
+Promela Declarations
+--------------------
+
+Variables and one-dimensional arrays can be declared in Promela in much the
+same way as they are done in C:
+
+.. code-block:: C
+
+ int x, y[3] ;
+
+All global variables and arrays are initialized to zero.
+
+The identifier ``unsigned`` is the name of a type, rather than a modifier.
+It is used to declare an unsigned number variable with a given bit-width:
+
+.. code-block:: C
+
+ unsigned mask : 4 ;
+
+
+Structure-like datatypes in Promela are defined using the ``typedef`` keyword
+that associates a name with what is basically a C ``struct``:
+
+.. code-block:: C
+
+ typedef CBuffer {
+ short count;
+ byte buffer[8]
+ }
+
+ CBuffers cbuf[6];
+
+Note that we can have arrays of ``typedef``\ s that themselves contain arrays.
+This is the only way to get multi-dimensional arrays in Promela.
+
+There is only one enumeration type, which can be defined incrementally.
+Consider the following sequence of four declarations that defines the values in
+``mtype`` and declares two variables of that type:
+
+.. code-block:: C
+
+ mtype = { up, down } ;
+ mtype dir1;
+ mtype = { left, right} ;
+ mtype dir2;
+
+This gives the same outcome with the following two declarations:
+
+.. code-block:: C
+
+ mtype = { left, right, up, down } ;
+ mtype dir1, dir2;
+
+Special Identifiers
+^^^^^^^^^^^^^^^^^^^
+
+The are a number of variable identifiers that have a special meaning in Promela.
+These all start with an underscore. We use the following:
+
+Process Id
+ ``_pid`` holds the process id of the currently active process
+
+Process Count
+ ``_nr_pr`` gives the number of currently active processes.
+
+Promela Atomic Statements
+-------------------------
+
+Assignment
+ ``x = e`` where ``x`` is a variable and ``e`` is an expression.
+
+ Expression ``e`` must have no side-effects. An assignment is always
+ executable. Its effect is to update the value of ``x`` with the current
+ value of ``e``.
+
+Condition Statement
+ ``e`` where ``e`` is an expression
+
+ Expression ``e``, used standalone as a statement, is executable if its
+ value in the current state is non-zero. If its current value is zero,
+ then it is blocked. It behaves like a NO-OP when executed.
+
+Skip
+ ``skip``, a keyword
+
+ ``skip`` is always executable, and behaves like a NO-OP when executed.
+
+Assertion
+ ``assert(e)`` where ``e`` is an expression
+
+ An assertion is always executable. When executed, it evaluates its
+ expression. If the value is non-zero, then it behaves like a NO-OP. If the
+ value is zero, then it generates an assertion error and aborts further
+ simulation/verification of the model.
+
+Printing
+ ``printf(string,args)`` where ``string`` is a format-string and ``args``
+ are values and expressions.
+
+ A ``printf`` statement is completely ignored in verification mode.
+ In simulation mode, it is always executable,
+ and generates output to ``stdout`` in much the same way as in C.
+ This is is used in a structured way to assist with test generation.
+
+Goto
+ ``goto lbl`` where ``lbl`` is a statement label.
+
+ Promela supports labels for statements, in the same manner as C.
+ The ``goto`` statement is always executable.
+ When executed, flow of control goes to the statement labelled by ``lbl:``.
+
+Break
+ ``break``, a keyword
+
+ Can only occur within a loop (``do ... od``, see below). It is always
+ executable, and when executed performs a ``goto`` to the statement just
+ after the end of the innermost enclosing loop.
+
+Promela Composite Statements
+----------------------------
+
+Sequencing
+ ``{ <stmt> ; <stmt> ; ... ; <stmt> }`` where each ``<stmt>`` can be any
+ kind of statement, atomic or composite. The sub-statements execute in
+ sequence in the usual way.
+
+Selection
+ .. code-block:: none
+
+ if
+ :: <stmt>
+ :: <stmt>
+ ...
+ :: <stmt>
+ fi
+
+ A selection construct is blocked if all the ``<stmt>`` are blocked. It is
+ executable if at least one ``<stmt>`` is executable. The scheduler will make
+ a non-deterministic choice from all of those ``<stmt>`` that are executable.
+ The construct terminates when/if the chosen ``<stmt>`` does.
+
+ Typically, a selection statement will be a sequence of the form
+ ``g ; s1 ; ... ; sN`` where ``g`` is an expression acting as a guard,
+ and the rest of the statements are intended to run if ``g`` is non-zero.
+ The symbol ``->`` plays the same syntactic role as ``;``, so this allows
+ for a more intuitive look and feel; ``g -> s1 ; ... ; sN``.
+
+ If the last ``<stmt>`` has the form ``else -> ...``, then the ``else`` is
+ executable only when all the other selection statements are blocked.
+
+Repetition
+ .. code-block:: none
+
+ do
+ :: <stmt>
+ :: <stmt>
+ ...
+ :: <stmt>
+ od
+
+ The executability rules here are the same as for Selection above. The key
+ difference is that when/if a chosen ``<stmt>`` terminates, then the whole
+ construct is re-executed, making it basically an infinite loop. The only
+ way to exit this loop is for an active ``<stmt>`` to execute a ``break``
+ or ``goto`` statement.
+
+ A ``break`` statement only makes sense inside a Repetition, is always
+ executable, and its effect is to jump to the next statement after the
+ next ``od`` keyword in text order.
+
+
+The selection and repetition syntax and semantics are based on Edsger
+Djikstra's Guarded Command Language :cite:`Djikstra:1975:GCL` .
+
+
+Atomic Composite
+ ``atomic{stmt}`` where ``stmt`` is usually a (sequential) composite.
+
+ Wrapping the ``atomic`` keyword around a statement makes its entire
+ execution proceed without any interference from the scheduler. Once it is
+ executable, if the scheduler chooses it to run, then it runs to completion.
+
+ There is one very important exception: if it should block internally because
+ some sub-statement is blocked, then the atomicity gets broken, and the
+ scheduler is free to find some other executable process to run. When/if the
+ sub-statement eventually becomes executable, once it gets chosen to run by
+ the scheduler then it continues to run atomically.
+
+Processes
+ ``proctype name (args) { sequence }`` where ``args`` is a list of zero
+ or more typed parameter declarations,
+ and ``sequence`` is a list of local declarations and statements.
+
+ This defines a process type called ``name`` which takes parameters defined
+ by ``args`` and has the behavior defined by ``sequence``. When invoked, it
+ runs as a distinct concurrent process. Processes can be invoked explicitly
+ by an existing process using the ``run`` statement,
+ or can be setup to start automatically.
+
+Run
+ ``run name (exprs)`` where ``exprs`` is a list of expressions that match
+ the arguments defined the ``proctype`` declaration for ``name``.
+
+ This is executable as long as the maximum process limit has not been reached,
+ and immediately starts the process running.
+ It is an atomic statement.
+
+Inlining
+ ``inline name (names) { sequence }`` where ``names`` is a list of zero or
+ more identifiers, and ``sequence`` is a list of declarations and statements.
+
+ Inlining does textual substitution, and does not represent some kind of
+ function call. An invocation ``name(texts)`` gets replaced by
+ ``{ sequence }`` where each occurrence of an identifier in ``names`` is
+ replaced by the corresponding text in ``texts``. Such an invocation can
+ only appear in a context where a Promela statement can appear.
+
+Promela Top-Level
+-----------------
+
+At the top-level, a Promela model is a list of declarations, much like a C
+program. The Promela equivalent of ``main`` is a process called ``init`` that
+has no arguments. There must be at least one Promela process setup to be running
+at the start. This can be ``init``, or one or more ``proctype``\ s declared as
+``active``.
diff --git a/eng/fv/refinement.rst b/eng/fv/refinement.rst
new file mode 100755
index 0000000..4cbad19
--- /dev/null
+++ b/eng/fv/refinement.rst
@@ -0,0 +1,559 @@
+.. SPDX-License-Identifier: CC-BY-SA-4.0
+
+.. Copyright (C) 2022 Trinity College Dublin
+
+.. _Promela2CRefinement:
+
+Promela to C Refinement
+=======================
+
+Promela models are more abstract than concrete C code.
+A rigorous link, known as a :term:`refinement`, needs to be established
+from Promela to C.
+This is composed of two parts:
+manual annotations in the Promela model to make its behavior easy
+to identify and parse;
+and a refinement defined as a YAML file that maps from
+annotations to corresponding C code.
+A single refinement YAML file is associated with each Promela model.
+
+Model Annotations
+-----------------
+
+Promela ``printf`` statements are used in the models to output information that
+is used by ``spin2test`` to generate test code. This information is used to
+lookup keys in a YAML file that defines the mapping to C code. It uses a simple
+format that makes it easy to parse and process, and is also designed to be
+easily understood by a human reader. This is important because any V&V process
+will require this information to be carefully assessed.
+
+Annotation Syntax
+^^^^^^^^^^^^^^^^^
+
+Format, where :math:`N \geq 0`:
+
+ ``@@@ <pid> <KEYWORD> <parameter1> ... <parameterN>``
+
+The leading ``@@@`` is a marker that makes it easy to filter out this
+information from other SPIN output.
+
+Parameters take the following forms:
+
+ ``<pid>`` Promela Process Id of ``proctype`` generating annotation
+
+ ``<word>`` chunk of text containing no white space
+
+ ``<name>`` Promela variable/structure/constant identifier
+
+ ``<type>`` Promela type identifier
+
+ ``<tid>`` OS Task/Thread/Process Id
+
+ ``_`` unused argument (within containers)
+
+Each ``<KEYWORD>`` is associated with specific forms of parameters:
+
+.. code-block:: none
+
+ LOG <word1> ... <wordN>
+ NAME <name>
+ INIT
+ DEF <name> <value>
+ DECL <type> <name> [<value>]
+ DCLARRAY <type> <name> <value>
+ TASK <name>
+ SIGNAL <name> <value>
+ WAIT <name> <value>
+ STATE tid <name>
+ SCALAR (<name>|_) [<index>] <value>
+ PTR <name> <value>
+ STRUCT <name>
+ SEQ <name>
+ END <name>
+ CALL <name> <value1> ... <valueN>
+
+
+Annotation Lookup
+-----------------
+
+The way that code is generated depends on the keyword in the annotation.
+In particular, the keyword determines how, or if,
+the YAML refinement file is looked up.
+
+ Direct Output - no lookup
+ (``LOG``, ``DEF``)
+
+ Keyword Refinement - lookup the ``<KEYWORD>``
+ (``NAME``, ``INIT``, ``SIGNAL``, ``WAIT``)
+
+ Name Refinement - lookup first parameter (considered as text)
+ (``TASK``, ``DECL``, ``DCLARRAY``, ``PTR``, ``CALL``, ``SCALAR``)
+
+The same name may appear in different contexts,
+and the name can be extended with a suffix of the form
+``_XXX`` to lookup less frequent uses:
+
+ ``_DCL`` - A variable declaration
+
+ ``_PTR`` - The pointer value itself
+
+ ``_FSCALAR`` - A scalar that is a struct field
+
+ ``_FPTR`` - A pointer that is a struct field
+
+Generally, the keyword, or name is used to lookup ``mymodel-rfn.yml`` to get a
+string result. This string typically has substitution placeholders, as used by
+the Python ``format()`` method for strings. The other parameters in the
+annotation are then textually substituted in, to produce a segment of test code.
+
+
+Specifying Refinement
+---------------------
+
+Using the terminology of the :ref:`RTEMSTestFramework`
+each Promela model is converted into a set of Test Cases,
+one for each complete scenario produced by test generation.
+There are a number of template files, tailored for each model,
+that are used to assemble the test code sources,
+along with code segments for each Promela process,
+based on the annotations output for any given scenario.
+
+
+The refinement mapping from annotations to code is defined in a YAML file that
+describes a Python dictionary that maps a name to some C code, with placeholders
+that are used to allow for substituting in actual test values.
+
+The YAML file has entries of the following form:
+
+.. code:: yaml
+
+ entity: |
+ C code line1{0}
+ ...
+ C code lineM{2}
+
+The entity is a reference to an annotation concept, which can refer to key
+declarations, values, variables, types, API calls or model events. There can be
+zero or more arguments in the annotations, and any occurrence of braces
+enclosing a number in the C code means that the corresponding annotation
+argument string is substituted in (using the python string object `format()`
+method).
+
+The general pattern is working through all the annotations in order. The
+code obtained by looking up the YAML file is collated into different
+code-segments, one for each Promela process id (``<pid>``).
+
+In addition to the explicit annotations generated by the Promela models, there
+are two implicit annotations produced by the python refinement code. These
+occur when the ``<pid>`` part of a given explicit annotation is different to the
+one belonging to the immediately preceding annotation. This indicates a point in
+a test generation scenario where one task is suspended and another resumes. This
+generates internal annotations with keywords ``SUSPEND`` and ``WAKEUP`` which
+should have entries in the refinement file to provide code to ensure that the
+corresponding RTEMS tasks in the test behave accordingly.
+
+The annotations can also be output as comments into the generated test-code, so
+it is easy to check that parameters are correct, and the generated code is
+correct.
+
+If a lookup fails, a C comment line is output stating the lookup failed.
+The translation continues in any case.
+
+Lookup Example
+^^^^^^^^^^^^^^
+
+Consider the following annotation, from the Events Manager model:
+
+ ``@@@ 1 CALL event_send 1 2 10 sendrc``
+
+This uses Name refinement so a lookup with ``event_send`` as the key
+and gets back the following text:
+
+.. code-block:: python3
+
+ T_log( T_NORMAL, "Calling Send(%d,%d)", mapid( ctx, {1}), {2} );
+ {3} = ( *ctx->send )( mapid( ctx, {1} ), {2} );
+ T_log( T_NORMAL, "Returned 0x%x from Send", {3} );
+
+Arguments ``1``, ``2``, ``10``, and ``sendrc``
+are then substituted to get the code:
+
+.. code-block:: c
+
+ T_log( T_NORMAL, "Calling Send(%d,%d)", mapid( ctx, 2), 10 );
+ sendrc = ( *ctx->send )( mapid( ctx, 2 ), 10 );
+ T_log( T_NORMAL, "Returned 0x%x from Send", sendrc );
+
+Given a Promela process id of ``1``, this code is put into a code segment
+for the corresponding RTEMS task.
+
+
+Annotation Refinement Guide
+---------------------------
+
+This guide describes how each annotation is processed
+by the test generation software.
+
+LOG
+^^^
+
+``LOG <word1> ... <wordN>`` (Direct Output)
+ Generate a call to ``T_log()`` with a message formed from the ``<word..>``
+ parameters.
+ This message will appear in the test output for certain verbosity settings.
+
+NAME
+^^^^
+
+``NAME <name>`` (Keyword Refinement)
+ Looks up ``NAME`` (currently ignoring ``<name>``) and returns the resulting
+ text as is as part of the code. This code should define the name of the
+ testcase, if needed.
+
+INIT
+^^^^
+
+``INIT`` (Keyword Refinement)
+ Lookup ``INIT`` and expect to obtain test initialisation code.
+
+TASK
+^^^^
+
+``TASK <name>`` (Name Refinement)
+ Lookup ``<name>`` and return corresponding C code.
+
+SIGNAL
+^^^^^^
+
+``SIGNAL <value>`` (Keyword Refinement)
+ Lookup `SIGNAL` and return code with `<value>` substituted in.
+
+WAIT
+^^^^
+
+``WAIT <value>`` (Keyword Refinement)
+ Lookup `WAIT` and return code with `<value>` substituted in.
+
+DEF
+^^^
+
+``DEF <name> <value>`` (Direct Output)
+ Output ``#define <name> <value>``.
+
+DECL
+^^^^
+
+``DECL <type> <name> [<value>]`` (Name Refinement)
+ Lookup ``<name>_DCL`` and substitute ``<name>`` in. If ``<value>`` is
+ present, append ``=<value>``. Add a final semicolon. If the `<pid>` value
+ is zero, prepend ``static``.
+
+DCLARRAY
+^^^^^^^^
+
+``DCLARRAY <type> <name> <value>`` (Name Refinement)
+ Lookup ``<name>_DCL`` and substitute ``<name>`` and ``<value>`` in. If the
+ `<pid>` value is zero, prepend ``static``.
+
+CALL
+^^^^
+
+``CALL <name> <value0> .. <valueN>`` (Name refinement, ``N`` < 6)
+ Lookup ``<name>`` and substitute all ``<value..>`` in.
+
+STATE
+^^^^^
+
+``STATE <tid> <name>`` (Name Refinement)
+ Lookup ``<name>`` and substitute in ``<tid>``.
+
+STRUCT
+^^^^^^
+
+``STRUCT <name>``
+ Declares the output of the contents of variable ``<name>``
+ that is itself a structure. The ``<name>`` is noted, as is the fact
+ that a structured value is being processes.
+ Should not occur if already be processing a structure or a sequence.
+
+SEQ
+^^^
+
+``SEQ <name>``
+ Declares the output of the contents of array variable ``<name>``.
+ The ``<name>`` is noted, as is the fact that an array is being processed.
+ Values are accumulated in a string now initialsed to empty.
+ Should not occur if already processing a structure or a sequence.
+
+PTR
+^^^
+
+``PTR <name> <value>`` (Name Refinement)
+ If not inside a ``STRUCT``, lookup ``<name>_PTR``. Two lines of code should
+ be returned. If the ``<value>`` is zero, use the first line, otherwise use
+ the second with ``<value>`` substituted in. This is required to handle NULL
+ pointers.
+
+ If inside a ``STRUCT``, lookup ``<name>_FPTR``. Two lines of code should
+ be returned. If the ``<value>`` is zero, use the first line, otherwise use
+ the second with ``<value>`` substituted in. This is required to handle NULL
+ pointers.
+
+SCALAR
+^^^^^^
+
+There are quite a few variations here.
+
+``SCALAR _ <value>``
+ Should only be used inside a ``SEQ``. A space and ``<value>`` is appended
+ to the string being accumulated by this ``SEQ``.
+
+``SCALAR <name> <value>`` (Name Refinement)
+ If not inside a ``STRUCT``, lookup ``<name>``, and substitute ``<value>``
+ into the resulting code.
+
+ If inside a ``STRUCT``, lookup ``<name>_FSCALAR`` and substitute the saved
+ ``STRUCT`` name and ``<value>`` into the resulting code.
+
+ This should not be used inside a ``SEQ``.
+
+``SCALAR <name> <index> <value>`` (Name Refinement)
+ If not inside a ``STRUCT``, lookup ``<name>``, and substitute ``<index>``
+ and ``<value>`` into the resulting code.
+
+ If inside a ``STRUCT``, lookup ``<name>_FSCALAR`` and substitute the saved
+ ``STRUCT`` name and ``<value>`` into the resulting code.
+
+ This should not be used inside a ``SEQ``.
+
+END
+^^^
+
+``END <name>``
+ If inside a ``STRUCT``, terminates processing a
+ structured variable.
+
+ If inside a ``SEQ``, lookup ``<name>_SEQ``. For each line of code obtained,
+ substitute in the saved sequence string.
+ Terminates processing a sequence/array variable.
+
+ This should not be encountered outside of a ``STRUCT`` or ``SEQ``.
+
+SUSPEND and WAKEUP
+^^^^^^^^^^^^^^^^^^
+
+A change of Promela process id from ``oldid`` to ``newid`` has been found.
+Increment a counter that tracks the number of such changes.
+
+``SUSPEND`` (Keyword Refinement)
+
+ Lookup ``SUSPEND`` and substitute in the counter value, ``oldid`` and
+ ``newid``.
+
+``WAKEUP`` (Keyword Refinement)
+
+ Lookup ``WAKEUP`` and substitute in the counter value, ``newid`` and
+ ``oldid``.
+
+Annotation Ordering
+-------------------
+
+While most annotations occur in an order determined by any given test scenario,
+there are some annotations that need to be issued first. These are, in order:
+``NAME``, ``DEF``, ``DECL`` and ``DCLARRAY``, and finally, ``INIT``.
+
+
+Test Code Assembly
+------------------
+
+The code snippets produced by refining annotations are not enough.
+We also need boilerplate code to setup, coordinate and teardown the tests,
+as well as providing useful C support functions.
+
+For a model called `mymodel` the following files are required:
+
+* ``mymodel.pml`` - the Promela model
+* ``mymodel-rfn.yml`` - the model refinement to C test code
+* ``tc-mymodel.c`` - the testcase setup C file
+* ``tr-mymodel.h`` - the test-runner header file
+* ``tr-mymodel.c`` - the test-runner setup C file
+
+The following files are templates used to assemble
+a single test-runner C file
+for each scenario generated by the Promela model:
+
+* ``mymodel-pre.h`` - preamble material at the start
+* ``mymodel-run.h`` - test runner material
+* ``mymodel-post.h`` - postamble material at the end.
+
+The process is entirely automated:
+
+.. code-block:: shell
+
+ tbuild all mymodel
+
+The steps of the process are as follows:
+
+Scenario Generation
+^^^^^^^^^^^^^^^^^^^
+
+When SPIN is invoked to find all scenarios,
+it will produce a number (N) of counterexample files
+with a ``.trail`` extension.
+These files hold numeric data that refer to SPIN internals.
+
+.. code-block:: none
+
+ mymodel.pml1.trail
+ ...
+ mymodel.pmlN.trail
+
+SPIN is then used to take each trail file and produce a human-readable
+text file, using the same format as the SPIN simulation output.
+SPIN numbers files from 1 up,
+whereas the RTEMS convention is to number things,
+including filenames, from zero.
+SPIN is used to produce readable output in text files with a ``.spn`` extension,
+with 1 subtracted from the trail file number.
+This results in the following files:
+
+.. code-block:: shell
+
+ mymodel-0.spn
+ ...
+ mymodel-{N-1}.spn
+
+Test Code Generation
+^^^^^^^^^^^^^^^^^^^^
+
+Each SPIN output file ``mymodel-I.spn``
+is converted to a C test runner file ``tr-mymodel-I.c``
+by concatenating the following components:
+
+``mymodel-pre.h``
+ This is a fairly standard first part of an RTEMS test C file.
+ It is used unchanged.
+
+refined test segments
+ The annotations in ``mymodel-I.spn`` are converted, in order,
+ into test code snippets using the refinement file ``mymodel-rfn.yml``.
+ Snippets are gathered into distinct code segments based on the Promela
+ process number reported in each annotation.
+ Each code segment is used to construct a C function called
+ ``TestSegmentP()``, where ``P`` is the relevant process number.
+
+``mymodel-post.h``
+ This is static code that declares the top-level RTEMS Tasks
+ used in the test.
+ These are where the code segments above get invoked.
+
+``mymodel-run.h``
+ This defines top-level C functions that implement a given test runner. The top-level function has a name like ``RtemsMyModel_Run``
+ This is not valid C as it needs to produce a name parameterized by
+ the relevant scenario number. It contains Python string format substitution
+ placeholders that allow the relevant number to be added to end of the
+ function name. So the above run function actually appears in this file as ``RtemsMyModel_Run{0}``, so ``I`` will be substituted in for ``{0}`` to result in the name ``RtemsMyModel_RunI``.
+ In particular, it invokes ``TestSegment0()`` which contains code
+ generated from Promela process 0, which is the main model function.
+ This declares test variables, and initializes them.
+
+These will generate test-runner test files as follows:
+
+.. code-block:: none
+
+ tr-mymodel-0.c
+ ...
+ tr-mymodel-{N-1}.c
+
+In addition, the test case file ``tc-mymodel.c`` needs to have entries added
+manually of the form below, for ``I`` in the range 0 to N-1.:
+
+.. code-block:: c
+
+ T_TEST_CASE( RtemsMyModelI )
+ {
+ RtemsMyModel_RunI(
+ ...
+ );
+ }
+
+These define the individual test cases in the model, each corresponding to precisely one SPIN scenario.
+
+Test Code Deployment
+^^^^^^^^^^^^^^^^^^^^
+
+All files starting with ``tc-`` or ``tr-`` are copied to the
+relevant testsuite directory.
+At present, this is ``testsuites/validation`` at the top level in
+the ``rtems`` repository.
+All the names of the above files with a ``.c`` extension are added
+into a YAML file that
+defines the Promela generated-test sources.
+At present, this
+is ``spec/build/testsuites/validation/model-0.yml``
+at the top-level in the ``rtems`` repository.
+They appear in the YAML file under the ``source`` key:
+
+.. code-block:: yaml
+
+ source:
+ - testsuites/validation/tc-mymodel.c
+ - testsuites/validation/tr-mymodel-0.c
+ ...
+ - testsuites/validation/tr-mymodel-{N-1}.c
+ - testsuites/validation/ts-model-0.c
+
+Performing Tests
+^^^^^^^^^^^^^^^^
+
+At this point build RTEMS as normal. e.g., with ``waf``,
+and the tests will get built.
+The executable will be found in the designated build directory,
+*(e.g.):*
+
+ ``rtems/build/sparc/gr740/testsuites/validation/ts-model-0.exe``
+
+ This can be run using the RTEMS Tester
+ (RTEMS User Manual, Host Tools, RTEMS Tester and Run).
+
+
+ Both building the code and running on the tester is also automated
+ (see :ref:`FormalToolSetup`).
+
+Traceability
+------------
+
+Traceability between requirements, specifications, designs, code, and tests,
+is a key part of any qualification/certification effort. The test generation
+methodology developed here supports this in two ways, when refining an
+annotation:
+
+1. If the annotation is for a declaration of some sort, the annotation itself
+ is added as a comment to the output code, just before the refined declaration.
+
+ .. code-block:: c
+
+ // @@@ 0 NAME Chain_AutoGen
+ // @@@ 0 DEF MAX_SIZE 8
+ #define MAX_SIZE 8
+ // @@@ 0 DCLARRAY Node memory MAX_SIZE
+ static item memory[MAX_SIZE];
+ // @@@ 0 DECL unsigned nptr NULL
+ static item * nptr = NULL;
+ // @@@ 0 DECL Control chain
+ static rtems_chain_control chain;
+
+2. If the annotation is for a test of some sort, a call to ``T_log()`` is
+ generated with the annotation as its text, just before the test code.
+
+ .. code-block:: c
+
+ T_log(T_NORMAL,"@@@ 0 INIT");
+ rtems_chain_initialize_empty( &chain );
+ T_log(T_NORMAL,"@@@ 0 SEQ chain");
+ T_log(T_NORMAL,"@@@ 0 END chain");
+ show_chain( &chain, ctx->buffer );
+ T_eq_str( ctx->buffer, " 0" );
+
+In addition to traceability, these also help when debugging models, refinement
+files, and the resulting test code.
diff --git a/eng/fv/tool-setup.rst b/eng/fv/tool-setup.rst
new file mode 100755
index 0000000..f8cf046
--- /dev/null
+++ b/eng/fv/tool-setup.rst
@@ -0,0 +1,317 @@
+.. SPDX-License-Identifier: CC-BY-SA-4.0
+
+.. Copyright (C) 2022 Trinity College Dublin
+
+.. _FormalToolSetup:
+
+Formal Tools Setup
+==================
+
+The required formal tools consist of
+the model checking software (Promela/SPIN),
+and the test generation software (spin2test/testbuilder).
+
+Installing Tools
+----------------
+
+Installing Promela/SPIN
+^^^^^^^^^^^^^^^^^^^^^^^
+
+Follow the installation instructions for Promela/Spin
+at https://spinroot.com/spin/Man/README.html.
+
+There are references there to the Spin Distribution which is now on
+Github (https://github.com/nimble-code/Spin).
+
+Installing Test Generation Tools
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+The test generation tools are found in ``formal/promela/src``, written in
+Python3, and installed using a virtual environment.
+To build the tools, enter ``formal/promela/src`` and issue the
+commands:
+
+.. code:: shell
+
+ make env
+ . env/bin/activate
+ make py
+
+The test generation tools need to be used from within this Python virtual
+environment. Use the ``deactivate`` command to exit from it.
+
+Test generation is managed at the top level by the script ``testbuilder.py``
+located in the top-level of ``formal/promela/src``.
+To avoid using (long) absolute pathnames,
+it helps to define an suitable alias
+*(e.g.)*:
+
+.. code-block:: shell
+
+ alias tbuild='python3 /..../formal/promela/src/testbuilder.py'
+
+This alias is used subsequently in this documentation.
+
+To check for a successful tool build, invoke the command without any
+arguments, which should result in an extended help message being displayed:
+
+.. code-block:: shell
+
+ (env) prompt % tbuild
+ USAGE:
+ help - more details about usage and commands below
+ all modelname - runs clean, spin, gentests, copy, compile and run
+ clean modelname - remove spin, test files
+ archive modelname - archives spin, test files
+ zero - remove all tesfiles from RTEMS
+ spin modelname - generate spin files
+ gentests modelname - generate test files
+ copy modelname - copy test files and configuration to RTEMS
+ compile - compiles RTEMS tests
+ run - runs RTEMS tests
+
+The tool is not yet ready for use, as it needs to be configured.
+
+Tool Configuration
+------------------
+
+Tool configuration involves setting up a new testsuite in RTEMS, and providing
+information to ``tbuild`` that tells it where to find key locations, and some
+command-line arguments for some of the tools.
+A template file ``testbuilder-template.yml`` is included,
+and contains the following entries:
+
+.. code-block:: python
+
+ # This should be specialised for your setup, as testbuilder.yml,
+ # located in the same directory as testbuilder.py
+ # All pathnames should be absolute
+
+ spin2test: <spin2test_directory>/spin2test.py
+ rtems: <path-to-main-rtems-directory> # rtems.git, or ..../modules/rtems/
+ rsb: <rsb-build_directory>/rtems/6/bin/
+ simulator: <path-to>/sparc-rtems6-sis
+ testyamldir: <rtems>/spec/build/testsuites/validation/ # directory containing <modelname>.yml
+ testcode: <rtems>/testsuites/validation/
+ testexedir: <rtems>/build/.../testsuites/validation/ # directory containing ts-<modelname>.exe
+ testsuite: model-0
+ simulatorargs: -leon3 -r s -m 2 # run command executes "<simulator> <simargs> <testexedir>/ts-<testsuite>.exe"
+ spinallscenarios: -DTEST_GEN -run -E -c0 -e # trail generation "spin <spinallscenarios> <model>.pml"
+
+This template should be copied/renamed to ``testbuilder.yml``
+and each entry updated as follows:
+
+* spin2test:
+ This should be the absolute path to ``spin2test.py``
+ in the Promela sources directory.
+
+ ``/.../formal/promela/src/spin2test.py``
+
+* rtems:
+ This should be the absolute path to your RTEMS source directory,
+ with the terminating ``/``.
+ From ``rtems-central`` this would be:
+
+ ``/.../rtems-central/modules/rtems/``
+
+ For a separate ``rtems`` installation
+ it would be where ``rtems.git`` was cloned.
+
+ We refer to this path below as ``<rtems>``.
+
+* rsb:
+ This should be the absolute path
+ to your RTEMS source-builder binaries directory,
+ with the terminating ``/``.
+ From ``rtems-central`` this would be (assuming RTEMS 6):
+
+ ``/.../rtems-central/modules/rsb/6/bin/``
+
+* simulator:
+ This should be the absolute path to the RTEMS Tester
+ (See Host Tools in the RTEMS User Manual)
+
+ It defaults at present to the ``sis`` simulator
+
+ ``/.../rtems-central/modules/rsb/6/bin/sparc-rtems6-sis``
+
+* testsuite:
+ This is the name for the testsuite :
+
+ Default value: ``model-0``
+
+* testyamldir:
+ This should be the absolute path to where validation tests are *specified*:
+
+ ``<rtems>/spec/build/testsuites/validation/``
+
+* testcode:
+ This should be the absolute path to where validation test sources
+ are found:
+
+ ``<rtems>/testsuites/validation/``
+
+* testexedir:
+ This should be the absolute path to where
+ the model-based validation test executable
+ will be found:
+
+ ``<rtems>/build/.../testsuites/validation/``
+
+ This will contain ``ts-<testsuite>.exe`` (e.g. ``ts-model-0.exe``)
+
+* simulatorargs:
+ These are the command line arguments for the RTEMS Tester.
+ It defaults at present to those for the ``sis`` simulator.
+
+ ``-<bsp> -r s -m <cpus>``
+
+ The first argument should be the BSP used when building RTEMS sources.
+ BSPs ``leon3``, ``gr712rc`` and ``gr740`` have been used.
+ The argument to the ``-m`` flag is the number of cores.
+ Possible values are: 1, 2 and 4 (BSP dependent)
+
+ Default: ``-leon3 -r s -m 2``
+
+* spinallscenarios:
+ These are command line arguments for SPIN,
+ that ensure that all counter-examples are generated.
+
+ Default: ``-DTEST_GEN -run -E -c0 -e`` (recommended)
+
+Testsuite Setup
+^^^^^^^^^^^^^^^
+
+The C test code generated by these tools is installed into the main ``rtems``
+repository at ``testsuites/validation`` in the exact same way as other RTEMS
+test code.
+This means that whenever ``waf`` is used at the top level to build and/or run
+tests, that the formally generated code is automatically included.
+This requires adding and modifying some *Specification Items*
+(See Software Requirements Engineering section in this document).
+
+To create a testsuite called ``model-0`` (say), do the following, in the
+``spec/build/testsuites/validation`` directory:
+
+* Edit ``grp.yml`` and add the following two lines into the `links` entry:
+
+ .. code-block:: YAML
+
+ - role: build-dependency
+ uid: model-0
+
+* Copy ``validation-0.yml`` (say) to ``model-0.yml``, and change the following
+ entries as shown:
+
+ .. code-block:: YAML
+
+ enabled-by: RTEMS_SMP
+ source:
+ - testsuites/validation/ts-model-0.c
+ target: testsuites/validation/ts-model-0.exe
+
+Then, go to the ``testsuites/validation`` directory, and copy
+``ts-validation-0.c`` to ``ts-model-0.c``, and edit as follows:
+
+ * Change all occurrences of ``Validation0`` in comments to ``Model0``.
+
+ * Change ``rtems_test_name`` to ``Model0``.
+
+Running Test Generation
+-----------------------
+
+The testbuilder takes a command as its first command-line argument. Some of
+these commands require the model-name as a second argument:
+
+ Usage: ``tbuild <command> [<modelname>]``
+
+The commands provided are:
+
+``clean <model>``
+ Removes generated files.
+
+``spin <model>``
+ Runs SPIN to find all scenarios. The scenarios are found in numbered files
+ called ``<model>N.spn``.
+
+``gentests <model>``
+ Convert SPIN scenarios to test sources. Each ``<model>N.spn`` produces a numbered
+ test source file.
+
+``copy <model>``
+ Copies the generated test files to the relevant test source directory, and
+ updates the relevant test configuration files.
+
+``archive <model>``
+ Copies generated spn, trail, source, and test log files to an archive
+ sub-directory of the model directory.
+
+``compile``
+ Rebuilds the test executable.
+
+``run``
+ Runs tests in a simulator.
+
+``all <model>``
+ Does clean, spin, gentests, copy, compile, and run.
+
+``zero``
+ Removes all generated test filenames from the test configuration files, but
+ does NOT remove the test sources from the test source directory.
+
+In order to generate test files the following input files are required:
+ ``<model>.pml``,
+ ``<model>-rfn.yml``,
+ ``<model>-pre.h``,
+ ``<model>-post.h``, and
+ ``<model>-run.h``.
+In addition there may be other files
+whose names have <model> embedded in them. These are included in what is
+transfered to the test source directory by the copy command.
+
+The simplest way to check test generation is setup properly is to visit one of
+the models, found under ``formal/promela/models`` and execute the following
+command:
+
+.. code-block:: shell
+
+ tbuild all mymodel
+
+This should end by generating a file `model-0-test.log`. The output is
+identical to that generated by the regular RTEMS tests, using the
+*Software Test Framework* described elsewhere in this document.
+
+Output for the Event Manager model, highly redacted:
+
+.. code-block::
+
+ SIS - SPARC/RISCV instruction simulator 2.29, copyright Jiri Gaisler 2020
+ Bug-reports to jiri at gaisler.se
+
+ GR740/LEON4 emulation enabled, 4 cpus online, delta 50 clocks
+
+ Loaded ts-model-0.exe, entry 0x00000000
+
+ *** BEGIN OF TEST Model0 ***
+ *** TEST VERSION: 6.0.0.03337dab21e961585d323a9974c8eea6106c803d
+ *** TEST STATE: EXPECTED_PASS
+ *** TEST BUILD: RTEMS_SMP
+ *** TEST TOOLS: 10.3.1 20210409 (RTEMS 6, RSB 889cf95db0122bd1a6b21598569620c40ff2069d, Newlib eb03ac1)
+ A:Model0
+ S:Platform:RTEMS
+ ...
+ B:RtemsModelSystemEventsMgr8
+ ...
+ L:@@@ 3 CALL event_send 1 2 10 sendrc
+ L:Calling Send(167837697,10)
+ L:Returned 0x0 from Send
+ ...
+ E:RtemsModelEventsMgr0:N:21:F:0:D:0.005648
+ Z:Model0:C:18:N:430:F:0:D:0.130464
+ Y:ReportHash:SHA256:5EeLdWsRd25IE-ZsS6pduLDsrD_qzB59dMU-Mg2-BDA=
+
+ *** END OF TEST Model0 ***
+
+ cpu 0 in error mode (tt = 0x80)
+ 6927700 0000d580: 91d02000 ta 0x0
+
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/>`_.
diff --git a/eng/index.rst b/eng/index.rst
index a4d4563..e4712ae 100644
--- a/eng/index.rst
+++ b/eng/index.rst
@@ -11,6 +11,7 @@ RTEMS Software Engineering (|version|)
.. topic:: Copyrights and License
+ | |copy| 2022 Trinity College Dublin
| |copy| 2018, 2020 embedded brains GmbH & Co. KG
| |copy| 2018, 2020 Sebastian Huber
| |copy| 1988, 2015 On-Line Applications Research Corporation (OAR)
@@ -31,11 +32,13 @@ RTEMS Software Engineering (|version|)
management
test-plan
test-framework
+ fv/index
build-system
release-mgmt
users-manuals
license-requirements
appendix-a
+ fv/appendix-fv
function_and_variable
concept
glossary
More information about the vc
mailing list