--- formal/.gitignore | 3 ++ formal/README.md | 27 +++++++++++++ formal/promela/.gitignore | 4 ++ formal/promela/README.md | 27 +++++++++++++ formal/promela/models/README.md | 53 ++++++++++++++++++++++++ formal/promela/src/README.md | 71 +++++++++++++++++++++++++++++++++ 6 files changed, 185 insertions(+) create mode 100644 formal/.gitignore create mode 100644 formal/README.md create mode 100644 formal/promela/.gitignore create mode 100644 formal/promela/README.md create mode 100644 formal/promela/models/README.md create mode 100644 formal/promela/src/README.md
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. -- 2.37.1 (Apple Git-137.1) _______________________________________________ devel mailing list devel@rtems.org http://lists.rtems.org/mailman/listinfo/devel