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.
Using mutation to assess fault detection capability of model review / P. Arcaini, A. Gargantini, E. Riccobene. - In: SOFTWARE TESTING VERIFICATION & RELIABILITY. - ISSN 0960-0833. - 25:5-7(2015), pp. 629-652. [10.1002/stvr.1530]
Using mutation to assess fault detection capability of model review
E. RiccobeneUltimo
2015
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.File | Dimensione | Formato | |
---|---|---|---|
Arcaini_et_al-2015-Software_Testing,_Verification_and_Reliability.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
896.28 kB
Formato
Adobe PDF
|
896.28 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.