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, i.e. basis for test generation. The main purpose of MBT track in DEPLOY 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.

TODO An overview of the work done about Model-based testing. In the last year of DEPLOY, the work done on MBT proceeded according to the plan (the plan was summarized in the previous similar deliverable D32). Moreover, new ideas involving a technique called "automata learning" was investigated. All the theoretical methods were implemented, released as a public Rodin plugin, and tested on the Event-B models available in the DEPLOY model repositories.

Motivations

TODO To be completed.

Choices / Decisions

TODO To be completed.

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:
• DEPLOY deliverable D54:
• DEPLOY deliverable D32: for reference

Papers

• 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 reference in April

• 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, pages 551–565. Springer, 2011.

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

• Florentin Ipate, Ionut Dinca, and Alin Stefanescu. Model learning and

test generation using cover automata. Submitted to IEEE Transactions on Software Engineering, January 2012.

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

• Sebastian Wieczorek, Alin Stefanescu, and Matthias Schur. Message

choreography modeling - a domain-specific language for consistent enterprise service integration. Submitted to Software and Systems Modeling (SoSyM) journal, 2011. TODO Update the reference in April

Status

TODO To be completed.