Combining Model Based Testing and Automated Analysis of Behavioural Models using GraphWalker and UPPAAL

Abstract

Software testing is continuously evolving and Model-based testing (MBT) is one such test automation strategy. MBT involves the generation of tests by executing a model created by studying the requirements of the System under test (SUT). Traversing different paths of the model generates different test cases which can be executed using an MBT tool. There are several commercial and open-source tools available for MBT and model checking. GraphWalker (GW)1 is an MBT tool but it does not perform efficient model checking. So, we use state-of-the-art model checking tool UPPAAL2, which is an integrated tool environment that allows developing models as a network of timed automata. It has a very powerful model verifier through which we can generate properties to verify the model against the expected system behaviour. In this thesis, we try to bridge the gap between MBT and model checking by providing a solution for combining GW with Model-Based Analysis using UPPAAL by transforming the GW model into UPPAAL timed automata and supporting a combined analysis and testing process. Our solution also enables the automatic verification of both reachability and deadlock freedom properties to exploit the results obtained from this analysis step for improving the test model before generating and executing test cases on the system-under-test. We developed a tool called GW2UPPAAL, to improve the combination of analysis and testing using MBT and is currently being evaluated in the context of real use cases. We found that the transformation of the model from GraphWalker to UPPAAL is applicable for several models available in the GraphWalker documentation as well as models created by industrial practitioners. Also, the average time taken to generate and execute the model using GW2UPPAAL is negligible in comparison to a manual approach.