1 files changed, 62 insertions, 0 deletions
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``.
+