Integrating model checking and model based testing for industrial software development

• Published in: Computers in industry 2019-01, Vol.104, p.88-102
• Main Authors: Villani, Emília, Pontes, Rodrigo Pastl, Coracini, Guilherme Kisselofl, Ambrósio, Ana Maria
• Format: Article
• Language: English
• Subjects: Model based design; Model based testing; Model checking; Verification techniques
• ISSN: 0166-3615; 1872-6194
• DOI: 10.1016/j.compind.2018.08.003

•We propose two hybrid processes that integrates model checking and model based testing in the design of industrial systems.•We present CONTEA, a tool for supporting the hybrid processes and evaluate the hybrid processes using three case studies.•The proposed hybrid processes contributes to the early and broader identification of errors. 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.