top level FV hierarchy

6 files changed, 185 insertions, 0 deletions

diff --git a/formal/.gitignore b/formal/.gitignore
new file mode 100644
index 00000000..2cfdbe69
--- /dev/null
+++ b/formal/.gitignore
@@ -0,0 +1,3 @@
+NOTES.pdf
+*.out
+
diff --git a/formal/README.md b/formal/README.md
new file mode 100644
index 00000000..d3ff71a6
--- /dev/null
+++ b/formal/README.md
@@ -0,0 +1,27 @@
+# Formal Verification
+
+`formal`
+
+This directory contains the models and tooling developed as part of the ESA-sponsored activity ***Qualification of RTEMS Symmetric Multiprocessing
(SMP)***, that has been added into RTEMS in the `rtems-central` repository.
+
+## Contributors
+
+* Andrew Butterfield
+* Frédéric Tuong
+* Robert Jennings
+* Jerzy Jaśkuć
+* Eoin Lynch
+* James Gooding Hunt
+
+## License
+
+This project is licensed under the
+[BSD-2-Clause](https://spdx.org/licenses/BSD-2-Clause.html) or
+[CC-BY-SA-4.0](https://spdx.org/licenses/CC-BY-SA-4.0.html).
+
+## Overview
+
+At present, the only formal verification in play here is the use of Promela to build formal models of key RTEMS components, and the SPIN model-checker to perform C test generation.
+
+This can be found in the `promela` sub-directory
+
diff --git a/formal/promela/.gitignore b/formal/promela/.gitignore
new file mode 100644
index 00000000..5b5b65fa
--- /dev/null
+++ b/formal/promela/.gitignore
@@ -0,0 +1,4 @@
+*/refine_command.py
+*/spin2test.py
+*/pan*
+*/testbuilder.yml
diff --git a/formal/promela/README.md b/formal/promela/README.md
new file mode 100644
index 00000000..87f7299e
--- /dev/null
+++ b/formal/promela/README.md
@@ -0,0 +1,27 @@
+# Promela/SPIN
+
+`formal/promela`
+
+This directory contains formal models written in Promela and tools that use SPIN to do test generation from those models.
+
+## Contributors
+
+* Andrew Butterfield
+* Frédéric Tuong
+* Robert Jennings
+* Jerzy Jaśkuć
+* Eoin Lynch
+* James Gooding Hunt
+
+## License
+
+This project is licensed under the
+[BSD-2-Clause](https://spdx.org/licenses/BSD-2-Clause.html) or
+[CC-BY-SA-4.0](https://spdx.org/licenses/CC-BY-SA-4.0.html).
+
+## Overview
+
+The  Promela models and supporting material can be found in the `models` subdirectory.
+
+The tools, written in Python3, are in the `src` directory.
+
diff --git a/formal/promela/models/README.md b/formal/promela/models/README.md
new file mode 100644
index 00000000..17de6f2b
--- /dev/null
+++ b/formal/promela/models/README.md
@@ -0,0 +1,53 @@
+# RTEMS Promela Models
+
+`formal/promela/models/'
+
+This directory contains formal models written in Promela to support test generation.
+
+## Contributors
+
+* Andrew Butterfield
+* Frédéric Tuong
+* Robert Jennings
+* Jerzy Jaśkuć
+* Eoin Lynch
+
+## License
+
+This project is licensed under the
+[BSD-2-Clause](https://spdx.org/licenses/BSD-2-Clause.html) or
+[CC-BY-SA-4.0](https://spdx.org/licenses/CC-BY-SA-4.0.html).
+
+## Models Overview
+
+There are currently five models present. Four are test-generation ready, whilst the fifth is still work in progress.
+
+We identify the usual RTEMS name for the component,
+the Promela "model-name", and the path to the model directory.
+
+* Barrier Manager: "barrier-mgr-model" `formal/promela/models/barriers`
+* Chains API:  "chains-api-model" `formal/promela/models/chains`
+* Event Manager "event-mgr-model" `formal/promela/models/events`
+* Message Manager "msg-mgr-model" `formal/promela/models/messages`
+* MrsP Thread Queues "mrsp-threadq-model" `formal/promela/models/threadq`
+
+## Doing Test Generation
+
+Ensure that the virtual environment defined in `formal/promela/src/env` is active.
+
+We shall assume that the alias `tb` has been defined as suggested in  `formal/promela/src/README.md`.
+
+Simply enter the relevant model sub-directory and invoke `tb` from the command line with desired command line arguments.
+
+A simple sequence that clears out all previously generated tests (from all models), clears all generated artifacts from this model,
+and then does the whole test generation process is:
+
+```
+tb zero
+tb clean
+tb all <model-name>
+```
+
+This will produce a test report in `<testsuite>-test.log`.
+
+
diff --git a/formal/promela/src/README.md b/formal/promela/src/README.md
new file mode 100644
index 00000000..dd80420a
--- /dev/null
+++ b/formal/promela/src/README.md
@@ -0,0 +1,71 @@
+# Test Generation Tools
+
+`formal/promela/src`
+
+This directory contains tools that use SPIN to do test generation from Promela models.
+
+## Contributors
+
+* Andrew Butterfield
+* Frédéric Tuong
+* Robert Jennings
+* James Gooding Hunt
+
+## License
+
+This project is licensed under the
+[BSD-2-Clause](https://spdx.org/licenses/BSD-2-Clause.html) or
+[CC-BY-SA-4.0](https://spdx.org/licenses/CC-BY-SA-4.0.html).
+
+
+## Tool Setup
+
+### Prerequisites
+
+The Promela/SPIN tool is required. It can be obtained from [spinroot.com](https://spinroot.com). Follow the installation instructions there and ensure that the executable `spin` is on your `$PATH`.
+
+### Tool Installation
+
+From within `formal/promela/src` do:
+
+```
+make env
+. env/bin/activate
+make py
+```
+
+Alternatively, you can run `src.sh`.
+
+You need to activate this virtual environment to use the toolset.
+
+### Tool Configuration
+
+The top-level program is `testbuilder.py`. 
+
+It relies on a configuration file `testbuilder.yml` that defines various key names/paths related to your RTEMS installation. A template file `testbuilder-template.yml` is provided. This should be edited to reflect your setup, and than saved as `testbuilder.yml`.
+
+
+To simplify matters, it helps to create a short alias for the full pathname to `testbuilder.py`. This should be defined in `.bashrc` or similar.
+
+```
+alias tb=path-to-formal/formal/promela/src/testbuilder.py
+```
+
+If all this is setup, then a quick test is simply to run the program without command line arguments, which will then issue a help statement:
+
+```
+:- tb
+USAGE:
+help - these instructions
+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
+```
+
+If there are obvious problems with `testbuilder.yml`, it will report an error.