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, adds MBT and SAP experience to the Pitesti team.

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 start 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 algorithm usually traverse the state space starting in an initial state and 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 will provide the test data associated with the test cases.

Given the above considerations, the following choices and decisions have been made:

• First, model-checking algorithms
• constraint solving
• using meta-heuristic search algorithms

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.

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 (based on KodKod). University of Pitesti will experiment with different fitness functions adapted to the concrete coverage requirements requested by the DPs. 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 Bepi Colombo use case).