Formal Tools Setup

9.4. Formal Tools Setup#

The required formal tools consist of the model checking software (Promela/SPIN), and the test generation software (spin2test/testbuilder).

9.4.1. Installing Tools#

9.4.1.1. 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 (nimble-code/Spin).

9.4.1.2. 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:

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.):

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:

(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.

9.4.2. 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:

# 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)

9.4.2.1. 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:

    - role: build-dependency
  uid: model-0

  • Copy validation-0.yml (say) to model-0.yml, and change the following entries as shown:

    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.

9.4.3. 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:

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:

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