User Guide

First steps

When you open BETA for the first time you’ll be welcomed by the following screen:

BETA first screen

The first thing you should do before you start using the tool is to make sure you have the path to the ProB directory configured on the Settings menu. To do this you should click on the Options menu on the top left and select Settings as presented bellow:

Settings

Loading a machine

The BETA approach generates unit tests for operations of an abstract B machine individually. The first thing you should do to generate tests for an operation is to open it respective machine. You can download the SimpleLift.mch machine and use it to follow the remainder of this guide.

Proceed clicking on the Options menu and selecting the Load Machine option. Locate the SimpleLift.mch file you just downloaded and click on Open. You’ll be presented to the following screen:

Load Machine

At this step the tool will present the following information (highlighted on the image above):

  1. The name of the machine you just loaded;

  2. The list of operations specified in this machine.

Generating tests

Now that we have loaded a machine on the tool we have to select the operation we intend to generate unit tests for. For this example we are going to select the “go_up” operation. Before we generate the unit test report we have to define the parameters of our report wich are defined on the menu shown bellow:

Test Case Generation Parameters

The image presents in:

  1. The Testing Strategy to be used in the unit test generation. To tool provides two options: Input Space Coverage and Logical Coverage;

  2. The Coverage Criteria that will be used to define the requirements of the test cases generated. For Input Space Coverage the tool provides six options: Equivalent Classes (Each-Choice), Equivalent Classes (Pairwise), Equivalent Classes (All-Combinations), Boundary Analysis (Each-Choice), Boundary Analysis (Pairwise) and Boundary Analysis (All-Combinations). For Logical Coverage the tool provides four options: Predicate Coverage, Clause Coverage, Combinatorial Clause Coverage and Active Clause Coverage.

Once the test generation parameters are defined, the user should click on the Generate Tests button. Then, following screen will be presented:

Report Generation Window

In this window the user is able to select how he or she wants to generate the test cases. The tool currently supports the generation of HTML and XML test case specifications. It also has a separate module that is capable of generating partial test scripts in Java and C++. Once the types of test cases are selected, the user should click on the Generate Report button. After the tests are generated, the tool should present the following window:

Reports Generated Window

The test cases generated will be located in the same directory of the machine we are testing. You can navigate through the generated report clicking here. This is how the report looks like:

Report Example

Other Information

In this spreadsheet you will find an overview on how predicates are partitioned into blocks for different types of characteristics extracted from the model. For more detailed information on this topic, read this report

More examples

You can download more examples of B specifications to use in the tool clicking here

Case Studies

So far we have done two case studies: CGP and FreeRTOS.

How to use the generated XML file

BETA is able to generate a test suite using the XML format. Visit this link to learn how to use it so you can integrate the tests generated by BETA into your own tool.