Test Case Generation - Revision history

David Geleßus: /* With a test description file */ Fix heading level

2021-02-04T16:28:17Z

With a test description file: Fix heading level

← Older revision		Revision as of 16:28, 4 February 2021
Line 202:		Line 202:
	The generated test cases are stored in a file called test_results.xml. Just as with model-checking-based test case generation you can provide the empty filename <pre>''</pre>, in which case no file is generated, and an empty <tt>EndPredicate</tt> that will only lead to test cases of length 1.		The generated test cases are stored in a file called test_results.xml. Just as with model-checking-based test case generation you can provide the empty filename <pre>''</pre>, in which case no file is generated, and an empty <tt>EndPredicate</tt> that will only lead to test cases of length 1.

	=== With a test description file ===		==== With a test description file ====
	The configuration for the test case generation can also be provided as an XML file.		The configuration for the test case generation can also be provided as an XML file.
	The format is shown below:		The format is shown below:

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

2021-02-04T16:27:26Z

Update with content from prob2-doc (originally written by Jessica Petrasch)

Show changes

Michael Leuschel: /* References */

2020-06-15T09:31:27Z

References

← Older revision		Revision as of 09:31, 15 June 2020
Line 179:		Line 179:

	Enabling Analysis:		Enabling Analysis:
	* Ivaylo Dobrikov, Michael Leuschel. [https://www.sciencedirect.com/science/article/abs/pii/S0167642317301624?via%3Dihub Enabling Analysis for Event-B]. ~~Science of Computer Programming~~.		* Ivaylo Dobrikov, Michael Leuschel. [https://www.sciencedirect.com/science/article/abs/pii/S0167642317301624?via%3Dihub Enabling Analysis for Event-B]. Sci. Comput. Program. 158: 81-99. 2018.

	Explicit test-case generation:		Explicit test-case generation:
	* Sebastian Wieczorek, Vitaly Kozyura, Andreas Roth, Michael Leuschel, Jens Bendisposto, Daniel Plagge, Ina Schieferdecker. [https://rdcu.be/b4UxY Applying Model Checking to Generate Model-Based Integration Tests from Choreography Models]. Proceedings FATES 2009, TestCom 2009.		* Sebastian Wieczorek, Vitaly Kozyura, Andreas Roth, Michael Leuschel, Jens Bendisposto, Daniel Plagge, Ina Schieferdecker. [https://rdcu.be/b4UxY Applying Model Checking to Generate Model-Based Integration Tests from Choreography Models]. Proceedings FATES 2009, TestCom 2009.

Michael Leuschel: /* References */

2020-06-15T09:30:44Z

References

← Older revision		Revision as of 09:30, 15 June 2020
Line 179:		Line 179:

	Enabling Analysis:		Enabling Analysis:
	* Ivaylo Dobrikov, Michael Leuschel. [https://www.sciencedirect.com/science/article/abs/pii/S0167642317301624?via%3Dihub Enabling Analysis for Event-B]		* Ivaylo Dobrikov, Michael Leuschel. [https://www.sciencedirect.com/science/article/abs/pii/S0167642317301624?via%3Dihub Enabling Analysis for Event-B]. Science of Computer Programming.

	Explicit test-case generation:		Explicit test-case generation:
	* Sebastian Wieczorek, Vitaly Kozyura, Andreas Roth, Michael Leuschel, Jens Bendisposto, Daniel Plagge, Ina Schieferdecker. [https://rdcu.be/b4UxY Applying Model Checking to Generate Model-Based Integration Tests from Choreography Models]		* Sebastian Wieczorek, Vitaly Kozyura, Andreas Roth, Michael Leuschel, Jens Bendisposto, Daniel Plagge, Ina Schieferdecker. [https://rdcu.be/b4UxY Applying Model Checking to Generate Model-Based Integration Tests from Choreography Models]. Proceedings FATES 2009, TestCom 2009.

Michael Leuschel: /* References */

2020-06-15T09:27:06Z

References

← Older revision		Revision as of 09:27, 15 June 2020
Line 177:		Line 177:
	Constraint-based test-case generation using enabling analysis:		Constraint-based test-case generation using enabling analysis:
	* Aymerick Savary, Marc Frappier, Michael Leuschel. [https://link.springer.com/chapter/10.1007%2F978-3-319-22969-0_10 Model-Based Robustness Testing in Event-B Using Mutation]. Proceedings SEFM'2015.		* Aymerick Savary, Marc Frappier, Michael Leuschel. [https://link.springer.com/chapter/10.1007%2F978-3-319-22969-0_10 Model-Based Robustness Testing in Event-B Using Mutation]. Proceedings SEFM'2015.

			Enabling Analysis:
			* Ivaylo Dobrikov, Michael Leuschel. [https://www.sciencedirect.com/science/article/abs/pii/S0167642317301624?via%3Dihub Enabling Analysis for Event-B]

	Explicit test-case generation:		Explicit test-case generation:
	* Sebastian Wieczorek, Vitaly Kozyura, Andreas Roth, Michael Leuschel, Jens Bendisposto, Daniel Plagge, Ina Schieferdecker. [https://rdcu.be/b4UxY Applying Model Checking to Generate Model-Based Integration Tests from Choreography Models]		* Sebastian Wieczorek, Vitaly Kozyura, Andreas Roth, Michael Leuschel, Jens Bendisposto, Daniel Plagge, Ina Schieferdecker. [https://rdcu.be/b4UxY Applying Model Checking to Generate Model-Based Integration Tests from Choreography Models]

Michael Leuschel: /* References */

2020-06-15T09:23:38Z

References

← Older revision		Revision as of 09:23, 15 June 2020
Line 179:		Line 179:

	Explicit test-case generation:		Explicit test-case generation:
	* Sebastian ~~WieczorekVitaly KozyuraAndreas RothMichael LeuschelJens BendispostoDaniel PlaggeIna~~ Schieferdecker. [https://rdcu.be/b4UxY Applying Model Checking to Generate Model-Based Integration Tests from Choreography Models]		* Sebastian Wieczorek, Vitaly Kozyura, Andreas Roth, Michael Leuschel, Jens Bendisposto, Daniel Plagge, Ina Schieferdecker. [https://rdcu.be/b4UxY Applying Model Checking to Generate Model-Based Integration Tests from Choreography Models]

Michael Leuschel at 09:23, 15 June 2020

2020-06-15T09:23:18Z

← Older revision		Revision as of 09:23, 15 June 2020
Line 171:		Line 171:
	./probcli.sh simplecounter.mch -test_description simple_counter_test_description.xml		./probcli.sh simplecounter.mch -test_description simple_counter_test_description.xml
	</pre>		</pre>


			== References ==

			Constraint-based test-case generation using enabling analysis:
			* Aymerick Savary, Marc Frappier, Michael Leuschel. [https://link.springer.com/chapter/10.1007%2F978-3-319-22969-0_10 Model-Based Robustness Testing in Event-B Using Mutation]. Proceedings SEFM'2015.

			Explicit test-case generation:
			* Sebastian WieczorekVitaly KozyuraAndreas RothMichael LeuschelJens BendispostoDaniel PlaggeIna Schieferdecker. [https://rdcu.be/b4UxY Applying Model Checking to Generate Model-Based Integration Tests from Choreography Models]

Michael Leuschel: /* From the command line */

2020-01-07T11:17:43Z

From the command line

← Older revision		Revision as of 11:17, 7 January 2020
Line 120:		Line 120:
	<tt>count = MAX-1</tt> is true and the explored paths do not have a depth of more than 5 operations we would specify this as follows, where we use CLPFD and have a timeout of 2000 ms. for each explored trace:		<tt>count = MAX-1</tt> is true and the explored paths do not have a depth of more than 5 operations we would specify this as follows, where we use CLPFD and have a timeout of 2000 ms. for each explored trace:
	<pre>		<pre>
	./probcli.sh simplecounter.mch -~~cb_tests~~ 5 count=MAX-1 test_results.xml -~~cb_cover~~ Increase -p CLPFD true -p TIME_OUT 2000		./probcli.sh simplecounter.mch -cbc_tests 5 count=MAX-1 test_results.xml -cbc_cover Increase -p CLPFD true -p TIME_OUT 2000
	</pre>		</pre>
	The generated test cases are stored in a file called test_results.xml. You can provide the empty filename <pre>''</pre>; in this case no file is generated.		The generated test cases are stored in a file called test_results.xml. You can provide the empty filename <pre>''</pre>; in this case no file is generated.

Michael Leuschel: /* Introduction */

2016-04-18T06:24:56Z

Introduction

← Older revision		Revision as of 06:24, 18 April 2016
Line 15:		Line 15:
	ProB has two main algorithms to find suites of test cases:		ProB has two main algorithms to find suites of test cases:
	* model-checking based (invoked, e.g., using the [[Using_the_Command-Line_Version_of_ProB#-mcm_tests_.3CDepth.3E_.3CMaxStates.3E_.3CEndPredicate.3E_.3CFILE.3E\|mcm_tests]] command of [[Using_the_Command-Line_Version_of_ProB\|probcli]]) and		* model-checking based (invoked, e.g., using the [[Using_the_Command-Line_Version_of_ProB#-mcm_tests_.3CDepth.3E_.3CMaxStates.3E_.3CEndPredicate.3E_.3CFILE.3E\|mcm_tests]] command of [[Using_the_Command-Line_Version_of_ProB\|probcli]]) and
	* constraint-based (invoked, e.g., using the [[Using_the_Command-Line_Version_of_ProB#-cbc_tests_.3CDepth.3E_.3CEndPredicate.3E_.3CFile.3E\|cbc_tests]] command of [[Using_the_Command-Line_Version_of_ProB\|probcli]])		* constraint-based (invoked, e.g., using the [[Using_the_Command-Line_Version_of_ProB#-cbc_tests_.3CDepth.3E_.3CEndPredicate.3E_.3CFile.3E\|cbc_tests]] command of [[Using_the_Command-Line_Version_of_ProB\|probcli]]; more details can be found below)
	The former will run the model checker to generate the state space of the formal model, and will stop when the coverage criterion has been satisfied. The full state space of the model contains all possible initialisations of the machine, along with all possible values of the constants.		The former will run the model checker to generate the state space of the formal model, and will stop when the coverage criterion has been satisfied. The full state space of the model contains all possible initialisations of the machine, along with all possible values of the constants.
	The latter, will use ProB's constraint solver to generate feasible sequences of events in a breadth-first fashion and will also stop when the coverage criterion has been satisfied.		The latter, will use ProB's constraint solver to generate feasible sequences of events in a breadth-first fashion and will also stop when the coverage criterion has been satisfied.

Michael Leuschel: /* Introduction */

2016-04-18T06:24:17Z

Introduction

← Older revision		Revision as of 06:24, 18 April 2016
Line 14:		Line 14:

	ProB has two main algorithms to find suites of test cases:		ProB has two main algorithms to find suites of test cases:
	* model-checking based (invoked, e.g., using the [[Using_the_Command-Line_Version_of_ProB#-mcm_tests_.3CDepth.3E_.3CMaxStates.3E_.3CEndPredicate.3E_.3CFILE.3E\|mcm_tests]] command of [[Using_the_Command-Line_Version_of_ProB probcli]]) and		* model-checking based (invoked, e.g., using the [[Using_the_Command-Line_Version_of_ProB#-mcm_tests_.3CDepth.3E_.3CMaxStates.3E_.3CEndPredicate.3E_.3CFILE.3E\|mcm_tests]] command of [[Using_the_Command-Line_Version_of_ProB\|probcli]]) and
	* constraint-based (invoked, e.g., using the [[Using_the_Command-Line_Version_of_ProB#-cbc_tests_.3CDepth.3E_.3CEndPredicate.3E_.3CFile.3E\|cbc_tests]] command of [[Using_the_Command-Line_Version_of_ProB probcli]])		* constraint-based (invoked, e.g., using the [[Using_the_Command-Line_Version_of_ProB#-cbc_tests_.3CDepth.3E_.3CEndPredicate.3E_.3CFile.3E\|cbc_tests]] command of [[Using_the_Command-Line_Version_of_ProB\|probcli]])
	The former will run the model checker to generate the state space of the formal model, and will stop when the coverage criterion has been satisfied. The full state space of the model contains all possible initialisations of the machine, along with all possible values of the constants.		The former will run the model checker to generate the state space of the formal model, and will stop when the coverage criterion has been satisfied. The full state space of the model contains all possible initialisations of the machine, along with all possible values of the constants.
	The latter, will use ProB's constraint solver to generate feasible sequences of events in a breadth-first fashion and will also stop when the coverage criterion has been satisfied.		The latter, will use ProB's constraint solver to generate feasible sequences of events in a breadth-first fashion and will also stop when the coverage criterion has been satisfied.