SpringerLink
Log in

Scaling Correctness-by-Construction

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles (ISoLA 2020)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 12476))

Included in the following conference series:

Abstract

The correctness-by-construction paradigm allows developers to derive formally correct programs from a pair of first-order precondition and postcondition. Although tool support has been proposed recently, and thus correctness-by-construction has left the period of pen-and-paper proofs, it is still applied in an unstructured manner to independent algorithmic problems only. To scale correctness-by-construction to more complex programs and to establish a repository of reusable off-the-shelf components, we present a formal framework and open-source tool support called ArchiCorC. In ArchiCorC, a developer models UML-style software components comprising required and provided interfaces, where methods contained in interfaces are associated to specification contracts and mapped to correct-by-construction implementations. We describe our proposed mathematical model for the horizontal and vertical composition of correct-by-construction components, and identify properties that allow to reuse them across different projects. Finally, we demonstrate feasibility of our approach on a case study and discuss future research directions related to the integration of correct-by-construction components into software engineering practices.

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
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 99.99
Price excludes VAT (USA)
  • 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/ArchiCorC.

  2. 2.

    https://eclipse.org/graphiti/.

References

  1. Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)

    Book  Google Scholar 

  2. Ahrendt, W., Beckert, B., Bubel, R., Hähnle, R., Schmitt, P.H., Ulbrich, M.: Deductive Software Verification-The KeY Book. Lecture Notes in Computer Science. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-319-49812-6

    Book  Google Scholar 

  3. Banach, R., Poppleton, M.: Retrenchment: an engineering variation on refinement. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 129–147. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0053358

    Chapter  Google Scholar 

  4. Beckert, B., Schlager, S.: Refinement and retrenchment for programming language data types. Formal Aspects Comput. 17(4), 423–442 (2005)

    Article  Google Scholar 

  5. Benveniste, A., Caillaud, B., Ferrari, A., Mangeruca, L., Passerone, R., Sofronis, C.: Multiple viewpoint contract-based specification and design. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2007. LNCS, vol. 5382, pp. 200–225. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-92188-2_9

    Chapter  MATH  Google Scholar 

  6. Benveniste, A., Caillaud, B., Passerone, R.: Multi-Viewpoint State Machines for Rich Component Models. Model-Based Design of Heterogeneous Embedded Systems (2009)

    Google Scholar 

  7. Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: advanced specification and verification with JML and ESC/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 342–363. Springer, Heidelberg (2006). https://doi.org/10.1007/11804192_16

    Chapter  Google Scholar 

  8. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  9. Dijkstra, E.W.: Guarded commands, non-determinacy and formal derivation of programs. Comm. ACM 18(8), 453–457 (1975)

    Article  MathSciNet  Google Scholar 

  10. Dijkstra, E.W.: A Discipline of Programming, 1st edn. Prentice Hall PTR, Upper Saddle River (1976)

    MATH  Google Scholar 

  11. Gries, D.: The Science of Programming, 1st edn. Springer, Secaucus (1981). https://doi.org/10.1007/978-1-4612-5983-1

    Book  MATH  Google Scholar 

  12. Hatcliff, J., Leavens, G.T., Leino, K.R.M., Müller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. (CSUR) 44(3), 1–58 (2012)

    Article  Google Scholar 

  13. Henzinger, T.A., Sifakis, J.: The discipline of embedded systems design. Computer 40(10), 32–40 (2007)

    Article  Google Scholar 

  14. Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)

    Article  Google Scholar 

  15. Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142–164. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25271-6_8

    Chapter  Google Scholar 

  16. 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). https://doi.org/10.1007/11813040_19

    Chapter  Google Scholar 

  17. Kourie, D.G., Watson, B.W.: The Correctness-by-Construction Approach to Programming. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27919-5

    Book  MATH  Google Scholar 

  18. Lau, K.-K., Tran, C.M.: X-MAN: an MDE tool for component-based system development. In: 2012 38th EUROMICRO Conference on Software Engineering and Advanced Applications, pp. 158–165. IEEE (2012)

    Google Scholar 

  19. Leavens, G.T., Baker, A.L., Ruby, C.: JML: a Java modeling language. In: Formal Underpinnings of Java Workshop (at OOPSLA 1998), pp. 404–420. Citeseer (1998)

    Google Scholar 

  20. Leavens, G.T., Muller, P.: Information hiding and visibility in interface specifications. In: 29th International Conference on Software Engineering (ICSE 2007), pp. 385–395. IEEE (2007)

    Google Scholar 

  21. Liskov, B.H., Wing, J.M.: A behavioral notion of subty**. ACM Trans. Programm. Lang. Syst. (TOPLAS) 16(6), 1811–1841 (1994)

    Article  Google Scholar 

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

    Article  Google Scholar 

  23. Morgan, C.: Programming from Specifications. Prentice Hall, Upper Saddle River (1994)

    MATH  Google Scholar 

  24. Oliveira, M., Cavalcanti, A., Woodcock, J.: ArcAngel: a Tactic Language For Refinement. Formal Aspects Comput. 15(1), 28–47 (2003)

    Article  Google Scholar 

  25. Ozkaya, M.: Visual specification and analysis of contract-based software architectures. J. Comput. Sci. Technol. 32(5), 1025–1043 (2017). https://doi.org/10.1007/s11390-017-1779-y

    Article  Google Scholar 

  26. Ozkaya, M., Kloukinas, C.: Design-by-contract for reusable components and realizable architectures. In: Proceedings of the 17th International ACM SIGSOFT Symposium on Component-Based Software Engineering, pp. 129–138 (2014)

    Google Scholar 

  27. Pierce, B.C.: Types and Programming Languages. MIT Press, Cambridge (2002)

    MATH  Google Scholar 

  28. Rademaker, A., Braga, C., Sztajnberg, A.: A rewriting semantics for a software architecture description language. Electron. Notes Theor. Comput. Sci. 130, 345–377 (2005)

    Article  Google Scholar 

  29. Rawat, D.B., Rodrigues, J.J., Stojmenovic, I.: Cyber-Physical Systems: From Theory to Practice. CRC Press, Boca Raton (2015)

    Google Scholar 

  30. Reussner, R.H., Schmidt, H.W., Poernomo, I.H.: Reliability prediction for component-based software architectures. J. Syst. Softw. 66(3), 241–252 (2003)

    Article  Google Scholar 

  31. Runge, T., Knüppel, A., Thüm, T., Schaefer, I.: Lattice-based information flow control-by-construction for security-by-design. In: FormaliSE 2020. IEEE (2020)

    Google Scholar 

  32. 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 

  33. 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., et al. (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 

  34. Sangiovanni-Vincentelli, A., Damm, W., Passerone, R.: Taming Dr. Frankenstein: contract-based design for cyber-physical systems. Eur. J. Control 18(3), 217–238 (2012)

    Google Scholar 

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

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. TU Braunschweig, Braunschweig, Germany

    Alexander Knüppel, Tobias Runge & Ina Schaefer

Authors
  1. Alexander Knüppel
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tobias Runge
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ina Schaefer
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Alexander Knüppel , Tobias Runge or Ina Schaefer .

Editor information

Editors and Affiliations

  1. Lero, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Knüppel, A., Runge, T., Schaefer, I. (2020). Scaling Correctness-by-Construction. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles. ISoLA 2020. Lecture Notes in Computer Science(), vol 12476. Springer, Cham. https://doi.org/10.1007/978-3-030-61362-4_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-61362-4_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-61361-7

  • Online ISBN: 978-3-030-61362-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation