From Model Checking to a Temporal Proof for Partial Models
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.
Research partly supported from the EU H2020 Research and Innovation Programme under GA No. 731869 (Co4Robots).
- 1.Alavi, H., Avrunin, G., Corbett, J., Dillon, L., Dwyer, M., Pasareanu, C.: Spec patterns (2017). http://patterns.projects.cs.ksu.edu/documentation/patterns/ltl.shtml
- 3.Arcaini, P., Bonfanti, S., Gargantini, A., Mashkoor, A., Riccobene, E.: Formal validation and verification of a medical software critical component. In: Formal Methods and Models for Codesign, pp. 80–89. IEEE (2015)Google Scholar
- 4.Bernasconi, A., Menghi, C., Spoletini, P., Zuck, L., Ghezzi, C.: From model checking to a temporal proof for partial models: preliminary example (2017). arXiv preprint arXiv:1706.02701
- 8.Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT press, Cambridge (1999)Google Scholar
- 9.Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Property specification patterns for finite-state verification. In: Proceedings of the Second Workshop on Formal Methods in Software Practice, pp. 7–15. ACM (1998)Google Scholar
- 11.Godefroid, P., Huth, M.: Model checking vs. generalized model checking: semantic minimizations for temporal logics. In: Logic in Computer Science, pp. 158–167. IEEE Computer Society (2005)Google Scholar
- 17.Larsen, K.G., Thomsen, B.: A modal process logic. In: Logic in Computer Science, pp. 203–210. IEEE (1988)Google Scholar
- 23.Pnueli, A.: The temporal logic of programs. In: Foundations of Computer Science, pp. 46–57. IEEE (1977)Google Scholar