MBT plugin

MBT (Model-based testing) for Event-B plugin [TODO]

Installing

The MBT plugin relies on Rodin release 2.0 or newer and ProB plugin 2.2 or newer. The following steps will guide you through the installation process:

1. Download the latest Rodin release for your platform from Sourceforge.
2. Extract the downloaded zip file.
3. Start Rodin from the folder where you extracted the zip file in the previous step.
4. Install the ProB plugin:
   1. See ProB instalation instructions...
5. Install the MBT plugin:
   1. In the menu choose Help -> Install New Software....
      1. Click Add....
      2. As Location enter http://fmi.upit.ro/mbt_plugin
      3. Enter a name e.g. MBT for Event-B Plugin.
      4. Click Ok.
6. Restart Rodin as suggested.

Now you should be ready to use the MBT for Event-B plugin.

Usage

This section should help you to get started with the MBT plugin.

Short theoretical aspects

The MBT for Event-B plugin iteratively constructs a subset of the state space of an Event-B model (which is essentially an abstract state machine where the states can be implicitly derived from the values of the model variables), together with an associated test suite, using an incremental model learning which keeps under control the state space explosion. In the following, we will refer to this process as the Learn DFCA algorithm.

The state model constructed is based on the concept of deterministic finite cover automaton (DFCA) of a finite set $L$, which is a deterministic finite automaton which accepts all sequences in $L$ but may also accept sequences that are longer than every sequence in $L$, with respect to an upper bound $l$ on the length of the considered sequences.

Given an Event-B model and an upper bound $l$, the MBT plugin will incrementally construct finite cover automata that will eventually cover all executable event sequences of length less than or equal to $l$. Also, a set of test cases associated with the cover automata is evolved during iterations, along with the corresponding test data that makes them executable on the Event-B model.

The execution of a test case implies the existence of appropriate test data for the events, i.e. appropriate values for the event parameters in order to ensure that the corresponding guard is true. By definition, test suite is a collection of test cases.

The state model is constructed in a gradual manner, permitting the integration of the refinement in this process.

Whenever the generated cover automaton is found inaccurate, a counterexample path (a collection of events) must be found and the Learn DFCA algorithm must be executed.

Starting the plugin

To start the MBT for Event-B plugin, the "Generate Test Suite" action must be selected from the context menu of an Event-B machine.

The plugin workflow is based on the concept of wizard, guiding the user step by step toward test suite generation.

Setting the constant value

The first step requires the user to specify the value for the maximum sequence length constant ($l$), which is the upper bound on the length of the event sequences accepted by the generated cover automaton.

By clicking the Next button, the Learn DFCA algorithm is executed, computing the deterministic finite cover automaton and the associated test suite along with the corresponding test data.

The generated cover automaton

The second wizard page displays the computed cover automaton and eventually the timeout paths.

In the graphical representation of the automaton, the final states are drawn in double line, whereas non-final states are drawn in single line. The initial state is labeled q0.

A timeout path is a sequence of events of length at most l, for which no test data were found to trigger it.

Based on the user selection, the following options are available:

• moving the generated automaton as a whole
• repositioning selected states of the automaton or highlighting transitions
• displaying the generated test suite, causing another wizard page to be displayed
• providing a counterexample path, causing another wizard page to be displayed

Display the generated test suite

By choosing to view the generated test suite a list of test cases is provided, along with the corresponding test data.

The MBT for Event-B plugin provides a means for optimizing a test suite according to a chosen coverage criteria, i.e. all events coverage criterion.

By selecting a coverage criterion and clicking Next the optimized test suite is displayed.

Display the optimized test suite

Based on the user selection, the following options are available:

• proceed to the next refinement, causing the Learn DFCA algorithm to be executed for a more concrete machine which refines the current one
• providing a counterexample path

Provide a counterexample path