Three-valued model checking has been proposed to support verification when some portions of the model are unspecified. Given a formal property, the model checker returns true if the property is satisfied, false and a violating behavior if it is not, maybe and a possibly violating behavior if it is possibly satisfied, i.e., its satisfaction may depend on how the unspecified parts are refined. Model checking, however, does not explain the reasons why a property holds, or possibly holds. Theorem proving can instead do it by providing a formal proof that explains why a property holds, or possibly holds in a system. Integration of theorem proving with model checking has only been studied for classical two-valued logic – hence, for fully specified models. This paper proposes a unified approach that enriches three-valued model checking with theorem proving to generate proofs which explain why true and maybe results are returned.

From model checking to a temporal proof for partial models

Spoletini P.;
2017-01-01

Abstract

Three-valued model checking has been proposed to support verification when some portions of the model are unspecified. Given a formal property, the model checker returns true if the property is satisfied, false and a violating behavior if it is not, maybe and a possibly violating behavior if it is possibly satisfied, i.e., its satisfaction may depend on how the unspecified parts are refined. Model checking, however, does not explain the reasons why a property holds, or possibly holds. Theorem proving can instead do it by providing a formal proof that explains why a property holds, or possibly holds in a system. Integration of theorem proving with model checking has only been studied for classical two-valued logic – hence, for fully specified models. This paper proposes a unified approach that enriches three-valued model checking with theorem proving to generate proofs which explain why true and maybe results are returned.
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/11383/2105608
 Attenzione

L'Ateneo sottopone a validazione solo i file PDF allegati

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 18
  • ???jsp.display-item.citation.isi??? ND
social impact