Vacuum cleaning is a mandatory process when an implementation is verified with respect to a specification modeled by means of formal properties. In fact, vacuum cleaning looks for properties that, passing vacuously (e.g., an implication whose antecedent is always false), may lead verification engineers to a false sense of safety. Current approaches to vacuum cleaning, generally, exploit formal methods to provide an interesting witness proving that a property does not pass vacuously. However, such approaches are as complex as model checking, and they require to define and model check further properties, thus increasing the verification time. This paper proposes an alternative approach, based on fault simulation, that requires neither the definition of new properties, nor the use of model checking. Experimental results show the high efficiency of this approach.

Vacuity Analysis by Fault Simulation

DI GUGLIELMO, Luigi;FUMMI, Franco;PRAVADELLI, Graziano
2008-01-01

Abstract

Vacuum cleaning is a mandatory process when an implementation is verified with respect to a specification modeled by means of formal properties. In fact, vacuum cleaning looks for properties that, passing vacuously (e.g., an implication whose antecedent is always false), may lead verification engineers to a false sense of safety. Current approaches to vacuum cleaning, generally, exploit formal methods to provide an interesting witness proving that a property does not pass vacuously. However, such approaches are as complex as model checking, and they require to define and model check further properties, thus increasing the verification time. This paper proposes an alternative approach, based on fault simulation, that requires neither the definition of new properties, nor the use of model checking. Experimental results show the high efficiency of this approach.
2008
9781424424177
vacuity analysis; Fault simulation
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11562/323061
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 2
  • ???jsp.display-item.citation.isi??? 1
social impact