Using mutation to assess fault detection capability of model review

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.