eng: Add formal verification chapter

11 files changed, 3268 insertions, 0 deletions

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@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