COVER – Generating Test-Vectors for Simulink/Stateflow Models

About COVER

COVER is a test-vector generation toolset for Matlab Simulink/Stateflow models. As backend COVER uses bounded model checking for fast generation of test-vectors achieving high coverage.

For questions about COVER, con­tact Daniel Kroening, Nannan He or Michael Tautschnig. You should also read the license.

Documentation

Our testing process consists of three main steps:

1. Translation of the model to goto binaries.
2. Test-vector generation.
3. Model-level simulation using test-vectors as input.

Using the binaries available for download below, these steps are performed as follows:

1. Translation:

     $ ./cprover --convert MODEL.mdl
     $ ./goto-cc -I simulink/ *.c simulink/blocktypes/*.c -o mdl.bin

   For Windows, use the following command line instead:

     $ cprover --convert MODEL.mdl
     $ goto-cl /I simulink *.c simulink\blocktypes\*.c /Femdl.bin

2. Generate test vectors:

     $ ./cover --unwind 10 mdl.bin --outfile tests

   This step produces a series of testsXYZ.xml files, where each file describes one test vector.
3. Use the test vectors in the simulation. To do so, add the block from our atc2xml.mdl file as provided in the distribution to your model. Its property dialog allows to select one of the generated test vector files.

To experiment with those steps, you may use our example.mdl file.

We also provide papers that describe how COVER works.

• Test-Case Generation for Embedded Simulink via Formal Concept Analysis
• Mutation-based Test Case Generation for Simulink Models