Tutorial Model-Based Testing: Difference between revisions

(Update with content from prob2-doc (originally written by Jessica Petrasch))
 
Line 27: Line 27:
There are two ways this coverage can be achieved systematically: using model checking or using a constraint-based approach.
There are two ways this coverage can be achieved systematically: using model checking or using a constraint-based approach.


== Model-Checking Based Testcase Generation ==
== Model-Checking Based Test Case Generation ==


Select the "Stop when all OPERATIONS Covered" check box in the model checking dialog:
To start the test case generation select ''Analyse'' > "Testing" > "model-checking-based test case generation...". In the appearing window one can set some parameters:


[[file:StopWhenAllOpsCovered.png|center||200px]]
* 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.


Press the "Model Check" button; after a short while ProB should respond with
[[File:MBT-MCM-Dialog-Acc.png|center]]


[[file:AllOpsCoveredDialog.png|center||200px]]
Clicking ''OK'' will start the test case generation. After a short while you will see the following window:


[TODO]
[[File:MBT-MCM-Result-Acc.png|center]]
 
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:
 
<pre><nowiki>
<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>
</nowiki></pre>


== Constraint-Based Testcase Generation ==
== 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.
[[File:MBT-CBC-Tree-Acc.png|center]]


[TODO]
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]].

Latest revision as of 16:07, 4 February 2021

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.
MBT-MCM-Dialog-Acc.png

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

MBT-MCM-Result-Acc.png

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.

MBT-CBC-Tree-Acc.png

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.