mirror of
https://git.rtems.org/rtems-docs/
synced 2025-05-15 02:07:11 +08:00
318 lines
9.6 KiB
ReStructuredText
Executable File
318 lines
9.6 KiB
ReStructuredText
Executable File
.. 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
|
|
|