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

A. Bernasconi;C. Ghezzi
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.
2017
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
9783319661964
9783319661971
Formal methods,Software engineering,Theorem proving,Formal proofs,Three-valued models,Two-valued logic,Model checking
File in questo prodotto:
File Dimensione Formato  
paper_30.pdf

accesso aperto

Descrizione: Articolo principale
: Post-Print (DRAFT o Author’s Accepted Manuscript-AAM)
Dimensione 556.45 kB
Formato Adobe PDF
556.45 kB Adobe PDF Visualizza/Apri

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/11311/1076519
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 17
  • ???jsp.display-item.citation.isi??? ND
social impact