Model Based Testing and Model Checking : An Efficient Combination

Abstract

This thesis aims to combine MBT with model analysis to provide an overall frame-work for feedback-based model analysis. We have used an MBT tool, Graph-Walker, and a model checker, UPPAAL, for transformation, feedback, and analy-sis. GW2UPPAAL1is an existing tool that transforms the GraphWalker model intoUPPAAL timed automata and supports a combined analysis and testing process.The tool enables the automatic verification of reachability and deadlocks freedomproperties to exploit the results obtained from this analysis step to improve thetest model before generating and executing test cases on the system under test.However, based on model analysis results, the test engineer must manually cre-ate the new GraphWalker model, which may be time-consuming and error-prone.We have developed a hybrid approach (a.k.a. UPPAAL2GW) to transform theUPPAAL-derived model to GraphWalker to provide automated feedback of themodel checker to the MBT model, which helps the test engineer to use the modi-fied GraphWalker model for test case generation. We have evaluated the overallapproach of the toolchain by seeding mutations into the models created by indus-trial practitioners and verifying whether the tool provides automated feedbackto the test engineer. We have also used Graphviz to reflect changes in the MBTmodels before and after the modifications. Furthermore, we have integrated bothtools for automated analysis and feedback. The integration of GW2UPPAAL andUPPAAL2GW tools bridges the gap between MBT and model checking and en-sures the overall analysis and feedback for MBT test case generation.