Tutorial Model-Based Testing

We assume that you have completed Tutorial Complete Model Checking. It may also be a good idea to complete the Tutorial_Model_Checking,_Proof_and_CBC.

Let us examine the following B model:

MACHINE SimpleAccount
CONSTANTS minb,maxb
PROPERTIES
 minb < maxb &
 minb <= 0 &
 maxb >= 0 & maxb > 1000
VARIABLES balance
INVARIANT
 balance: minb..maxb
INITIALISATION balance:=0
OPERATIONS
  Deposit(s) = SELECT s>0 & balance+s<= maxb THEN balance := balance + s END;
  Withdraw(s) = SELECT s>0 & balance-s >= minb THEN balance := balance - s END;
  NoWithrawalPossible = SELECT balance = minb THEN skip END;
  NoDepositPossible = SELECT balance = maxb THEN skip END
END

In model-based testing you want to generate traces for your model which satisfy a certain coverage criterion. Currently, ProB basically supports one coverage criterion: operation coverage, i.e., ProB tries to cover all operations (aka events for Event-B).

There are two ways this coverage can be achieved systematically: using model checking or using a constraint-based approach.

Model-Checking Based Test Case Generation

To start the test case generation select Analyse > "Testing" > "model-checking-based test case generation...". In the appearing window one can set some parameters:

• Output file: Enter a filename in the first text field to save the test cases in this file.
• Predicate: Enter the predicate that the last state in a test case has to satisfy. Leaving this field empty leads to test cases of length 1 only.
• Operations: Choose the operations/events that should be covered.
• Depth: Enter the maximum depth of a trace in the state space.
• States: Enter the maximum number of states in the state space to be explored.

Clicking OK will start the test case generation. After a short while you will see the following window:

You cannot look at the test cases in ProB. Instead you can open the file you just saved the results to. It contains the three generated test cases in XML format:

<extended_test_suite>
  <test_case id="1" targets="[Deposit]">
    <global>
      <step id="1" name="INITIALISATION">
      <value name="minb">-1</value>
    </step>
      <step id="2" name="Deposit">
      <value name="s">10</value>
    </step>
    </global>
  </test_case>
  <test_case id="2" targets="[NoWithdrawalPossible]">
    <global>
      <step id="1" name="INITIALISATION">
      <value name="minb">0</value>
    </step>
      <step id="2" name="NoWithdrawalPossible" />
      <step id="3" name="Deposit">
      <value name="s">10</value>
    </step>
    </global>
  </test_case>
  <test_case id="3" targets="[Withdraw]">
    <global>
      <step id="1" name="INITIALISATION">
      <value name="minb">-1</value>
    </step>
      <step id="2" name="Deposit">
      <value name="s">1</value>
    </step>
      <step id="3" name="Withdraw">
      <value name="s">1</value>
    </step>
      <step id="4" name="Deposit">
      <value name="s">10</value>
    </step>
    </global>
  </test_case>
</extended_test_suite>

Constraint-Based Testcase Generation

The constraint-based test case generation can be started by selecting Analyse > "Testing" > "constraint-based test case generation...". In the appearing window one can set the same parameters as described before (except for the maximum number of states). Clicking on "View CBC Test Tree" in the window popping up will open another window showing the test cases.

More examples and information on how to execute the test case generation via the command line can be found in the documentation on Test Case Generation.