Advertisement

From Model Checking to a Temporal Proof for Partial Models

  • Anna BernasconiEmail author
  • Claudio MenghiEmail author
  • Paola Spoletini
  • Lenore D. Zuck
  • Carlo Ghezzi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10469)

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.

Notes

Acknowledgments

Research partly supported from the EU H2020 Research and Innovation Programme under GA No. 731869 (Co4Robots).

References

  1. 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
  2. 2.
    Antonik, A., Huth, M.: Efficient patterns for model checking partial state spaces in CTL \(\cap \) LTL. Electron. Notes Theor. Comput. Sci. 158, 41–57 (2006)CrossRefGoogle Scholar
  3. 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. 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
  5. 5.
    Bruns, G., Godefroid, P.: Model checking partial state spaces with 3-valued temporal logics. In: Halbwachs, N., Peled, D. (eds.) CAV 1999. LNCS, vol. 1633, pp. 274–287. Springer, Heidelberg (1999). doi: 10.1007/3-540-48683-6_25CrossRefGoogle Scholar
  6. 6.
    Bruns, G., Godefroid, P.: Generalized model checking: reasoning about partial state spaces. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 168–182. Springer, Heidelberg (2000). doi: 10.1007/3-540-44618-4_14CrossRefGoogle Scholar
  7. 7.
    Bruns, G., Godefroid, P.: Model checking with multi-valued logics. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 281–293. Springer, Heidelberg (2004). doi: 10.1007/978-3-540-27836-8_26CrossRefGoogle Scholar
  8. 8.
    Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT press, Cambridge (1999)Google Scholar
  9. 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
  10. 10.
    Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembiński, P., Średniawa, M. (eds.) Protocol Specification, Testing and Verification, pp. 3–18. Springer, Boston (1996). doi: 10.1007/978-0-387-34892-6_1CrossRefGoogle Scholar
  11. 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
  12. 12.
    Godefroid, P., Huth, M., Jagadeesan, R.: Abstraction-based model checking using modal transition systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 426–440. Springer, Heidelberg (2001). doi: 10.1007/3-540-44685-0_29CrossRefGoogle Scholar
  13. 13.
    Godefroid, P., Piterman, N.: LTL generalized model checking revisited. Int. J. Softw. Tools Technol. Transfer 13(6), 571–584 (2011)CrossRefGoogle Scholar
  14. 14.
    Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997). doi: 10.1007/3-540-63166-6_10CrossRefGoogle Scholar
  15. 15.
    Gurfinkel, A., Chechik, M.: Multi-valued model checking via classical model checking. In: Amadio, R., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 266–280. Springer, Heidelberg (2003). doi: 10.1007/978-3-540-45187-7_18CrossRefGoogle Scholar
  16. 16.
    Gurfinkel, A., Chechik, M.: How thorough is thorough enough? In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 65–80. Springer, Heidelberg (2005). doi: 10.1007/11560548_8CrossRefGoogle Scholar
  17. 17.
    Larsen, K.G., Thomsen, B.: A modal process logic. In: Logic in Computer Science, pp. 203–210. IEEE (1988)Google Scholar
  18. 18.
    Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1992)CrossRefGoogle Scholar
  19. 19.
    Menghi, C., Spoletini, P., Ghezzi, C.: Dealing with incompleteness in automata-based model checking. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 531–550. Springer, Cham (2016). doi: 10.1007/978-3-319-48989-6_32CrossRefGoogle Scholar
  20. 20.
    Namjoshi, K.S.: Certifying model checkers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 2–13. Springer, Heidelberg (2001). doi: 10.1007/3-540-44585-4_2CrossRefGoogle Scholar
  21. 21.
    Peled, D., Pnueli, A., Zuck, L.: From falsification to verification. In: Hariharan, R., Vinay, V., Mukund, M. (eds.) FSTTCS 2001. LNCS, vol. 2245, pp. 292–304. Springer, Heidelberg (2001). doi: 10.1007/3-540-45294-X_25CrossRefGoogle Scholar
  22. 22.
    Peled, D., Zuck, L.: From model checking to a temporal proof. In: Dwyer, M. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 1–14. Springer, Heidelberg (2001). doi: 10.1007/3-540-45139-0_1CrossRefzbMATHGoogle Scholar
  23. 23.
    Pnueli, A.: The temporal logic of programs. In: Foundations of Computer Science, pp. 46–57. IEEE (1977)Google Scholar
  24. 24.
    Rajan, S., Shankar, N., Srivas, M.K.: An integration of model checking with automated proof checking. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 84–97. Springer, Heidelberg (1995). doi: 10.1007/3-540-60045-0_42CrossRefGoogle Scholar
  25. 25.
    Tan, L., Cleaveland, R.: Evidence-based model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 455–470. Springer, Heidelberg (2002). doi: 10.1007/3-540-45657-0_37CrossRefGoogle Scholar
  26. 26.
    Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.S.: Formal methods: practice and experience. ACM Comput. Surv. 41(4) (2009)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.DEIB - Politecnico di MilanoMilanItaly
  2. 2.Chalmers University of TechnologyGothenburgSweden
  3. 3.University of GothenburgGothenburgSweden
  4. 4.Kennesaw State UniversityMariettaGeorgia
  5. 5.University of Illinois at ChicagoChicagoUSA

Personalised recommendations