MBT plugin

MBT (Model-Based Testing) for Event-B plugin

Installing

The MBT for Event-B plugin (also referred to as MBT plugin) relies on Rodin release 2.0 or newer and ProB plugin 2.2 or newer. The following steps 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 installation instructions here...
5. Install the MBT for Event-B 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, a test suite is a collection of test cases.

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

Whenever the generated cover automaton is found inaccurate, a counterexample path (a collection/sequence of events) must be provided and the Learn DFCA algorithm must be re-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, starting with the most abstract machine and ending with the selected one.

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 cover automaton which will be generated.

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.

Displaying the generated cover automaton

The second wizard page displays the computed cover automaton and (if this is the case) the timeout paths. A timeout path is a sequence of events of length at most $l$, for which no test data were found to trigger it within a given time bound. 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 and the transitions are labeled with event names.

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
• providing a counterexample path

Displaying 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, e.g. the all events coverage criterion.

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

Displaying the optimized test suite

It displays a list of test cases along with the corresponding test data, with respect to the selected coverage criterion.

If the all events coverage criterion was selected for test suite optimization and was not satisfied, a list of uncovered events is provided.

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

• proceeding 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

By proceeding to the next refinement, it causes for a more concrete Event-B machine (which refines the current one) to be loaded and for the DFCA to be recomputed such that to accept new sequences which include the new events of the loaded machine.

Providing a counterexample path

A counterexample path is sequence of events of length at most $l$, which was not accepted by the generated cover automaton. By providing a counterexample, the Learn DFCA algorithm will compute a new DFCA which accepts it, if there exist test data to trigger the given event sequence.

The events of the current Event-B machine and their parameters are displayed in the "Event list" table. By double-clicking an event (or selecting it and then pressing the green arrow) it is added to the "Selected path" list. The events from the constructed sequence can be reordered by using the blue arrows or deleted by using the red cross button.

After building a counterexample path and clicking Next, the wizard returns to displaying the computed DFCA.

Licensing

The MBT for Event-B plugin and the accompanying materials are made available under the terms of the Eclipse Public License v1.0.

The MBT plugin uses the Java Universal Network/Graph Framework (JUNG), licensed as follows:

Copyright (c) 2003-2004, Regents of the University of California and the JUNG Project

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

• Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.
• Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.
• Neither the name of the University of California nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.