Tutorial Model-Based Testing - Revision history

David Geleßus: Update with content from prob2-doc (originally written by Jessica Petrasch)

2021-02-04T16:07:54Z

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.
-== 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.
-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]]
 == Constraint-Based Testcase Generation ==
-[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]].

Michael Leuschel: /* Model-Checking Based Testcase Generation */

2014-10-28T15:51:46Z

Model-Checking Based Testcase Generation

← Older revision		Revision as of 15:51, 28 October 2014
Line 31:		Line 31:
	Select the "Stop when all OPERATIONS Covered" check box in the model checking dialog:		Select the "Stop when all OPERATIONS Covered" check box in the model checking dialog:

	[[file:StopWhenAllOpsCovered.png\|center\|\|~~300px~~]]		[[file:StopWhenAllOpsCovered.png\|center\|\|200px]]

			Press the "Model Check" button; after a short while ProB should respond with

			[[file:AllOpsCoveredDialog.png\|center\|\|200px]]

	[TODO]		[TODO]

Michael Leuschel: Created page with '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…'

2014-10-28T15:50:28Z

Created page with '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…'

New page

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:

<PRE>
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
</PRE>

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: <b>operation coverage</b>, 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 Testcase Generation ==

Select the "Stop when all OPERATIONS Covered" check box in the model checking dialog:

[[file:StopWhenAllOpsCovered.png|center||300px]]

[TODO]

== Constraint-Based Testcase Generation ==

[TODO]