RE.PUBLIC@POLIMI Research Publications at Politecnico di Milano
Re.Public@Polimi, archivio istituzionale dei prodotti della ricerca, è il punto di raccolta, conservazione e disseminazione della produzione scientifica del Politecnico di Milano
E' basato su IRIS, il nuovo sistema di gestione dei dati della ricerca (persone, progetti, pubblicazioni, attività) adottato dall’ateneo
EnglishThree-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.
| Titolo: | From model checking to a temporal proof for partial models |
| Autori: | |
| Data di pubblicazione: | 2017 |
| Serie: | |
| Handle: | http://hdl.handle.net/11311/1076519 |
| ISBN: | 9783319661964 9783319661971 |
| Appare nelle tipologie: | 04.1 Contributo in Atti di convegno |
File in questo prodotto:
| File | Descrizione | Tipologia | Licenza | |
|---|---|---|---|---|
| paper_30.pdf | Articolo principale | Post-Print (DRAFT o Author’s Accepted Manuscript-AAM) | Accesso apertoVisualizza/Apri |
Copyright © 2021