We present a technique for checking the equivalence of NuSMV specifications. The approach is founded on the notion of equivalence between Kripke structures. The necessity to tackle this problem arisen working on using mutation to asses the static analysis fault detection capability. Indeed, mutation, consisting into introducing simple syntactic changes -- representing typical mistakes designers often make -- into specifications, may produce equivalent mutants, namely models behaving as the original one. Equivalent mutants should be detected since they do not represent actual faults. In program mutation, detecting equivalent mutants is an undecidable problem and, when possible, is a time-consuming activity, difficult to automatize. In this work we focus on how detecting equivalence of NuSMV specifications. The novel technique we propose, consists in building a merging unique specification and proving by model checking a series of CTL properties.
Equivalence checking of NuSMV specifications / P. Arcaini, A. Gargantini, E. Riccobene. - Milano : Università degli Studi di Milano, 2011 Nov.
Equivalence checking of NuSMV specifications
P. ArcainiPrimo
;E. RiccobeneUltimo
2011
Abstract
We present a technique for checking the equivalence of NuSMV specifications. The approach is founded on the notion of equivalence between Kripke structures. The necessity to tackle this problem arisen working on using mutation to asses the static analysis fault detection capability. Indeed, mutation, consisting into introducing simple syntactic changes -- representing typical mistakes designers often make -- into specifications, may produce equivalent mutants, namely models behaving as the original one. Equivalent mutants should be detected since they do not represent actual faults. In program mutation, detecting equivalent mutants is an undecidable problem and, when possible, is a time-consuming activity, difficult to automatize. In this work we focus on how detecting equivalence of NuSMV specifications. The novel technique we propose, consists in building a merging unique specification and proving by model checking a series of CTL properties.File | Dimensione | Formato | |
---|---|---|---|
technicalReport.pdf
accesso aperto
Tipologia:
Pre-print (manoscritto inviato all'editore)
Dimensione
351.1 kB
Formato
Adobe PDF
|
351.1 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.