Conformance Testing in UPPAAL: A diabolic approach

Model-based mutation testing is a fault-based method in the model-based testing area of research. It has been applied to several modeling formalisms, including timed automata. We propose a model transformation termed 'diabolic completion' that allows for conformance testing directly in the UPPAAL tool. We have also developed a system to automate most of the process, which include taking a model, and performing diabolic completion, with the additions of allowing creation of mutants, conformance checking using the UPPAAL verification engine, and test case generation. We then set up a case study using a car alarm system model, which has been used several times in this area of research, and compare the efficiency with two existing tools, Ecdar 2.2 and MoMuT::TA, observing a significant speedup.