D32 Model-based testing

Overview

Model-based testing (MBT) is an approach from software engineering that uses formal models as basis for automatic generation of test cases. A test case is defined as a sequence of actions (or events, or triggers) together with corresponding test data that can be executed against a System Under Test (SUT). There are different types of test models that can be used for MBT, many of them being state-based models (e.g. UML state diagrams). In DEPLOY, we investigate a version of MBT using Event-B models as test models. This research work provides a new feature in the Rodin platform, complementing the existing theorem proving and model-checking capabilities.

The main purpose of MBT track in DEPLOY is to provide the deployment partners an MBT method together with a Rodin plug-in that allows generation of test cases satisfying different coverage criteria (e.g. covering of all events in a model or covering paths to a set of target global states). This includes the generation of appropriate test data that satisfies the guards of the single test steps.

University of Duesseldorf (Michael Leuschel, Daniel Plagge, Jens Bendisposto) started developing first tool support for MBT for Event-B in 2009 and continuously improved the prototype based on the feedback from SAP, the main deployment partner interested in MBT. Starting with June 2010, the team of University of Pitesti (led by Florentin Ipate) joined the DEPLOY consortium when DEPLOY-Enlarged-EU officially begun. Moreover, Alin Stefanescu, who moved from the SAP team to Pitesti team in September 2010, added MBT and SAP experience to the Pitesti team.

Motivations

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.

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.

Choices / Decisions

For MBT using state-based models, test generation algorithms usually traverse the state space starting in an initial state and being guided by a certain coverage criteria (e.g. state coverage) collecting the execution paths in a test suite. Event-B models do not have an explicit state space, but its state space is given by value of the variables and the state is changed by the execution of events that are enabled in that state. ProB tool has a good grip of the state space, being able to explore it, visualize it, and verify various properties using model checking algorithms. Such model checking algorithms can be used to explore the state space of Event-B models using certain coverage criteria (e.g. event coverage) and thus generating test cases along the traversal. Moreover, the input data that allows to trigger the different events provides the test data associated with the test cases.

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 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) 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.

Available Documentation

Papers describing previous work:

• M. Satpathy, M. Butler, M. Leuschel, S. Ramesh. Automatic Testing from Formal Specifications. In Proc. of TAP'07, pp. 95-113, LNCS 4454, Springer, 2007.
• S. Wieczorek, V. Kozyura, A. Roth, M. Leuschel, J. Bendisposto, D. Plagge, I. Schieferdecker. Applying Model Checking to Generate Model-Based Integration Tests from Choreography Models. In Proc. of TestCom/FATES 2009, pp. 179-194, IEEE Computer Society, 2009.
• R. Lefticaru, F. Ipate. Functional Search-based Testing from State Machines. In Proc. of ICST 2008, pp. 525-528, IEEE Computer Society, 2008.
• S. Wieczorek, A. Stefanescu. Improving Testing of Enterprise Systems by Model-Based Testing on Graphical User Interfaces. In Proc. of the Satellite Workshops of ECBS'10. pp. 352-357, IEEE Computer Society, 2010.

See also: DEPLOY Deliverable D53 (August 2010).

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?).