ChainCover Test Chain Generation for Reactive Systems

Tutorial

ChainCover is to be used within the following tool chain:
tool chain

ChainCover generates a test chain for a set of requirements specified by properties / test goals (in the safety fragment of linear temporal logic).

Usage

Full code examples are included in the examples directory of the distribution package.

ChainCover takes a list of source files and a configuration XML file. To run ChainCover on the cruise example, go into the examples/cruise directory type make cfg1.

If everything works fine, after a few seconds, this will produce an output like

[...]
1 test vector(s) found:
testvector0[9] =
{
new_i = { .signal=2 },
new_i = { .signal=2 },
new_i = { .signal=1 },
new_i = { .signal=3 },
new_i = { .signal=4 },
new_i = { .signal=3 },
new_i = { .signal=3 },
new_i = { .signal=5 },
new_i = { .signal=1 }
}
covers 5 test goals:
{
c::prop1,
c::prop2,
c::prop3,
c::prop4,
c::final
}

indicating the length of the generated test case chain, the input values for each execution step, and the test goals covered. You can use --xml-ui to produce XML output.

ChainCover can operate in several modes:

  • SAT-Based Test Chain Generation
  • SAT-Based Test Vector Generation
  • SAT+TSP-Based Test Chain Generation

    SAT-Based Test Chain Generation

    In this mode, ChainCover searches for single test vectors of minimised length that cover all test goals (specified as assertions). Currently, it will not terminate if such a test chain does not exist. Multiple test chains are supported by the SAT-TSP-Based Test Chain Generation (see below).

    To do this, ChainCover must be given a loop to be unwound incrementally:

    chaincover/chaincover ../examples/cruise/cruise.c --chain --incremental-check c::main.3

    Properties / Test Goals

    Properties / test goals to be chained are typically stated as follows:

    if((s_old.mode==1) && (s_old.speed==1) && (s_old.button==1) && (i.signal==I_DEC)) __CPROVER_assert(s.speed==1,"c::prop1");

    Configuration File

    Using the option --config mycfg.xml, ChainCover can be provided with a configuration file that contains some parameters and a list of test goals to be considered. By default, ChainCover automatically guesses the configuration. The guessed configuration can be written to a file by adding the options --output-config --config mycfg.xml.

    Test Vector Output

    Besides text and XML output, test vectors can be written into a header file as C code using the option --output-tests tests.h, which facilitates the integration into a test harness for test execution.

    SAT-Based Test Vector Generation

    In this mode, ChainCover covers all test goals in the code (specified as assertions) with shortest possible test vectors and removes redundant test vectors.

    ChainCover can be run in a non-incremental way:

    chaincover/chaincover ../examples/cruise/cruise.c --no-chain

    or incrementally by specifying a loop to be unwound incrementally:

    chaincover/chaincover ../examples/cruise/cruise.c --no-chain --incremental-check c::main.3

    Test goals can also be automatically generated with the help of goto-instrument. Running

    ../lib/cbmc-CBMC_VERSION/src/goto-cc/goto-cc ../examples/cruise/cruise.c -o ../examples/cruise/cruise.o
    goto-instrument/goto-instrument ../examples/cruise/cruise.o ../examples/cruise/cruise.i.o --branchtest --functiontest

    instruments the program with test goals for branch coverage and function coverage. Test vectors can then be generated by

    chaincover/chaincover ../examples/cruise/cruise.i.o --no-chain

    SAT+TSP-Based Test Chain Generation

    In this mode, ChainCover searches for single test vectors of minimised length that cover all test goals. If this is not possible it will generate a minimised number of test vectors that, together, cover all test goals.

    Configuration File

    ChainCover can be provided with a configuration file that contains parameters about the functions, types, and properties to be considered. You can also make ChainCover automatically guess the configuration by simply running

    chaincover/chaincover ../examples/cruise/cruise.c --chain-properties

    The guessed configuration can be written to a file by adding the options --output-config --config mycfg.xml.

    LKH is the default TSP backend. For Clingo, use the option --clingo.

    By default, abstraction refinement is used (see paper). To use the path constraints-based method, add the options --path-constraints --clingo to the command.

    By default, ChainCover will generate multiple chains if a single chain cannot be found; to search for single chains only, use the option --no-multi-chain.

    Generated C Code

    ChainCover assumes that the generated C code consists of two functions:

    • a initialisation function that initialises the state of the model; and
    • a compute function that computes an exection step of the model.
    Moreover, it is assumed that state and input variables are organised in C structs that are passed to the above functions.
    For example, the Simulink code generator Gene-Auto produces such C code.

    Requirements Specification

    ChainCover generates a test chain for a set of requirements specified by properties (in the safety fragment of linear temporal logic). Properties are written as C functions. For example,

    G ((mode=ON && speed=1 && brake) => (X speed=1))

    is straightforwardly written as

    void prop1(io_t* i, t_state* s) {
      __CPROVER_assume(s->mode==ON && s->speed==1 && i->brake);
      compute(i,s);
      assert(s->speed==1);
    }

    or, for instance,

    G (speed=2 && brake && (X brake)) => (XX speed==0)

    as

    void prop2(io_t* i1, state_t* s) {
      io_t i2;
      __CPROVER_assume(s->mode==ON && s->speed==1 &&
          i1->brake && i2.brake);
      compute(i1,s);
      compute(&i2,s);
      assert(s->speed==0);
    }

    State Invariant

    At last, ChainCover requires a state invariant in order to restrict the range of the state variables to the reachable values. The state invariant can be computed with a static analyser or, in most cases, easily derived from the Stateflow diagram, for example. Again the state invariant is defined as a C function:

    void state_assume(state_t* s) {
      __CPROVER_assume((s->mode==ON || s->mode==OFF) &&
        0<=s->speed && s->speed<=2);
    }

    Configuration File

    ChainCover can be parametrised using an XML configuration file. If no file is given, ChainCover will guess the configuration from the source files (see Usage above). The configuration file contains state and I/O struct types, function names for state invariant, initialisation and step, as well as bounds for reachability queries and chain length and function names of the initial and final state of the chain and the properties. Typically, it looks as follows:

    <chaincover-config>
      <program>
        <state-type>c::tag-state_t</state-type>
        <io-type>c::tag-io_t</io-type>
        <state-assume>c::state_assume</state-assume>
        <init>c::init</init>
        <step>c::compute</step>
      </program>
      <chain>
        <init>c::init</init>
        <final>c::final</final>
        <reach-bound>10</reach-bound>
        <chain-bound>0</chain-bound>
        <testgoals>
          <testgoal>c::prop1</testgoal>
          <testgoal>c::prop2</testgoal>
          <testgoal>c::prop3</testgoal>
          <testgoal>c::prop4</testgoal>
        </testgoals>
      </chain>
    </chaincover-config>

    Common Errors

    ABORTED: ERROR: cannot open file __in__.res and ABORTED: ERROR: parse error in clingo result file indicate that the LKH or clingo executables are not on the PATH.

     

    Back to the main page