README

Linking Promela/SPIN to RTEMS-SMP C Tests

A demonstration prototype for proposed RTEMS Qualification tools.

This demonstrates a way to use the Promela/SPIN model checker to generate tests for RTEMS API code. The tester has to develop:

1. A Promela model of the API calls of interest, with print statements that output key API "events" in an easy to parse notation.
2. Some C code boilerplate files used to setup (and teardown) tests
3. A YAML file that maps key Promela model concepts into C test fragments

The tool described here will then use the above information to generate a C test. The use of the tool will itself be easy to automate, and is intended to be part of the RTEMS qualification toolset.

All feedback welcome

INSTALL

Prerequisites

This requires Python3, and PyYAML and Coconut packages.

pip3 install pyyaml
pip3 install coconut

It also requires an installation of the SPIN Model checker (spinroot.com), which itself requires a C compiler plus yacc/lex and other standard C tools.

Build

The source file for the tool is spin2test.coco. To compile it do

coconut spin2test.coco

This will create a python script spin2test.py.

Test Generation

We are going to do test generation for a simple Chains API example (chains.pml).

A counter-example generated by a simulation or verification run of chains.pml, e.g.

spin -run chains.pml
spin -t -T chains.pml > chains.spn

We then run the test generator, giving it the root filename "chains" as a parameter:

python3 spin2test.py chains

This will take chains.spn, along with chains-pre.h, chains-rfn.yml, and chains-post.h, and use these to generate a C test program chains-test.c.

Test Running

The example here works with the new RTEMS Testing Framework, but similar examples could be constructed for the old framework. The test should be installed into the RTEMS test system and built, as chains-test.exe, perhaps.

The test can be run and saved by using a simulator (we assume the leon3 BSP here):

sparc-rtems5-sis -leon3 -r s -m 4 path-to/chains-test.exe > chains-test.log

Here we assume sparc-rtems5-sis is on our $PATH.

File Manifest

The repository top-level contains the minimal set of files required to generate everything. The generated folder includes all the files that are generated, so they can be inspected without having to install and build anything.

chains-pure.pml

A Promela model that looks at the behaviour of the "append" and "get" operations in the RTEMS Chains API. It has no printf statements.

chains.pml

The Promela model above modified so that key points in the model have Promela printf statements, starting with "@@@" that output lines to be used by the test generation software.

generated/chains.pml.trail

A counter-example data-file generated by a simulation or verification run of chains.pml, stored as a SPIN "trail" file.

generated/chains.spn

A counter-example readable textfile generated from the "trail" file.

chains-rfn.yml

A YAML File describing the refinement relationship between the Promela model and C code.

chains-X.h

For X in pre, post : standard boiler-plate code to open and close the generated test program.

generated/chains-test.c

The automatically generated C test code.

generated/chains-test.exe

The SPARC LEON3 executable built in RTEMS.

generated/chains-test.log

The test log output, obtained

Syntax for Promela "@@@" lines

The general format of these lines is @@@<key> <param1> <param2> ... <paramN>.

The <key> component ranges over NAME, DEF, DECL, INIT, SCALAR, STRUCT, SEQ, and CALL.

• NAME name - overall name of test program.
• DEF macroname value - used when there is a #define in the Promela file that needs to be copied over to the test C program.
• DECL decl indicates a global variable declaration that needs a corresponding one in the test program.
• INIT - identifies the test-specific initialisation point.
• SCALAR name val - asserts that variable name has value val.
• PTR name addr - asserts that pointer name has, as value, the address addr.
• STRUCT name, ..., END name - supports displaying current state of a structure. The components ... are a list of SCALAR and PTR forms
• SEQ name, ..., END name, - supports displaying current state of a global variable name referring to a sequence of values (...). The values are listed using SCALAR _ val (the _ indicates that a name is irrelevant here).
• CALL name p1 ... pN - calling Promela function/process name with arguments p1 through pN.

Refinement file format

This is a YAML file that defines a dictionary used to map Promela names into the corresponing C test code. More details to follow.