nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

From Model Checking to a Temporal Proof for Partial Models

verfasst von : Anna Bernasconi, Claudio Menghi, Paola Spoletini, Lenore D. Zuck, Carlo Ghezzi

Erschienen in: Software Engineering and Formal Methods

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel A Complete Generative Label Model for Lattice-Based Access Control Models

Nächstes Kapitel Modeling and Reasoning on Requirements Evolution with Constrained Goal Models

In [6] the procedure is presented for PML but is valid also for LTL (see [6, 11, 13]).

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

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)CrossRef

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)

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

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_25CrossRef

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_14CrossRef

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_26CrossRef

Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT press, Cambridge (1999)

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)

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_1CrossRef

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)

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_29CrossRef

13.

Godefroid, P., Piterman, N.: LTL generalized model checking revisited. Int. J. Softw. Tools Technol. Transfer 13(6), 571–584 (2011)CrossRef

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_10CrossRef

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_18CrossRef

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_8CrossRef

17.

Larsen, K.G., Thomsen, B.: A modal process logic. In: Logic in Computer Science, pp. 203–210. IEEE (1988)

18.

Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York (1992)CrossRef

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_32CrossRef

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_2CrossRef

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_25CrossRef

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_1CrossRefMATH

23.

Pnueli, A.: The temporal logic of programs. In: Foundations of Computer Science, pp. 46–57. IEEE (1977)

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_42CrossRef

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_37CrossRef

26.

Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.S.: Formal methods: practice and experience. ACM Comput. Surv. 41(4) (2009)CrossRef

Titel: From Model Checking to a Temporal Proof for Partial Models
verfasst von: Anna Bernasconi
Claudio Menghi
Paola Spoletini
Lenore D. Zuck
Carlo Ghezzi
Verlag: Springer International Publishing
Buch: Software Engineering and Formal Methods
Print ISBN: 978-3-319-66196-4

Electronic ISBN: 978-3-319-66197-1

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-319-66197-1_4

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner