Advertisement

Why Programming Must Be Supported by Modeling and How

  • Egon BörgerEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11244)

Abstract

The development of code for software intensive systems involves numerous levels of abstraction, leading from requirements to code. Having abstract modeling concepts available as high-level programming constructs helps to define the code and to make sure that when the system runs with the software executed by machines, the software components behave in the expected way. We explain in this paper that nevertheless, there remains a gap, which cannot be closed by mere programming methods, but which can be closed if programming is supported by an appropriate modeling framework (a design and analysis method and a language).

Notes

Acknowledgement

We thank the following colleagues for a critical reading of various drafts of the paper: Don Batory, Heinz Dobler, Albert Fleischmann, Uwe Glässer, Daniel Jackson, Michael Jackson, Alexander Raschke, Klaus-Dieter Schewe and two anonymous referees.

References

  1. 1.
    Abrial, J.-R.: The B-Book. Cambridge University Press, Cambridge (1996)CrossRefGoogle Scholar
  2. 2.
    Abrial, J.-R.: Modeling in Event-B. Cambridge University Press, New York (2010)CrossRefGoogle Scholar
  3. 3.
    Artho, C., Havelund, K., Kumar, R., Yamagata, Y.: Domain-specific languages with scala. In: Butler, M., Conchon, S., Zaïdi, F. (eds.) ICFEM 2015. LNCS, vol. 9407, pp. 1–16. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-25423-4_1CrossRefGoogle Scholar
  4. 4.
    Back, R., Kurki-Suoni, R.: Decentralization of process nets with centralized control. Technical report Ser. A, No. 58, Department of Computer Science at Abo Akademi, Abo, Finland, February 1988Google Scholar
  5. 5.
    Batory, D., Börger, E.: Modularizing theorems for software product lines: the Jbook case study. J. Univers. Comput. Sci. 14(12), 2059–2082 (2008)Google Scholar
  6. 6.
    Berry, G.: Formally unifying modeling and design for embedded systems - a personal view. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 134–149. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47169-3_11CrossRefGoogle Scholar
  7. 7.
    Börger, E.: A logical operational semantics of full Prolog. Part I: selection core and control. In: Börger, E., Büning, H.K., Richter, M.M. (eds.) CSL 1989. LNCS, vol. 440, pp. 36–64. Springer, Heidelberg (1990).  https://doi.org/10.1007/3-540-52753-2_31CrossRefGoogle Scholar
  8. 8.
    Börger, E.: A logical operational semantics of full Prolog. Part II: built-in predicates for database manipulations. In: Rovan, B. (ed.) MFCS 1990. LNCS, vol. 452, pp. 1–14. Springer, Heidelberg (1990).  https://doi.org/10.1007/BFb0029592CrossRefGoogle Scholar
  9. 9.
    Börger, E.: Logic programming: the evolving algebra approach. In: Pehrson, B., Simon, I. (eds.) IFIP 13th World Computer Congress. Technology/Foundations, vol. 1, pp. 391–395. Elsevier, Amsterdam (1994)Google Scholar
  10. 10.
    Błlorger, E.: Review of E. W. Dijkstra and C. S. Scholten. Predicate Calculus and Program Semantics. Springer, Heidelberg (1989).  https://doi.org/10.1007/978-1-4612-3228-5; Science of Computer Programming 23, 1–11 (1994)CrossRefGoogle Scholar
  11. 11.
    Börger, E.: The ASM refinement method. Form. Aspects Comput. 15, 237–257 (2003)CrossRefGoogle Scholar
  12. 12.
    Börger, E.: The abstract state machines method for modular design and analysis of programming languages. J. Logic Comput. 27(2), 417–439 (2014)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Börger, E., Dässler, K.: Prolog: DIN papers for discussion. ISO/IEC JTCI SC22 WG17 Prolog Standardization Document 58, National Physical Laboratory (1990)Google Scholar
  14. 14.
    Börger, E., Durdanović, I.: Correctness of compiling Occam to Transputer code. Comput. J. 39(1), 52–92 (1996)CrossRefGoogle Scholar
  15. 15.
    Börger, E., Durdanović, I., Rosenzweig, D.: Occam: specification and compiler correctness. Part I: simple mathematical interpreters. In: Montanari, U., Olderog, E.R. (eds.) Proceedings of the PROCOMET 1994, IFIP Working Conference on Programming Concepts, Methods and Calculi, North-Holland, pp. 489–508 (1994)Google Scholar
  16. 16.
    Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. Perspectives in Mathematical Logic. Springer, Heidelberg (1997). Second printing in “Universitext”, Springer 2001CrossRefGoogle Scholar
  17. 17.
    Börger, E., Fruja, G., Gervasi, V., Stärk, R.: A high-level modular definition of the semantics of C#. Theor. Comput. Sci. 336(2–3), 235–284 (2005)MathSciNetCrossRefGoogle Scholar
  18. 18.
    Börger, E., Gargantini, A., Riccobene, E.: Abstract state machines. A method for system specification and analysis. In: Frappier, M., Habrias, H. (eds.) Software Specification Methods: An Overview Using a Case Study, pp. 103–119. HERMES Sc. Publ. (2006)Google Scholar
  19. 19.
    Börger, E., Joannou, P., Parnas, D.L.: Practical Methods for Code Documentation and Inspection, vol. 178. Dagstuhl Seminar No. 9720, Schloss Dagstuhl, International Conference and Research Center for Computer Science, May 1997Google Scholar
  20. 20.
    Börger, E., Mearelli, L.: Integrating ASMs into the software development life cycle. J. Univers. Comput. Sci. 3(5), 603–665 (1997)zbMATHGoogle Scholar
  21. 21.
    Börger, E., Päppinghaus, P., Schmid, J.: Report on a practical application of ASMs in software design. In: Gurevich, Y., Kutter, P.W., Odersky, M., Thiele, L. (eds.) ASM 2000. LNCS, vol. 1912, pp. 361–366. Springer, Heidelberg (2000).  https://doi.org/10.1007/3-540-44518-8_20CrossRefGoogle Scholar
  22. 22.
    Börger, E., Raschke, A.: Modeling Companion for Software Practitioners. Springer, Heidelberg (2018).  https://doi.org/10.1007/978-3-662-56641-1. For Corrigenda and lecture material on themes treated in the book see http://modelingbook.informatik.uni-ulm.deCrossRefGoogle Scholar
  23. 23.
    Börger, E., Rosenzweig, D.: A mathematical definition of full Prolog. Sci. Comput. Program. 24, 249–286 (1995)MathSciNetCrossRefGoogle Scholar
  24. 24.
    Börger, E., Rosenzweig, D.: The WAM - definition and compiler correctness. In: Beierle, C., Plümer, L. (eds.) Logic Programming: Formal Methods and Practical Applications. Studies in Computer Science and Artificial Intelligence, vol. 11, Chapter 2, pp. 20–90. North-Holland (1995)Google Scholar
  25. 25.
    Börger, E., Schewe, K.-D.: Concurrent abstract state machines. Acta Informatica 53(5), 469–492 (2016).  https://doi.org/10.1007/s00236-015-0249-7. Listed as Notable Article in ACM 21th Annual BEST OF COMPUTING, see http://www.computingreviews.com/recommend/bestof/notableitems.cfm?bestYear=2016MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Börger, E., Stärk, R.F.: Abstract State Machines. A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003).  https://doi.org/10.1007/978-3-642-18216-7CrossRefzbMATHGoogle Scholar
  27. 27.
    Börger, E., Stärk, R.F.: Exploiting abstraction for specification reuse. The Java/C# case study. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2003. LNCS, vol. 3188, pp. 42–76. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-540-30101-1_3CrossRefzbMATHGoogle Scholar
  28. 28.
    Brooks, F.P.: No silver bullet: essence and accidents of software engineering. Computer 20(4), 10–19 (1987)CrossRefGoogle Scholar
  29. 29.
    Broy, M., Havelund, K., Kumar, R.: Towards a unified view of modeling and programming. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016, Part II. LNCS, vol. 9953, pp. 238–257. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47169-3_17CrossRefGoogle Scholar
  30. 30.
    The CoreASM Project. http://www.coreasm.org and https://github.com/coreasm/, since 2005
  31. 31.
    Del Castillo, G.: The ASM Workbench. A Tool Environment for Computer-Aided Analysis and Validation of Abstract State Machine Models. Ph.D. thesis, Universität Paderborn, Germany (2001). Published in HNI-Verlagsschriftenreihe, vol. 83Google Scholar
  32. 32.
    Derrick, J., Boiten, E.A.: Refinement in Z and Object-Z. Springer, London (2001).  https://doi.org/10.1007/978-1-4471-0257-1CrossRefzbMATHGoogle Scholar
  33. 33.
    Dijkstra, E.: Guarded commands, non-determinacy and formal derivation of programs. Commun. ACM 18(8), 453–457 (1975). Also documented as EWD 472CrossRefGoogle Scholar
  34. 34.
    Dmitriev, S.: Language oriented programming: The next programming paradigm. onBoard Electronic Monthly Magazine, April 2010. http://www.onboard.jetbrains.com/articles/04/10/lop/index.html
  35. 35.
    Dold, A.: A formal representation of Abstract State Machines using PVS. Verifix Technical report Ulm/6.2, Universität Ulm, Germany, July 1998Google Scholar
  36. 36.
    Ernst, G., Pfähler, J.: Modular, crash-safe refinement for ASMs with submachines. Sci. Comput. Program. 131, 3–21 (2016). Alloy, B, TLA, VDM and Z (ABZ 2014)CrossRefGoogle Scholar
  37. 37.
    Ernst, G., Pfähler, J., Schellhorn, G., Reif, W.: Inside a verified flash file system: transactions and garbage collection. In: Gurfinkel, A., Seshia, S.A. (eds.) VSTTE 2015. LNCS, vol. 9593, pp. 73–93. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-29613-5_5CrossRefGoogle Scholar
  38. 38.
    Ernst, G., Schellhorn, G., Haneberg, D., Pfähler, J., Reif, W.: Verification of a virtual filesystem switch. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 242–261. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54108-7_13CrossRefGoogle Scholar
  39. 39.
    Fehnker, A., van Glabbeek, R., Hoefner, P., McIver, A., Portmann, M., Tan, W.L.: A process algebra for wireless mesh networks used for modelling, verifying and analysing AODV. Technical report 5513, NICTA, Brisbane, Australia (2013)Google Scholar
  40. 40.
    Ferrarotti, F., Schewe, K.-D., Tec, L.: A behavioural theory for reflective sequential algorithms. In: Petrenko, A.K., Voronkov, A. (eds.) PSI 2017. LNCS, vol. 10742, pp. 117–131. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-74313-4_10CrossRefGoogle Scholar
  41. 41.
    Ferrarotti, F., Schewe, K.-D., Tec, L., Wang, Q.: A new thesis concerning synchronised parallel computing - simplified parallel ASM thesis. Theor. Comp. Sci. 649, 25–53 (2016)MathSciNetCrossRefGoogle Scholar
  42. 42.
    Fleischmann, A., Oppl, S., Schmidt, W., Stary, C.: Ganzheitliche Digitalisierung von Prozessen. Springer, Heidelberg (2018).  https://doi.org/10.1007/978-3-658-22648-0. Open Access BookCrossRefGoogle Scholar
  43. 43.
    Fleischmann, A., Schmidt, W., Stary, C., Obermeier, S., Börger, E.: Subject-Oriented Business Process Management. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-32392-8. http://www.springer.com/978-3-642-32391-1 (Open Access Book)CrossRefGoogle Scholar
  44. 44.
    Fruja, N.G.: Type Safety of C# and .NET CLR. Ph.D. thesis, ETH Zürich (2006)Google Scholar
  45. 45.
    Fuchs, N.E.: Specifications are (preferably) executable. Softw. Eng. J. 7, 323–334 (1992)CrossRefGoogle Scholar
  46. 46.
    Gervasi, V., Riccobene, E.: From English to ASM: on the process of deriving a formal specification from a natural language one. In Integration of Tools for Rigorous Software Construction and Analysis, volume 3(9) of Dagstuhl Report, pp. 85–90 (2014). Dagstuhl Seminar 13372 organized by Uwe Glässer, Stefan Hallerstede, Michael Leuschel, Elvinia Riccobene, 08.–13 September 2013.  https://doi.org/10.4230/DagRep.3.9.74, URN: urn:nbn:de:0030-drops-43584, http://drops.dagstuhl.de/opus/volltexte/2014/4358/
  47. 47.
    Goerigk, W., et al.: Compiler correctness and implementation verification: The Verifix approach. In: Fritzson, P. (ed.) International Conference on Compiler Construction, Proceedings Poster Session of CC 1996, IDA Technical Report LiTH-IDA-R-96-12, Linköping, Sweden (1996)Google Scholar
  48. 48.
    Grandy, H., Bischof, M., Stenzel, K., Schellhorn, G., Reif, W.: Verification of Mondex electronic purses with KIV: from a security protocol to verified code. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 165–180. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-68237-0_13CrossRefGoogle Scholar
  49. 49.
    Granger, C.: Coding is not the new literacy, January 2015. http://www.chris-granger.com/2015/01/26/coding-is-not-the-new-literacy/. Consulted 01 December 2017
  50. 50.
    Hall, J.A.: Taking Z seriously. In: Bowen, J.P., Hinchey, M.G., Till, D. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 87–91. Springer, Heidelberg (1997).  https://doi.org/10.1007/BFb0027285CrossRefGoogle Scholar
  51. 51.
    Haneberg, D., Grandy, H., Reif, W., Schellhorn, G.: Verifying smart card applications: an ASM approach. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 313–332. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-73210-5_17CrossRefGoogle Scholar
  52. 52.
    Haneberg, D., Moebius, N., Reif, W., Schellhorn, G., Stenzel, K.: Mondex: engineering a provable secure electronic purse. Int. J. Softw. Inform. 5(1), 159–184 (2011). http://www.ijsi.orgGoogle Scholar
  53. 53.
    Haneberg, D., Schellhorn, G., Grandy, H., Reif, W.: Verification of Mondex electronic purses with KIV: from transactions to a security protocol. Form. Aspects Comput. 20(1), 41–59 (2008)CrossRefGoogle Scholar
  54. 54.
    Havelund, K.: Data automata in scala. In: Leucker, M., Wang, J. (eds.) Proceedings of the 8th International Symposium on Theoretical Aspects of Software Engineering (TASE), pp. 1–9. IEEE Computer Society Press (2014)Google Scholar
  55. 55.
    Havelund, K., Joshi, R.: Modeling and monitoring of hierarchical state machines in scala. In: Romanovsky, A., Troubitsyna, E.A. (eds.) SERENE 2017. LNCS, vol. 10479, pp. 21–36. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-65948-0_2CrossRefGoogle Scholar
  56. 56.
    Hayes, I.J., Jones, C.B.: Specifications are not (necessarily) executable. Softw. Eng. J. 4(6), 330–33 (1989)CrossRefGoogle Scholar
  57. 57.
    Jackson, M.: Problem Frames. Addison-Wesley, Boston (2001)Google Scholar
  58. 58.
    Jackson, M.: The right-hand side problem: Research topics in RE. In: RE Silver Jubilee, RE 2017, Lisbon, 6 September 2017Google Scholar
  59. 59.
  60. 60.
    Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002). http://lamport.org
  61. 61.
    Lamport, L., Paulson, L.C.: Should your specification language be typed? ACM Trans. Program. Lang. Syst. 21(3), 502–526 (1999)CrossRefGoogle Scholar
  62. 62.
    Leibniz, G.W.: Dialogus de connexione inter res et verba. Leibniz, G.W.: Philosophische Schriften, August 1677. Edited by Leibniz-Forschungsstelle der Universität Münster, vol. 4 A, n.8. Akademie Verlag (1999)Google Scholar
  63. 63.
    Leveson, N.G.: Engineering a Safer World: Systems Thinking Applied to Safety. Engineering Systems. MIT Press, Cambridge (2012)Google Scholar
  64. 64.
    Lewerentz, C., Lindner, T. (eds.): Formal Development of Reactive Systems. LNCS, vol. 891. Springer, Heidelberg (1995).  https://doi.org/10.1007/3-540-58867-1CrossRefzbMATHGoogle Scholar
  65. 65.
    Mearelli, L.: Refining an ASM specification of the production cell to C++ code. J. Univers. Comput. Sci. 3(5), 666–688 (1997)zbMATHGoogle Scholar
  66. 66.
    Meta Programming System. https://www.jetbrains.com/mps/
  67. 67.
    Naur, P.: Programming as Theory Building. Microprocessing and Microprogramming, vol. 15 (1985)CrossRefGoogle Scholar
  68. 68.
    Perkins, C., Belding-Royer, E., Das, S.: Ad hoc on-demand distance vector (AODV) routing. Technical report RFC 3561, Copyright (C) The Internet Society, Network Working Group, July 2003. http://tools.ietf.org/html/rfc3561
  69. 69.
    Pfähler, J., Ernst, G., Bodenmüller, S., Schellhorn, G., Reif, W.: Modular verification of order-preserving write-back caches. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 375–390. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-66845-1_25CrossRefGoogle Scholar
  70. 70.
    Popper, K.: Logik der Forschung. Springer, Heidelberg (1935)CrossRefGoogle Scholar
  71. 71.
    Schellhorn, G.: Verification of ASM refinements using generalized forward simulation. J. Univers. Comput. Sci. 7(11), 952–979 (2001)MathSciNetGoogle Scholar
  72. 72.
    Schellhorn, G.: ASM refinement and generalizations of forward simulation in data refinement: a comparison. Theor. Comput. Sci. 336(2–3), 403–436 (2005)MathSciNetCrossRefGoogle Scholar
  73. 73.
    Schellhorn, G.: ASM refinement preserving invariants. J. UCS 14(12), 1929–1948 (2008)MathSciNetzbMATHGoogle Scholar
  74. 74.
    Schellhorn, G.: Completeness of ASM refinement. Electr. Notes Theor. Comput. Sci. 214, 25–49 (2008)CrossRefGoogle Scholar
  75. 75.
    Schellhorn, G.: Completeness of fair ASM refinement. Sci. Comput. Program. 76(9), 756–773 (2011)CrossRefGoogle Scholar
  76. 76.
    Schellhorn, G., Ahrendt, W.: Reasoning about abstract state machines: the WAM case study. J. Univers. Comput. Sci. 3(4), 377–413 (1997)MathSciNetzbMATHGoogle Scholar
  77. 77.
    Schellhorn, G., Ahrendt, W.: The WAM case study: verifying compiler correctness for Prolog with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction - A Basis for Applications, volume III: Applications, pp. 165–194. Kluwer Academic Publishers, Dordrecht (1998)CrossRefGoogle Scholar
  78. 78.
    Schellhorn, G., Ernst, G., Pfähler, J., Haneberg, D., Reif, W.: Development of a verified flash file system. ABZ 2014. LNCS, vol. 8477, pp. 9–24. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-662-43652-3_2CrossRefGoogle Scholar
  79. 79.
    Schellhorn, G., Grandy, H., Haneberg, D., Moebius, N., Reif, W.: A systematic verification approach for Mondex electronic purses using ASMs. In: Abrial, J.-R., Glässer, U. (eds.) Rigorous Methods for Software Construction and Analysis. LNCS, vol. 5115, pp. 93–110. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-11447-2_7CrossRefGoogle Scholar
  80. 80.
    Schewe, K.-D., Ferrarotti, F., Tec, L., Wang, Q.: Distributed adaptive systems: theory, specification, reasoning. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) ABZ 2018. LNCS, vol. 10817, pp. 16–30. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-91271-4_2CrossRefGoogle Scholar
  81. 81.
    Schewe, K.-D., Ferrarotti, F., Tec, L., Wang, Q., An, W.: Evolving concurrent systems: behavioural theory and logic. In: Proceedings of the Australasian Computer Science Week Multiconference (ACSW 2017), pp. 77:1–77:10. ACM (2017)Google Scholar
  82. 82.
    Schmid, J.: Executing ASM specifications with AsmGofer. https://tydo.eu/AsmGofer
  83. 83.
    Schmid, J.: Compiling abstract state machines to C++. J. Univers. Comput. Sci. 7(11), 1069–1088 (2001)Google Scholar
  84. 84.
    Selic, B.: Programming \(\subset \) Modeling \(\subset \) Engineering. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 11–26. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-47169-3_2CrossRefGoogle Scholar
  85. 85.
    Somers, J.: The coming software apocalypse. The Atlantic, 26 September 2017. Email newsletter, consulted on 11 November 2017Google Scholar
  86. 86.
    Stärk, R.F., Schmid, J., Börger, E.: Java and the Java Virtual Machine: Definition, Verification, Validation. Springer, Heidelberg (2001).  https://doi.org/10.1007/978-3-642-59495-3CrossRefzbMATHGoogle Scholar
  87. 87.
    Thalheim, B., Nissen, I. (eds.): Wissenschaft und Kunst der Modellierung: Kieler Zugang zur Definition, Nutzung und Zukunft. Philosophische Analyse/Philosophical Analysis. vol. 64, De Gruyter (2015)Google Scholar
  88. 88.
    Ward, M.P.: Language oriented programming. Softw. Concepts Tools 15(4), 147–161 (1994)Google Scholar
  89. 89.
    Zimmerman, W., Gaul, T.: On the construction of correct compiler back-ends: an ASM approach. J. Univers. Comput. Sci. 3(5), 504–567 (1997)zbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Dipartimento di InformaticaUniversità di PisaPisaItaly

Personalised recommendations