nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Proof Repositories for Compositional Verification of Evolving Software Systems

Managing Change When Proving Software Correct

verfasst von : Richard Bubel, Ferruccio Damiani, Reiner Hähnle, Einar Broch Johnsen, Olaf Owe, Ina Schaefer, Ingrid Chieh Yu

Erschienen in: Transactions on Foundations for Mastering Change I

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

We propose a new and systematic framework for proof reuse in the context of deductive software verification. The framework generalizes abstract contracts into incremental proof repositories. Abstract contracts enable a separation of concerns between called methods and their implementations, facilitating proof reuse. Proof repositories allow the systematic caching of partial proofs that can be adapted to different method implementations. The framework provides flexible support for compositional verification in the context of, e.g., partly developed programs, evolution of programs and contracts, and product variability.

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 Compositional Model-Based System Design and Other Foundations for Mastering Change

Nächstes Kapitel Statistical Model Checking with Change Detection

We are aware that this basic technique is insufficient to achieve modular verification. Advanced techniques for modular verification, e.g. [1, 22, 34], would obfuscate the fundamental questions considered in this paper and can be superimposed.

Not all locations in LS need to appear in the defs. About the ones who do not, nothing is known except what is stated in E.

This implies the limitation that no (not even pure) method calls can occur in pre- and postconditions. This could be lifted or worked around in various ways.

If i is the label of a method implementation that contains at least one method call, then \(S\Downarrow i,\epsilon \) will always return a non-empty set. More generally, if i is the label of a method implementation and the domain of \(\mathcal {B}\) does not contain all the method calls in i, then \(S\Downarrow i,\mathcal {B}\) will always return a non-empty set.

This is not a restriction since, in Java, method overloading is resolved statically.

This can be checked straightforwardly by comparing the labels.

Barnett, M., DeLine, R., Fähndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. J. Object Technol. 3(6), 27–56 (2004)CrossRef

Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005). doi:10.1007/978-3-540-30569-9_3 CrossRef

Beckert, B., Hähnle, R.: Reasoning and verification. IEEE Intell. Syst. 29(1), 20–29 (2014)CrossRef

Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. The KeY Approach. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)

Beckert, B., Klebanov, V.: Proof reuse for deductive program verification. In: Third IEEE International Conference on Software Engineering and Formal Methods, pp. 77–86. IEEE Computer Society (2004). http://doi.ieeecomputersociety.org/10.1109/SEFM.2004.10013

Beckert, B., Schmitt, P.H.: Program verification using change information. In: Proceedings, Software Engineering and Formal Methods (SEFM), Brisbane, Australia, pp. 91–99. IEEE Press (2003)

Bettini, L., Damiani, F., Schaefer, I.: Compositional type checking of delta-oriented software product lines. Acta Inform. 50(2), 77–122 (2013). doi:10.1007/s00236-012-0173-z MathSciNetCrossRefMATH

Bruns, D., Klebanov, V., Schaefer, I.: Verification of software product lines with delta-oriented slicing. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 61–75. Springer, Heidelberg (2011). doi:10.1007/978-3-642-18070-5_5 CrossRef

Bubel, R., Hähnle, R., Pelevina, M.: Fully abstract operation contracts. In: Margaria, T., Steffen, B. (eds.) ISoLA 2014. LNCS, vol. 8803, pp. 120–134. Springer, Heidelberg (2014). doi:10.1007/978-3-662-45231-8_9

10.

Damiani, F., Dovland, J., Johnsen, E.B., Schaefer, I.: Verifying traits: an incremental proof system for fine-grained reuse. Formal Aspects Comput. 26(4), 761–793 (2014)CrossRefMATH

11.

Damiani, F., Owe, O., Dovland, J., Schaefer, I., Johnsen, E.B., Yu, I.C.: A transformational proof system for delta-oriented programming. In: Proceedings of the 16th International Software Product Line Conference (SPLC), vol. 2, pp. 53–60. ACM (2012)

12.

Dovland, J., Johnsen, E.B., Owe, O., Steffen, M.: Lazy behavioral subtyping. J. Logic Algebraic Program. 79(7), 578–607 (2010)MathSciNetCrossRefMATH

13.

Dovland, J., Johnsen, E.B., Owe, O., Steffen, M.: Incremental reasoning with lazy behavioral subtyping for multiple inheritance. Sci. Comput. Program. 76(10), 915–941 (2011)CrossRefMATH

14.

Dovland, J., Johnsen, E.B., Owe, O., Yu, I.C.: A proof system for adaptable class hierarchies. J. Log. Algebraic Methods Program. 84(1), 37–53 (2015)MathSciNetCrossRefMATH

15.

Dovland, J., Johnsen, E.B., Yu, I.C.: Tracking behavioral constraints during object-oriented software evolution. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 253–268. Springer, Heidelberg (2012). doi:10.1007/978-3-642-34026-0_19 CrossRef

16.

Engel, C., Roth, A., Schmitt, P.H., Weiß, B.: Verification of modifies clauses in dynamic logic with non-rigid functions. Technical report 2009–9, Department of Computer Science, University of Karlsruhe (2009)

17.

Fähndrich, M., Logozzo, F.: Static contract checking with abstract interpretation. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 10–30. Springer, Heidelberg (2011). doi:10.1007/978-3-642-18070-5_2 CrossRef

18.

Filliâtre, J.-C., Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007). doi:10.1007/978-3-540-73368-3_21 CrossRef

19.

Hähnle, R., Schaefer, I., Bubel, R.: Reuse in software verification by abstract method calls. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 300–314. Springer, Heidelberg (2013). doi:10.1007/978-3-642-38574-2_21 CrossRef

20.

Hutter, D., Autexier, S.: Formal software development in MAYA. In: Hutter, D., Stephan, W. (eds.) Mechanizing Mathematical Reasoning. LNCS (LNAI), vol. 2605, pp. 407–432. Springer, Heidelberg (2005). doi:10.1007/978-3-540-32254-2_24 CrossRef

21.

Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011). doi:10.1007/978-3-642-20398-5_4 CrossRef

22.

Kassios, I.T.: Dynamic frames: support for framing, dependencies and sharing without restrictions. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 268–283. Springer, Heidelberg (2006). doi:10.1007/11813040_19 CrossRef

23.

Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Müller, P., Kiniry, J., Chalin, P., Zimmerman, D.M.: JML reference manual (2009). ftp://ftp.cs.iastate.edu/pub/leavens/JML/jmlrefman.pdf. Draft revision 1.235

24.

Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS(LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). doi:10.1007/978-3-642-17511-4_20 CrossRef

25.

Leino, K.R.M., Wüstholz, V.: Fine-grained caching of verification results. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 380–397. Springer, Heidelberg (2015). doi:10.1007/978-3-319-21690-4_22 CrossRef

26.

Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811–1841 (1994)CrossRef

27.

Meyer, B.: Applying “design by contract”. IEEE Comput. 25(10), 40–51 (1992)CrossRef

28.

Müller, P., et al.: The 1st verified software competition: experience report. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 154–168. Springer, Heidelberg (2011)

29.

Reif, W., Stenzel, K.: Reuse of proofs in software verification. In: Shyamasundar, R.K. (ed.) FSTTCS 1993. LNCS, vol. 761, pp. 284–293. Springer, Heidelberg (1993). doi:10.1007/3-540-57529-4_61 CrossRef

30.

Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: 17th IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 55–74. IEEE Computer Society (2002)

31.

Schaefer, I., Bettini, L., Bono, V., Damiani, F., Tanzarella, N.: Delta-oriented programming of software product lines. In: Bosch, J., Lee, J. (eds.) SPLC 2010. LNCS, vol. 6287, pp. 77–91. Springer, Heidelberg (2010). doi:10.1007/978-3-642-15579-6_6 CrossRef

32.

Schaefer, I., Rabiser, R., Clarke, D., Bettini, L., Benavides, D., Botterweck, G., Pathak, A., Trujillo, S., Villela, K.: Software diversity: state of the art and perspectives. Int. J. Softw. Tools Technol. Transf. 14(5), 477–495 (2012). doi:10.1007/s10009-012-0253-y CrossRef

33.

Schairer, A., Hutter, D.: Proof transformations for evolutionary formal software development. In: Kirchner, H., Ringeissen, C. (eds.) AMAST 2002. LNCS, vol. 2422, pp. 441–456. Springer, Heidelberg (2002). doi:10.1007/3-540-45719-4_30 CrossRef

34.

Schmitt, P.H., Ulbrich, M., Weiß, B.: Dynamic frames in java dynamic logic. In: Beckert, B., Marché, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 138–152. Springer, Heidelberg (2011). doi:10.1007/978-3-642-18070-5_10 CrossRef

Titel: Proof Repositories for Compositional Verification of Evolving Software Systems
verfasst von: Richard Bubel
Ferruccio Damiani
Reiner Hähnle
Einar Broch Johnsen
Olaf Owe
Ina Schaefer
Ingrid Chieh Yu
Verlag: Springer International Publishing
Buch: Transactions on Foundations for Mastering Change I
Print ISBN: 978-3-319-46507-4

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

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-319-46508-1_8

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"