Abstract
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.
[read the copyright and download the pdf file] [DOI]