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.

WP1-4 partners, 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. [TODO: add more concrete requirements and industrial settings]

Choices/Decisions

[TODO]

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

Available Documentation

[TODO] Previous work:

• ProTest paper: <Satpathy, M., Leuschel, M., Butler, M.: ProTest: An Automatic Test Environment for B Specifications, In: Proc. ENTCS 111, 113-136, 2005>
• SAP-UniDue paper: ...
• Florentin & Raluca: ...
• SAP MBT paper ...

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 tha mBT tool by integrating of a constraint solver (KodKod). University of Pitesti will experiment with different fitness functions adapted to the concrete coverage requirements requested by the DP. [TO FINISH]