MBT plugin - Revision history

imported>Alinstef: /* Installing */

2012-04-06T06:45:38Z

Installing

← Older revision		Revision as of 06:45, 6 April 2012
Line 19:		Line 19:
	# Install the MBT for Event-B plugin:		# Install the MBT for Event-B plugin:
	## In the menu choose ''Help'' -> ''Install New Software...''.		## In the menu choose ''Help'' -> ''Install New Software...''.
	### Click ''Add...''.		## Click ''Add...''.
	### As ''Location'' enter ''http://fmi.upit.ro/mbt_plugin''		## As ''Location'' enter ''http://fmi.upit.ro/mbt_plugin''
	### Enter a name e.g. ''MBT for Event-B Plugin''.		## Enter a name e.g. ''MBT for Event-B Plugin''.
	### Click ''Ok''.		## Click ''Ok''.
	# Restart Rodin as suggested.		# Restart Rodin as suggested.

2012-04-04T13:15:15Z

← Older revision		Revision as of 13:15, 4 April 2012
Line 107:		Line 107:
	After building a ''counterexample path'' and clicking ''Next'', the wizard returns to displaying the computed DFCA.		After building a ''counterexample path'' and clicking ''Next'', the wizard returns to displaying the computed DFCA.

			== References ==

			I. Dinca, F. Ipate, L. Mierla, A. Stefanescu. Learn and Test for Event-B - a Rodin Plugin. To appear in Proceedings of ABZ'12, 2012. Online at: http://deploy-eprints.ecs.soton.ac.uk/379/
	== Licensing ==		== Licensing ==

2012-02-24T11:30:39Z

Displaying the generated cover automaton

← Older revision		Revision as of 11:30, 24 February 2012
Line 60:		Line 60:
	==== Displaying the generated cover automaton ====		==== Displaying the generated cover automaton ====

	The second wizard page displays the computed ''cover automaton'' and (if this is the case) the ''timeout paths''. ~~Timeout paths are sequences~~ of events for which it ~~was not possible to decide positively or negatively if the path is executable or not (for some values of the global variables and local parameters)~~.		The second wizard page displays the computed ''cover automaton'' and (if this is the case) the ''timeout paths''. A ''timeout path'' is a sequence of events of length at most <math>l</math>, for which no ''test data'' were found to trigger it within a given time bound.

	In the graphical representation of the automaton, the final states are drawn in double line, whereas non-final states are drawn in single line. The initial state is labeled ''q0'' and the transitions are labeled with event names.		In the graphical representation of the automaton, the final states are drawn in double line, whereas non-final states are drawn in single line. The initial state is labeled ''q0'' and the transitions are labeled with event names.

	~~A ''timeout path'' is a sequence of events of length at most <math>l</math>, for which no ''test data'' were found to trigger it.~~

	[[Image:MBT_for_Event-B_Screenshot__-3.png]]		[[Image:MBT_for_Event-B_Screenshot__-3.png]]

2012-02-24T11:29:04Z

Displaying the generated cover automaton

← Older revision		Revision as of 11:29, 24 February 2012
Line 60:		Line 60:
	==== Displaying the generated cover automaton ====		==== Displaying the generated cover automaton ====

	The second wizard page displays the computed ''cover automaton'' and ~~eventually~~ the ''timeout paths''.		The second wizard page displays the computed ''cover automaton'' and (if this is the case) the ''timeout paths''. Timeout paths are sequences of events for which it was not possible to decide positively or negatively if the path is executable or not (for some values of the global variables and local parameters).

	In the graphical representation of the automaton, the final states are drawn in double line, whereas non-final states are drawn in single line. The initial state is labeled ''q0'' and the transitions are labeled with event names.		In the graphical representation of the automaton, the final states are drawn in double line, whereas non-final states are drawn in single line. The initial state is labeled ''q0'' and the transitions are labeled with event names.
Line 73:		Line 73:
	* displaying the generated ''test suite''		* displaying the generated ''test suite''
	* providing a ''counterexample path''		* providing a ''counterexample path''


	==== Displaying the generated test suite ====		==== Displaying the generated test suite ====

2012-02-24T11:25:46Z

Short theoretical aspects

← Older revision		Revision as of 11:25, 24 February 2012
Line 41:		Line 41:
	The ''state model'' is constructed in a gradual manner, permitting the integration of the Event-B refinement in this process.		The ''state model'' is constructed in a gradual manner, permitting the integration of the Event-B refinement in this process.

	Whenever the generated ''cover automaton'' is found inaccurate, a ''counterexample path (a collection/sequence of events)'' must be provided and the ''Learn DFCA'' algorithm must be executed.		Whenever the generated ''cover automaton'' is found inaccurate, a ''counterexample path (a collection/sequence of events)'' must be provided and the ''Learn DFCA'' algorithm must be re-executed.

	=== Starting the plugin ===		=== Starting the plugin ===

2012-02-24T11:25:01Z

← Older revision		Revision as of 11:25, 24 February 2012
Line 10:		Line 10:

	The MBT for Event-B plugin (also referred to as MBT plugin) relies on Rodin release 2.0 or newer and ProB plugin 2.2 or newer.		The MBT for Event-B plugin (also referred to as MBT plugin) relies on Rodin release 2.0 or newer and ProB plugin 2.2 or newer.
	The following steps ~~will~~ guide you through the installation process:		The following steps guide you through the installation process:

	# Download the latest Rodin release for your platform from [http://sourceforge.net/projects/rodin-b-sharp/files/Core_%20Rodin%20Platform/ Sourceforge].		# Download the latest Rodin release for your platform from [http://sourceforge.net/projects/rodin-b-sharp/files/Core_%20Rodin%20Platform/ Sourceforge].

2011-07-10T20:36:55Z

Disclaimer

2011-07-10T20:36:08Z

Short theoretical aspects

← Older revision		Revision as of 20:36, 10 July 2011
Line 39:		Line 39:
	The ''execution of a test case'' implies the existence of appropriate test data for the events, i.e. appropriate values for the event parameters in order to ensure that the corresponding guard is true. By definition, a ''test suite'' is a collection of ''test cases''.		The ''execution of a test case'' implies the existence of appropriate test data for the events, i.e. appropriate values for the event parameters in order to ensure that the corresponding guard is true. By definition, a ''test suite'' is a collection of ''test cases''.

	The ''state model'' is constructed in a gradual manner, permitting the integration of the ~~[http://en.wikipedia.org/wiki/Program_refinement~~ refinement] in this process.		The ''state model'' is constructed in a gradual manner, permitting the integration of the Event-B refinement in this process.

	Whenever the generated ''cover automaton'' is found inaccurate, a ''counterexample path (a collection/sequence of events)'' must be provided and the ''Learn DFCA'' algorithm must be executed.		Whenever the generated ''cover automaton'' is found inaccurate, a ''counterexample path (a collection/sequence of events)'' must be provided and the ''Learn DFCA'' algorithm must be executed.

2011-07-09T00:03:43Z

2011-07-08T23:50:15Z

← Older revision		Revision as of 23:50, 8 July 2011
Line 3:		Line 3:
	\|}		\|}

	'''MBT (Model-Based Testing) for Event-B plugin'''		'''MBT (Model-Based Testing) for Event-B plugin'''

			[[Image:MBT_for_Event-B_Logo_Large.png]]

	==Installing ==		==Installing ==