D32 Model-based testing - Revision history

imported>Tommy at 15:14, 27 January 2011

2011-01-27T15:14:37Z

← Older revision		Revision as of 15:14, 27 January 2011
Line 36:		Line 36:
	= Planning =		= Planning =

	In the fourth year of the project, the work on MBT will continue in a sustained pace in order to support the work of the deployment partners. SAP for instance has MBT as one of its main focus deployment area in the last year of the project. The tool provider Duesseldorf will continue to improve the MBT tooling by improving its constraint solver to solve the state space explosion problem. University of Pitesti will experiment with different fitness functions adapted to the concrete coverage requirements requested by the DPs. Such approaches proved to work good for numerical problems, but need adaptations to also be fully applied to data domains using sets. Finally, the tool providers may investigate the MBT requirements of SSF use case (i.e., how feasible is it to generate test cases from the Event-B models for their Bepi Colombo use case?).		In the fourth year of the project, the work on MBT will continue in a sustained pace in order to support the work of the deployment partners. SAP for instance has MBT as one of its main focus deployment area in the last year of the project. The tool provider Duesseldorf will continue to improve the MBT tooling by improving its constraint solver to solve the state space explosion problem. University of Pitesti will experiment with different fitness functions adapted to the concrete coverage requirements requested by the DPs. Such approaches proved to work good for numerical problems, but need adaptations to also be fully applied to data domains using sets. Finally, the tool providers may investigate the MBT requirements of SSF use case (i.e., how feasible is it to generate test cases from the Event-B models for their Bepi Colombo use case?).

			== References ==
			<references/>

	[[Category:D32 Deliverable]]		[[Category:D32 Deliverable]]

imported>Tommy at 15:13, 27 January 2011

2011-01-27T15:13:47Z

← Older revision		Revision as of 15:13, 27 January 2011
Line 21:		Line 21:
	Given the above considerations, the following choices and decisions have been made:		Given the above considerations, the following choices and decisions have been made:
	* Using explicit model-checking: First, model-checking algorithms described in the previous paragraph were implemented and applied to message choreography models from SAP. They work fine for models with data with a small finite range. However, in case of variables with a large range (e.g. integers), the known state space explosion problem creates difficulties, since the model-checker explores the state enumerating the many possible values of the variables. This required to consider different approaches as described below.		* Using explicit model-checking: First, model-checking algorithms described in the previous paragraph were implemented and applied to message choreography models from SAP. They work fine for models with data with a small finite range. However, in case of variables with a large range (e.g. integers), the known state space explosion problem creates difficulties, since the model-checker explores the state enumerating the many possible values of the variables. This required to consider different approaches as described below.
	* Using constraint solving: To avoid the state space explosion due to the large bounds of the variables, another approach ignores these values in the first step and uses the model-checker only to generate abstract test cases satisfying the coverage criteria. However, these paths may be infeasible in the concrete model due to the data constraints along the path. The solution is to represent the intermediate states of the path as existentially quantified variables. The whole path is then represented as a single predicate consisting of the guards and before-after predicates of its events. ProB's improved constraint solver (see ~~[[D32_Model_Animation\|~~Model Animation]]) is then used to validate the path feasibility and find appropriate data satisfying the constraints.		* Using constraint solving: To avoid the state space explosion due to the large bounds of the variables, another approach ignores these values in the first step and uses the model-checker only to generate abstract test cases satisfying the coverage criteria. However, these paths may be infeasible in the concrete model due to the data constraints along the path. The solution is to represent the intermediate states of the path as existentially quantified variables. The whole path is then represented as a single predicate consisting of the guards and before-after predicates of its events. ProB's improved constraint solver (see Model Animation<ref>http://wiki.event-b.org/index.php/D32_Model_Animation</ref>) is then used to validate the path feasibility and find appropriate data satisfying the constraints.
	* Using meta-heuristic search algorithms: As an alternative to the above constraint solving approach, we investigated also a recent approach to test data generation using meta-heuristic search algorithms (e.g. evolutionary and genetic algorithms). The idea is to solve the test data problem by starting with an initial set of data and improving it using guidance from the constraints to be satisfied (using certain fitness functions that describe "how far" is the current data from a solution). Meta-heuristic search algorithms can be applied not only to the test data generation for one path but also to obtain a set of test cases with the required coverage.		* Using meta-heuristic search algorithms: As an alternative to the above constraint solving approach, we investigated also a recent approach to test data generation using meta-heuristic search algorithms (e.g. evolutionary and genetic algorithms). The idea is to solve the test data problem by starting with an initial set of data and improving it using guidance from the constraints to be satisfied (using certain fitness functions that describe "how far" is the current data from a solution). Meta-heuristic search algorithms can be applied not only to the test data generation for one path but also to obtain a set of test cases with the required coverage.

imported>Tommy: /* Planning */

2011-01-27T13:38:06Z

Planning

← Older revision		Revision as of 13:38, 27 January 2011
Line 36:		Line 36:
	= Planning =		= Planning =

	In the fourth year of the project, the work on MBT will continue in a sustained pace in order to support the work of the deployment partners. SAP for instance has MBT as one of its main focus deployment area in the last year of the project. The tool provider Duesseldorf will continue to improve the MBT tooling by improving its constraint solver to solve the state space explosion problem. University of Pitesti will experiment with different fitness functions adapted to the concrete coverage requirements requested by the DPs. Such approaches proved to work good for numerical problems, but need adaptations to also be fully applied to data domains using sets. Finally, the tool providers may investigate the MBT requirements of SSF use case (i.e., how feasible is to generate test cases from the Event-B models for their Bepi Colombo use case).		In the fourth year of the project, the work on MBT will continue in a sustained pace in order to support the work of the deployment partners. SAP for instance has MBT as one of its main focus deployment area in the last year of the project. The tool provider Duesseldorf will continue to improve the MBT tooling by improving its constraint solver to solve the state space explosion problem. University of Pitesti will experiment with different fitness functions adapted to the concrete coverage requirements requested by the DPs. Such approaches proved to work good for numerical problems, but need adaptations to also be fully applied to data domains using sets. Finally, the tool providers may investigate the MBT requirements of SSF use case (i.e., how feasible is it to generate test cases from the Event-B models for their Bepi Colombo use case?).

	[[Category:D32 Deliverable]]		[[Category:D32 Deliverable]]

imported>Tommy: /* Motivations */

2011-01-27T13:36:24Z

Motivations

← Older revision		Revision as of 13:36, 27 January 2011
Line 9:		Line 9:
	= Motivations =		= Motivations =

	The interest in MBT is ~~given by~~ the opportunity of using the Event-B models not only ~~for formal validation of the specification~~ but also to verify using test cases that an existing implementation behaves as expected. Along with code generation, MBT using Event-B operates at the lower level of the envisaged rigorous engineering chain in DEPLOY ~~that starts~~ from high-level requirements down to software implementations via specification, architecture and refined designs.		The interest in MBT is to get the opportunity, by using the Event-B models, not only to formally validate specifications, but also to verify using test cases, that an existing implementation behaves as expected. Along with code generation, MBT (using Event-B) operates at the lower level of the envisaged rigorous engineering chain. In DEPLOY, this chain goes from high-level requirements down to software implementations via specification, architecture and refined designs.

	Deployment partners (DP), especially SAP (WP4), showed interest into having tool support for MBT. As a consequence, this topic was introduced in the refocus exercise in the middle of the project (M24) and was documented in the updated version DoW signed in August 2010 (see Task 9.10 there). The deployment partner SSF (WP3) had recently also shown interest in the MBT task.		Deployment partners (DP), especially SAP (WP4), showed interest into having tool support for MBT. As a consequence, this topic was introduced in the refocus exercise (in the middle of the project [M24]) and was documented in the updated version DoW signed in August 2010 (see Task 9.10 there). The deployment partner SSF (WP3) had recently also shown interest in the MBT task.

	For the SAP use case, MBT is applied in the area of integration and system testing for service-oriented applications. First, a method for integration testing using SAP's message choreography models was developed using ProB. In the reported period (Feb. 2010 - Jan. 2011), SAP focused on UI system testing using high-level business processes. This required an adaptation of the first MBT approach to the new model types. In these new models, the associated test data constraints played a more prominent position which required also more effort from the tooling point of view.		For the SAP use case, MBT is applied in the area of integration and system testing for service-oriented applications. First, a method for integration testing using SAP's message choreography models was developed using ProB. In the reported period (Feb. 2010 - Jan. 2011), SAP focused on UI system testing using high-level business processes. This required an adaptation of the first MBT approach to the new model types. In these new models, the associated test data constraints played a more prominent position which required also more effort from the tooling point of view.

imported>Alinstef: /* Planning */

2010-11-30T12:43:28Z

Planning

← Older revision		Revision as of 12:43, 30 November 2010
Line 36:		Line 36:
	= Planning =		= Planning =

	In the fourth year of the project, the work on MBT will continue in a sustained pace in order to support the work of the deployment partners. SAP for instance has MBT as one of its main focus deployment area in the last year of the project. The tool provider Duesseldorf will continue to improve the MBT tooling by improving its constraint solver to solve the state space explosion problem. University of Pitesti will experiment with different fitness functions adapted to the concrete coverage requirements requested by the DPs. Such approaches proved to work good for numerical problems, but need adaptations to also be fully applied to data domains using sets. Finally, the tool ~~provides~~ may investigate the MBT requirements of SSF use case (i.e., how feasible is to generate test cases from the Event-B models for their Bepi Colombo use case).		In the fourth year of the project, the work on MBT will continue in a sustained pace in order to support the work of the deployment partners. SAP for instance has MBT as one of its main focus deployment area in the last year of the project. The tool provider Duesseldorf will continue to improve the MBT tooling by improving its constraint solver to solve the state space explosion problem. University of Pitesti will experiment with different fitness functions adapted to the concrete coverage requirements requested by the DPs. Such approaches proved to work good for numerical problems, but need adaptations to also be fully applied to data domains using sets. Finally, the tool providers may investigate the MBT requirements of SSF use case (i.e., how feasible is to generate test cases from the Event-B models for their Bepi Colombo use case).

	[[Category:D32 Deliverable]]		[[Category:D32 Deliverable]]

imported>Alinstef: /* Choices / Decisions */

2010-11-30T12:42:58Z

Choices / Decisions

← Older revision		Revision as of 12:42, 30 November 2010
Line 21:		Line 21:
	Given the above considerations, the following choices and decisions have been made:		Given the above considerations, the following choices and decisions have been made:
	* Using explicit model-checking: First, model-checking algorithms described in the previous paragraph were implemented and applied to message choreography models from SAP. They work fine for models with data with a small finite range. However, in case of variables with a large range (e.g. integers), the known state space explosion problem creates difficulties, since the model-checker explores the state enumerating the many possible values of the variables. This required to consider different approaches as described below.		* Using explicit model-checking: First, model-checking algorithms described in the previous paragraph were implemented and applied to message choreography models from SAP. They work fine for models with data with a small finite range. However, in case of variables with a large range (e.g. integers), the known state space explosion problem creates difficulties, since the model-checker explores the state enumerating the many possible values of the variables. This required to consider different approaches as described below.
	* Using constraint solving: To avoid the state space explosion due to the large bounds of the variables, another approach ignores these values in the first step and uses the model-checker only ~~generating~~ abstract test cases satisfying the coverage criteria. However, these paths may be infeasible in the concrete model due to the data constraints along the path. The solution is to represent the intermediate states of the path as existentially quantified variables. The whole path is then represented as a single predicate consisting of the guards and before-after predicates of its events. ProB's improved constraint solver (see [[D32_Model_Animation\|Model Animation]]) is then used to validate the path feasibility and find appropriate data satisfying the constraints.		* Using constraint solving: To avoid the state space explosion due to the large bounds of the variables, another approach ignores these values in the first step and uses the model-checker only to generate abstract test cases satisfying the coverage criteria. However, these paths may be infeasible in the concrete model due to the data constraints along the path. The solution is to represent the intermediate states of the path as existentially quantified variables. The whole path is then represented as a single predicate consisting of the guards and before-after predicates of its events. ProB's improved constraint solver (see [[D32_Model_Animation\|Model Animation]]) is then used to validate the path feasibility and find appropriate data satisfying the constraints.
	* Using meta-heuristic search algorithms: As an alternative to the above constraint solving approach, we investigated also a recent approach to test data generation using meta-heuristic search algorithms (e.g. evolutionary and genetic algorithms). The idea is to solve the test data problem by starting with an initial set of data and improving it using guidance from the constraints to be satisfied (using certain fitness functions that describe "how far" is the current data from a solution). Meta-heuristic search algorithms can be applied not only to the test data generation for one path but also to obtain a set of test cases with the required coverage.		* Using meta-heuristic search algorithms: As an alternative to the above constraint solving approach, we investigated also a recent approach to test data generation using meta-heuristic search algorithms (e.g. evolutionary and genetic algorithms). The idea is to solve the test data problem by starting with an initial set of data and improving it using guidance from the constraints to be satisfied (using certain fitness functions that describe "how far" is the current data from a solution). Meta-heuristic search algorithms can be applied not only to the test data generation for one path but also to obtain a set of test cases with the required coverage.

imported>Daniel: /* Choices / Decisions */

2010-11-30T11:42:19Z

Choices / Decisions

← Older revision		Revision as of 11:42, 30 November 2010
Line 21:		Line 21:
	Given the above considerations, the following choices and decisions have been made:		Given the above considerations, the following choices and decisions have been made:
	* Using explicit model-checking: First, model-checking algorithms described in the previous paragraph were implemented and applied to message choreography models from SAP. They work fine for models with data with a small finite range. However, in case of variables with a large range (e.g. integers), the known state space explosion problem creates difficulties, since the model-checker explores the state enumerating the many possible values of the variables. This required to consider different approaches as described below.		* Using explicit model-checking: First, model-checking algorithms described in the previous paragraph were implemented and applied to message choreography models from SAP. They work fine for models with data with a small finite range. However, in case of variables with a large range (e.g. integers), the known state space explosion problem creates difficulties, since the model-checker explores the state enumerating the many possible values of the variables. This required to consider different approaches as described below.
	* Using constraint solving: To avoid the state space explosion due to the large bounds of the variables, another approach ignores these values in the first step and uses the model-checker only generating abstract test cases satisfying the coverage criteria. However, these paths may be infeasible in the concrete model due to the data constraints along the path. The solution is to represent the intermediate states of the path as existentially quantified variables. The whole		* Using constraint solving: To avoid the state space explosion due to the large bounds of the variables, another approach ignores these values in the first step and uses the model-checker only generating abstract test cases satisfying the coverage criteria. However, these paths may be infeasible in the concrete model due to the data constraints along the path. The solution is to represent the intermediate states of the path as existentially quantified variables. The whole path is then represented as a single predicate consisting of the guards and before-after predicates of its events. ProB's improved constraint solver (see [[D32_Model_Animation\|Model Animation]]) is then used to validate the path feasibility and find appropriate data satisfying the constraints.
	path is then represented as a single predicate consisting of the guards and before-after predicates of its events.
	ProB's improved constraint solver (see ~~...~~) is then ~~able~~ to validate the path feasibility and find appropriate data satisfying the constraints.
	* Using meta-heuristic search algorithms: As an alternative to the above constraint solving approach, we investigated also a recent approach to test data generation using meta-heuristic search algorithms (e.g. evolutionary and genetic algorithms). The idea is to solve the test data problem by starting with an initial set of data and improving it using guidance from the constraints to be satisfied (using certain fitness functions that describe "how far" is the current data from a solution). Meta-heuristic search algorithms can be applied not only to the test data generation for one path but also to obtain a set of test cases with the required coverage.		* Using meta-heuristic search algorithms: As an alternative to the above constraint solving approach, we investigated also a recent approach to test data generation using meta-heuristic search algorithms (e.g. evolutionary and genetic algorithms). The idea is to solve the test data problem by starting with an initial set of data and improving it using guidance from the constraints to be satisfied (using certain fitness functions that describe "how far" is the current data from a solution). Meta-heuristic search algorithms can be applied not only to the test data generation for one path but also to obtain a set of test cases with the required coverage.

imported>Daniel: /* Choices / Decisions */

2010-11-30T11:36:32Z

Choices / Decisions

← Older revision		Revision as of 11:36, 30 November 2010
Line 21:		Line 21:
	Given the above considerations, the following choices and decisions have been made:		Given the above considerations, the following choices and decisions have been made:
	* Using explicit model-checking: First, model-checking algorithms described in the previous paragraph were implemented and applied to message choreography models from SAP. They work fine for models with data with a small finite range. However, in case of variables with a large range (e.g. integers), the known state space explosion problem creates difficulties, since the model-checker explores the state enumerating the many possible values of the variables. This required to consider different approaches as described below.		* Using explicit model-checking: First, model-checking algorithms described in the previous paragraph were implemented and applied to message choreography models from SAP. They work fine for models with data with a small finite range. However, in case of variables with a large range (e.g. integers), the known state space explosion problem creates difficulties, since the model-checker explores the state enumerating the many possible values of the variables. This required to consider different approaches as described below.
	* Using constraint solving: To avoid the state space explosion due to the large bounds of the variables, another approach ignores these values in the first step and uses the model-checker only generating abstract test cases satisfying the coverage criteria. However, these paths may be infeasible in the concrete model due to the data constraints along the path.		* Using constraint solving: To avoid the state space explosion due to the large bounds of the variables, another approach ignores these values in the first step and uses the model-checker only generating abstract test cases satisfying the coverage criteria. However, these paths may be infeasible in the concrete model due to the data constraints along the path. The solution is to represent the intermediate states of the path as existentially quantified variables. The whole
	The solution is to represent the intermediate states of the path as existentially quantified variables. The whole
	path is then represented as a single predicate consisting of the guards and before-after predicates of its events.		path is then represented as a single predicate consisting of the guards and before-after predicates of its events.
	ProB's improved constraint solver (see ...) is then able to validate the path feasibility and find appropriate data satisfying the constraints.		ProB's improved constraint solver (see ...) is then able to validate the path feasibility and find appropriate data satisfying the constraints.

imported>Daniel: /* Choices / Decisions */

2010-11-30T10:45:51Z

Choices / Decisions

← Older revision		Revision as of 10:45, 30 November 2010
Line 21:		Line 21:
	Given the above considerations, the following choices and decisions have been made:		Given the above considerations, the following choices and decisions have been made:
	* Using explicit model-checking: First, model-checking algorithms described in the previous paragraph were implemented and applied to message choreography models from SAP. They work fine for models with data with a small finite range. However, in case of variables with a large range (e.g. integers), the known state space explosion problem creates difficulties, since the model-checker explores the state enumerating the many possible values of the variables. This required to consider different approaches as described below.		* Using explicit model-checking: First, model-checking algorithms described in the previous paragraph were implemented and applied to message choreography models from SAP. They work fine for models with data with a small finite range. However, in case of variables with a large range (e.g. integers), the known state space explosion problem creates difficulties, since the model-checker explores the state enumerating the many possible values of the variables. This required to consider different approaches as described below.
	* Using constraint solving: To avoid the state space explosion due to the large bounds of the variables, another approach ignores these values in the first step and uses the model-checker only generating abstract test cases satisfying the coverage criteria. However, these paths may be infeasible due to the data constraints along the path. The solution is to ~~use~~ the constraint solver ~~feature of ProB tool in order~~ to validate the path feasibility and find appropriate data satisfying the constraints.		* Using constraint solving: To avoid the state space explosion due to the large bounds of the variables, another approach ignores these values in the first step and uses the model-checker only generating abstract test cases satisfying the coverage criteria. However, these paths may be infeasible in the concrete model due to the data constraints along the path.
			The solution is to represent the intermediate states of the path as existentially quantified variables. The whole
			path is then represented as a single predicate consisting of the guards and before-after predicates of its events.
			ProB's improved constraint solver (see ...) is then able to validate the path feasibility and find appropriate data satisfying the constraints.
	* Using meta-heuristic search algorithms: As an alternative to the above constraint solving approach, we investigated also a recent approach to test data generation using meta-heuristic search algorithms (e.g. evolutionary and genetic algorithms). The idea is to solve the test data problem by starting with an initial set of data and improving it using guidance from the constraints to be satisfied (using certain fitness functions that describe "how far" is the current data from a solution). Meta-heuristic search algorithms can be applied not only to the test data generation for one path but also to obtain a set of test cases with the required coverage.		* Using meta-heuristic search algorithms: As an alternative to the above constraint solving approach, we investigated also a recent approach to test data generation using meta-heuristic search algorithms (e.g. evolutionary and genetic algorithms). The idea is to solve the test data problem by starting with an initial set of data and improving it using guidance from the constraints to be satisfied (using certain fitness functions that describe "how far" is the current data from a solution). Meta-heuristic search algorithms can be applied not only to the test data generation for one path but also to obtain a set of test cases with the required coverage.

imported>Alinstef: /* Planning */

2010-11-29T09:21:12Z

Planning

← Older revision		Revision as of 09:21, 29 November 2010
Line 36:		Line 36:
	= Planning =		= Planning =

	In the fourth year of the project, the work on MBT will continue in a sustained pace in order to support the work of the deployment partners. SAP for instance has MBT as one of its main focus deployment area in the last year of the project. The tool provider Duesseldorf will continue to improve the MBT tooling by improving its constraint solver to solve the state space explosion problem. University of Pitesti will experiment with different fitness functions adapted to the concrete coverage requirements requested by the DPs. Such approaches proved to work good for numerical problems, but need adaptations to also be fully applied to data domains using sets. Finally, the tool provides may investigate the MBT requirements of SSF use case (i.e., how feasible is to generate test cases from the Event-B models for ~~theirbBepi~~ Colombo use case).		In the fourth year of the project, the work on MBT will continue in a sustained pace in order to support the work of the deployment partners. SAP for instance has MBT as one of its main focus deployment area in the last year of the project. The tool provider Duesseldorf will continue to improve the MBT tooling by improving its constraint solver to solve the state space explosion problem. University of Pitesti will experiment with different fitness functions adapted to the concrete coverage requirements requested by the DPs. Such approaches proved to work good for numerical problems, but need adaptations to also be fully applied to data domains using sets. Finally, the tool provides may investigate the MBT requirements of SSF use case (i.e., how feasible is to generate test cases from the Event-B models for their Bepi Colombo use case).

	[[Category:D32 Deliverable]]		[[Category:D32 Deliverable]]