SpringerLink
Log in

Re-CorC-ing KeY: Correct-by-Construction Software Development Based on KeY

  • Chapter
  • First Online:
The Logic of Software. A Tasting Menu of Formal Methods

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13360))

Abstract

Deductive program verification is a post-hoc quality assurance technique following the design-by-contract paradigm where correctness of the program is proven only after it was written. Contrary, correctness-by-construction (CbC) is an incremental program construction technique. Starting with the functional specification, the program’s correctness is guaranteed by application of a small set of refinement rules. Even though CbC is supposed to lead to code with a low defect rate and improve the traceability of errors, it is not widespread. One of the main reasons is insufficient tool support which we addressed with our tool CorC. CorC provides support for CbC-based program construction with the KeY program verifier as backend prover for checking correctness of refinement rule applications. However, CorC was limited to constructing single method bodies restricting its applicability. In this work, we introduce and discuss CorC 2.0, which extends CorC ’s programming model with objects as used in object-oriented programming. We integrate CorC into a development process that allows to use post-hoc verification and CbC interchangeably to construct correct programs, and scale the applicability of CbC on the architectural level in our tool extension ArchiCorC. We developed three object-oriented case studies and evaluated the verification effort and the usability of CorC in comparison to post-hoc verification.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
EUR 29.95
Price includes VAT (Germany)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
EUR 85.59
Price includes VAT (Germany)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
EUR 106.99
Price includes VAT (Germany)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    https://github.com/TUBS-ISF/CorC.

  2. 2.

    https://eclipse.org/emf/.

  3. 3.

    https://eclipse.org/graphiti/.

References

  1. Abrial, J.R.: Modeling in Event-B: System and Software Engineering. 1st edn. (2010)

    Google Scholar 

  2. Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in event-B. Int. J. Softw. Tools Technol. Transf. 12(6), 447–466 (2010)

    Article  Google Scholar 

  3. Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M.: Deductive Software Verification - The KeY Book (2016)

    Google Scholar 

  4. Amighi, A., Blom, S., Darabi, S., Huisman, M., Mostowski, W., Zaharieva-Stojanovski, M.: Verification of concurrent systems with VerCors. In: Bernardo, M., Damiani, F., Hähnle, R., Johnsen, E.B., Schaefer, I. (eds.) SFM 2014. LNCS, vol. 8483, pp. 172–216. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-07317-0_5

    Chapter  Google Scholar 

  5. Apel, S., Batory, D., Kästner, C., Saake, G.: Feature-Oriented Software Product Lines (2013)

    Google Scholar 

  6. Back, R.J.: Invariant based programming: basic approach and teaching experiences. Formal Aspects Comput. 21(3), 227–244 (2009). https://doi.org/10.1007/s00165-008-0070-y

    Article  MATH  Google Scholar 

  7. Back, R.-J., Eriksson, J., Myreen, M.: Testing and verifying invariant based programs in the SOCOS environment. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 61–78. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73770-4_4

    Chapter  Google Scholar 

  8. Back, R.J., Wright, J.: Refinement Calculus: A Systematic Introduction. Springer Science & Business Media (2012). https://doi.org/10.1007/978-1-4612-1674-2

  9. Barnes, J.G.P.: High Integrity Software: The Spark Approach to Safety and Security. Pearson Education (2003)

    Google Scholar 

  10. Batory, D., Sarvela, J.N., Rauschmayer, A.: Scaling step-wise refinement. IEEE Trans. Softw. Eng. 30(6), 355–371 (2004)

    Article  Google Scholar 

  11. Bordis, T., Runge, T., Schaefer, I.: Correctness-by-construction for feature-oriented software product lines. In: Proceedings of the 19th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, pp. 22–34 (2020)

    Google Scholar 

  12. Borgida, A., Mylopoulos, J., Reiter, R.: On the frame problem in procedure specifications. IEEE Trans. Softw. Eng. 21(10), 785–798 (1995)

    Article  Google Scholar 

  13. 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). https://doi.org/10.1007/978-3-642-18070-5_5

    Chapter  MATH  Google Scholar 

  14. Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03359-9_2

    Chapter  Google Scholar 

  15. Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 472–479. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-20398-5_35

    Chapter  Google Scholar 

  16. Crnkovic, I., Sentilles, S., Vulgarakis, A., Chaudron, M.R.: A classification framework for software component models. IEEE Trans. Softw. Eng. 37(5), 593–615 (2010)

    Article  Google Scholar 

  17. Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233–247. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33826-7_16

    Chapter  Google Scholar 

  18. Czarnecki, K., Østerbye, K., Völter, M.: Generative programming. In: Hernández, J., Moreira, A. (eds.) ECOOP 2002. LNCS, vol. 2548, pp. 15–29. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-36208-8_2

    Chapter  Google Scholar 

  19. Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975)

    Article  MathSciNet  Google Scholar 

  20. Dijkstra, E.W.: A Discipline of Programming. 1st edn. Prentice Hall PTR (1976)

    Google Scholar 

  21. Gries, D.: The Science of Programming. 1st edn. (1981)

    Google Scholar 

  22. Gulwani, S., Jha, S., Tiwari, A., Venkatesan, R.: Component-based Synthesis Applied to Bitvector Programs

    Google Scholar 

  23. Hähnle, R., Schaefer, I.: A Liskov principle for delta-oriented programming. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7609, pp. 32–46. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-34026-0_4

    Chapter  Google Scholar 

  24. Hall, R.J.: Fundamental nonmodularity in electronic mail. Autom. Softw. Eng. 12(1), 41–79 (2005)

    Article  Google Scholar 

  25. Heisel, M.: Formalizing and implementing Gries’ program development method in dynamic logic. Sci. Comput. Program. 18(1), 107–137 (1992)

    Article  MathSciNet  Google Scholar 

  26. Jacobs, B., Smans, J., Piessens, F.: A quick tour of the VeriFast program verifier. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 304–311. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17164-2_21

    Chapter  Google Scholar 

  27. Knüppel, A., Runge, T., Schaefer, I.: Scaling correctness-by-construction. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12476, pp. 187–207. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-61362-4_10

    Chapter  Google Scholar 

  28. Knüppel, A., Thüm, T., Padylla, C., Schaefer, I.: Scalability of deductive verification depends on method call treatment. In: Margaria, T., Steffen, B. (eds.) ISoLA 2018. LNCS, vol. 11247, pp. 159–175. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-03427-6_15

    Chapter  Google Scholar 

  29. Kourie, D.G., Watson, B.W.: The Correctness-by-Construction Approach to Programming (2012)

    Google Scholar 

  30. Leavens, G.T., Müller, P.: Information Hiding and Visibility in Interface Specifications, pp. 385–395 (2007)

    Google Scholar 

  31. 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). https://doi.org/10.1007/978-3-642-17511-4_20

    Chapter  MATH  Google Scholar 

  32. Leino, K.R.M., Nelson, G.: Data abstraction and information hiding. ACM Trans. Program. Lang. Syst. 24(5), 491–553 (2002)

    Article  Google Scholar 

  33. Manna, Z., Waldinger, R.: A deductive approach to program synthesis. ACM Trans. Program. Lang. Syst. 2(1), 90–121 (1980)

    Article  Google Scholar 

  34. Meyer, B.: Eiffel: a language and environment for software engineering. J. Syst. Softw. 8(3), 199–246 (1988)

    Article  Google Scholar 

  35. Meyer, B.: Applying ‘design by contract’. Computer 25(10), 40–51 (1992)

    Article  Google Scholar 

  36. Morgan, C.: Programming from Specifications. Prentice Hall (1998)

    Google Scholar 

  37. Oliveira, M., Cavalcanti, A., Woodcock, J.: ArcAngel: a tactic language for refinement. Form. Asp. Comput. 15(1), 28–47 (2003)

    Article  Google Scholar 

  38. Pearce, D.J., Groves, L.: Whiley: a platform for research in software verification. In: Erwig, M., Paige, R.F., Van Wyk, E. (eds.) SLE 2013. LNCS, vol. 8225, pp. 238–248. Springer, Cham (2013). https://doi.org/10.1007/978-3-319-02654-1_13

    Chapter  Google Scholar 

  39. Plath, M., Ryan, M.: Feature integration using a feature construct. Sci. Comput. Program. 41(1), 53–84 (2001)

    Article  Google Scholar 

  40. Pohl, K., Böckle, G., van der Linden, F.J.: Software Product Line Engineering: Foundations, Principles and Techniques (2005)

    Google Scholar 

  41. Polikarpova, N., Kuraj, I., Solar-Lezama, A.: Program synthesis from polymorphic refinement types. ACM SIGPLAN Not. 51(6), 522–538 (2016)

    Article  Google Scholar 

  42. Runge, T., Bordis, T., Thüm, T., Schaefer, I.: Teaching correctness-by-construction and post-hoc verification – the online experience. In: Ferreira, J.F., Mendes, A., Menghi, C. (eds.) FMTea 2021. LNCS, vol. 13122, pp. 101–116. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-91550-6_8

    Chapter  Google Scholar 

  43. Runge, T., Schaefer, I., Cleophas, L., Thüm, T., Kourie, D., Watson, B.W.: Tool support for correctness-by-construction. In: Hähnle, R., van der Aalst, W. (eds.) FASE 2019. LNCS, vol. 11424, pp. 25–42. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-16722-6_2

    Chapter  Google Scholar 

  44. Runge, T., Servetto, M., Potanin, A., Schaefer, I.: Traits for Correct-by-Construction Programming. To be published (2021)

    Google Scholar 

  45. Runge, T., Thüm, T., Cleophas, L., Schaefer, I., Watson, B.W.: Comparing correctness-by-construction with post-hoc verification—a qualitative user study. In: Sekerinski, E., Moreira, N., Oliveira, J.N., Ratiu, D., Guidotti, R., Farrell, M., Luckcuck, M., Marmsoler, D., Campos, J., Astarte, T., Gonnord, L., Cerone, A., Couto, L., Dongol, B., Kutrib, M., Monteiro, P., Delmas, D. (eds.) FM 2019. LNCS, vol. 12233, pp. 388–405. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-54997-8_25

    Chapter  Google Scholar 

  46. Sametinger, J.: Software Engineering with Reusable Components. Springer Science & Business Media (1997)

    Google Scholar 

  47. Steinhöfel, D., Hähnle, R.: Abstract execution. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 319–336. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-30942-8_20

    Chapter  Google Scholar 

  48. Stickel, M., Waldinger, R., Lowry, M., Pressburger, T., Underwood, I.: Deductive composition of astronomical software from subroutine libraries. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 341–355. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58156-1_24

    Chapter  Google Scholar 

  49. Szyperski, C., Gruntz, D., Murer, S.: Component Software: Beyond Object-Oriented Programming. Pearson Education (2002)

    Google Scholar 

  50. Thüm, T., Apel, S., Kästner, C., Schaefer, I., Saake, G.: A classification and survey of analysis strategies for software product lines. ACM Comput. Surv. 47(1), 1–45 (2014)

    Article  Google Scholar 

  51. Thüm, T., Knüppel, A., Krüger, S., Bolle, S., Schaefer, I.: Feature-oriented contract composition. J. Syst. Softw. 152, 83–107 (2019)

    Article  Google Scholar 

  52. Thüm, T., Schaefer, I., Apel, S., Hentschel, M.: Family-based deductive verification of software product lines. In: Proceedings of the 11th International Conference on Generative Programming and Component Engineering, p. 11–20. GPCE 2012, Association for Computing Machinery, NY (2012)

    Google Scholar 

  53. Tschannen, J., Furia, C.A., Nordio, M., Polikarpova, N.: AutoProof: auto-active functional verification of object-oriented programs. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 566–580. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_53

    Chapter  Google Scholar 

  54. Watson, B.W., Kourie, D.G., Schaefer, I., Cleophas, L.: Correctness-by-construction and post-hoc verification: a marriage of convenience? In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9952, pp. 730–748. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-47166-2_52

    Chapter  Google Scholar 

  55. Weiß, B.: Deductive verification of object-oriented software: dynamic frames, dynamic logic, and predicate abstraction. Ph.D. thesis, Karlsruhe Institute of Technology (2011)

    Google Scholar 

Download references

Acknowledgement

We thank Maximilian Kodetzki from TU Braunschweig for implementing large parts of the new features for CorC 2.0.

Author information

Authors and Affiliations

  1. Karlsruhe Institute of Technology (KIT), Karlsruhe, Germany

    Tabea Bordis, Alexander Kittelmann, Tobias Runge & Ina Schaefer

  2. TU Braunschweig, Braunschweig, Germany

    Tabea Bordis, Alexander Kittelmann, Tobias Runge & Ina Schaefer

  3. TU Eindhoven, Eindhoven, The Netherlands

    Loek Cleophas

  4. Stellenbosch University, Stellenbosch, South Africa

    Loek Cleophas & Bruce W. Watson

  5. School for Data-Science and Computational Thinking, Stellenbosch University, Stellenbosch, South Africa

    Bruce W. Watson

Authors
  1. Tabea Bordis
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Loek Cleophas
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Alexander Kittelmann
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Tobias Runge
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Ina Schaefer
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. Bruce W. Watson
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Tabea Bordis .

Editor information

Editors and Affiliations

  1. Chalmers University of Technology, Gothenburg, Sweden

    Wolfgang Ahrendt

  2. Karlsruhe Institute of Technology, Karlsruhe, Germany

    Bernhard Beckert

  3. TU Darmstadt, Darmstadt, Germany

    Richard Bubel

  4. University of Oslo, Oslo, Norway

    Einar Broch Johnsen

A Appendix

A Appendix

Table 2. Verification Time and Verification Steps of All Methods
Full size table

Rights and permissions

Reprints and permissions

Copyright information

© 2022 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Bordis, T., Cleophas, L., Kittelmann, A., Runge, T., Schaefer, I., Watson, B.W. (2022). Re-CorC-ing KeY: Correct-by-Construction Software Development Based on KeY. In: Ahrendt, W., Beckert, B., Bubel, R., Johnsen, E.B. (eds) The Logic of Software. A Tasting Menu of Formal Methods. Lecture Notes in Computer Science, vol 13360. Springer, Cham. https://doi.org/10.1007/978-3-031-08166-8_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-08166-8_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-08165-1

  • Online ISBN: 978-3-031-08166-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation