Integrating model checking and model based testing for industrial software development

With the purpose of making the use of model based techniques in industrial software development more efficient, this work proposes the combined application of two verification techniques: model checking with UPPAAL and CoFI (Conformance and Fault Injection) model based testing with ConData. This combination is supported by ConTEA, a software tool for automatically connecting UPPAAL to ConData, and, therefore, explore both techniques simultaneously. We present the tool and discuss the use of ConTEA in two different development processes. The first process investigates how CoFI can contribute to identify gaps in the specification and implicit assumptions made by engineers when applying model checking. The second process focuses on how model checking can improve the development and verification of the models that are used for model based testing. The proposed processes were applied to three case studies. Based on them, we compare the proposed processes to the traditional CoFI and UPPAAL stand-alone processes. The results indicate that the combined use of the two verification technique contributes to the identification of a large range of diversified errors and problems early in the development cycle.