Using mutation to assess fault detection capability of model review. (25th April 2014)

• Record Type: Journal Article
• Authors: Arcaini, Paolo; Gargantini, Angelo; Riccobene, Elvinia
• Other Names: Jia Yue guestEditor.; Merayo Mercedes guestEditor.; Harman Mark guestEditor.
• Is Part Of: Software testing, verification & reliability. Volume 25:Number 5/7(2015)
• Page Start: 629
• Page End: 652
• Publication Date: 2014-04-25
• Subjects: mutation analysis -- model review -- fault detection capability -- NuSMV -- equivalent mutants; Computer software -- Testing -- Periodicals; Computer software -- Verification -- Periodicals; Computer software -- Reliability -- Periodicals; 005.14
• DOI: 10.1002/stvr.1530
• Languages: English
• ISSNs: 0960-0833

Abstract

Summary: Among validation techniques, model review is a static analysis approach that can be performed at the early stages of software development, at the specification level, and aims at determining if a model owns certain quality attributes (like completeness, consistency and minimality). However, the model review capability to detect behavioural faults has never been measured. In this paper, a methodology and a supporting tool for evaluating the fault detection capability of a NuSMV model advisor are presented, which performs an automatic static model review of NuSMV models. The approach is based on the use of mutation in a similar way as in mutation testing: several mutation operators for NuSMV models are defined, and the model advisor is used to detect behavioural faults by statically analysing mutated specifications. In this way, it is possible to measure the model advisor ability to discover faults. To improve the quality of the analysis, the equivalence between a NuSMV model and any of its mutants must be checked. To perform this task, this paper proposes a technique based on the concept of equivalent Kripke structures, as NuSMV models are Kripke structures. A number of experiments assess the fault‐detecting capability, precision and accuracy of the proposed approach. Analysis of variance is used to check if the results are statistically significant. Some relationships among mutation operators and model quality attributes are also established. Copyright © 2014 John Wiley & Sons, Ltd. Abstract : Model review is a static analysis approach that aims at determining if a model owns certain quality attributes. This paper presents a methodology for evaluating the fault detection capability of the NuSMV model advisor. The approach is based on the use of mutation analysis; to improve the quality of the analysis, the equivalence between a NuSMV model and any of its mutants is checked. Some experiments assess the fault detecting capability, precision, and accuracy of the NuSMV model advisor. Copyright©2014 John Wiley & Sons, Ltd.