D45 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). In DEPLOY, we investigated a version of MBT using Event-B models as test models from which test cases are generated. The main purpose was 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.

The partners involved in MBT for Event-B were University of Pitesti and University of Dusseldorf on the academic side and SAP on the deployment partners side.

In the last year of DEPLOY, the work done on MBT proceeded according to the plan (summarized in the previous deliverable D32), i.e. generating test cases and test data using constraint-solving and evolutionary techniques. Moreover, new ideas involving a technique called "automata learning" were investigated. The proposed methods were implemented, a new Rodin plugin was publicly released, and experiments were performed using the Event-B models available in the DEPLOY model repositories.

Motivations

MBT is a very active research area using several types of test models and delivering promising results. Before our investigations, the Event-B approach and framework did not support MBT, even though the MBT prerequisites were satisfied. Moreover, deployment partners such as SAP, showed interest into MBT as a good candidate for adoption of formal methods in practice. A first attempt to MBT was based on the model-checking and state exploration capabilities of the ProB plugin, by exploring the explicit state of an Event-B model and outputting event sequences as test cases. However, the attempt worked only for small domains of the variables and faced the classical state space explosion problem for larger domains. This motivated the search for alternative solutions as presented below.

Choices / Decisions

In the reporting period, the following three different approaches were defined, implemented, and tested: Using abstraction and Constraint-solving: ... Using search-based: ... Using model-learning: ...

Furthermore, the output of the above procedures was complemented by the test suite optimisations according to different test coverage criteria. This was motivated by ...

Available Documentation

MBT plug-in wiki page: http://wiki.event-b.org/index.php/MBT_plugin

Associated deliverables containing technical information on the MBT work:

• DEPLOY deliverable D44 - see chapter 10 for technical details
• DEPLOY deliverable D54
• DEPLOY deliverable D32 - see chapter 10 for backward reference

Papers:

• Ionut Dinca, Alin Stefanescu, Florentin Ipate, Raluca Lefticaru, and Cristina Tudose. Test data generation for Event-B models using genetic algorithms. In Proc. of 2nd International Conference on Software Engineering and Computer Systems (ICSECS’11), volume 181 of CCIS, pages 76–90. Springer, 2011.
• Alin Stefanescu, Florentin Ipate, Raluca Lefticaru, and Cristina Tudose. Towards search-based testing for Event-B models. In Proc. of 4th Workshop on Search-Based Software Testing (SBST’11), pages 194–197. IEEE, 2011.

Ionut Dinca. Multi-objective test suite optimization for Event-B models. In Proc. of Int. Conf. on Informatics Engineering and Information Science (ICIEIS’11), volume 251 of CCIS series (Communications in Computer and Information Science), pages 551–565. Springer, 2011. Florentin Ipate, Ionut Dinca, and Alin Stefanescu. Model learning and test generation using cover automata. Submitted to IEEE Transactions on Software Engineering, January 2012. Ionut Dinca, Florentin Ipate, Laurentiu Mierla, and Alin Stefanescu. Learn and test for Event-B - a Rodin plugin. Submitted to ABZ'12, 2012.

TODO Update the references in April 2012

Status

TODO To be completed.