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

Model-based Testing (MBT) has been proposed to create test cases more efficiently and effectively. In contrast, analysis techniques (e.g., model checking) have been used separately from testing and have shown great potential when applied early in the development process. Still, these are confronted by applicability and scalability issues and work on specific modeling languages. The combined use of MBT and analysis techniques can support engineers in using both dynamic and static techniques. This paper proposes a hybrid approach by combining MBT using GraphWalker (GW) with Model-Based Analysis using UPPAAL by transforming the GW model into UPPAAL timed automata and supporting a combined analysis and testing process. The approach enables the automatic verification of both reachability and deadlock freedom properties to exploit the results obtained from this analysis step to improve the test model before generating and executing test cases on the system under test. The proposed approach can improve the combination of analysis and testing using a promising open-source MBT tool and is currently being evaluated in the context of actual use cases.