A Non-unified View of Modelling, Specification and Programming

  • Stefan HallerstedeEmail author
  • Peter Gorm Larsen
  • John Fitzgerald
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11244)


The languages used to express specifications, models and programs have much in common. However, in this paper we argue that because they serve different purposes, real care should be taken to distinguish them during development. Rather than seeking unification at the language level, we would recommend exploiting intersections between them where they arise. The main contribution of this paper is to point out the necessary differences and to offer evidence of situations in which common ground can be reached.



We are grateful to our many collaborators and sponsors in projects such as DESTECS (FP7-248134), COMPASS (FP7-287829) and INTO-CPS (H2020-644047) as well as those mentioned in the appendices which collectively have formed our minds seeing the development of software in a more holistic fashion causing us to have the opinions presented in this article.


  1. 1.
    Abrial, J.R.: The B Book – Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)CrossRefGoogle Scholar
  2. 2.
    Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)CrossRefGoogle Scholar
  3. 3.
    Andrews, J.H.: Executing formal specifications by translation to higher order logic programming. In: Gunter, E.L., Felty, A. (eds.) TPHOLs 1997. LNCS, vol. 1275, pp. 17–32. Springer, Heidelberg (1997). Scholar
  4. 4.
    Berrou, C., Glavieux, A.: Near optimum error-correcting coding and decoding: Turbo codes. IEEE Trans. Commun. 44(10), 1261–1271 (1996)CrossRefGoogle Scholar
  5. 5.
    Börger, E., Stärk, R.: Abstract State Machines. Springer, Heidelberg (2003). Scholar
  6. 6.
    Cansell, D., Hallerstede, S., Oliver, I.: UML-B specification and hardware implementation of a Hamming coder/decoder. In: Mermet, J. (ed.) UML-B Specification for Proven Embedded Systems Design. Kluwer Academic Publishers, Boston (2004)Google Scholar
  7. 7.
    Jones, C., Jones, K., Lindsay, P.A., Moore, R. (eds.): mural: A Formal Development Support System. Springer, London (1991). ISBN 3-540-19651-XCrossRefzbMATHGoogle Scholar
  8. 8.
    Couto, L.D., Tran-Jørgensen, P.W.V., Edwards, G.T.C.: Combining harvesting operations optimisation using strategy-based simulation. In: Proceedings of the 6th International Conference on Simulation and Modeling Methodologies, Technologies and Applications (SIMULTECH), July 2016Google Scholar
  9. 9.
    Couto, L.D., Tran-Jørgensen, P.W.V., Edwards, G.T.C.: Model-based development of a multi-algorithm harvest planning system. In: Obaidat, M.S., Ören, T., Merkuryev, Y. (eds.) SIMULTECH 2016. AISC, vol. 676, pp. 19–33. Springer, Cham (2018). Scholar
  10. 10.
    Couto, L.D., Tran-Jørgensen, P.W.V., Larsen, P.G.: Enabling continuous integration in a formal methods setting (2018). Submitted for publicationGoogle Scholar
  11. 11.
    Fitzgerald, J., Larsen, P.G., Verhoef, M. (eds.): Collaborative Design for Embedded Systems – Co-modelling and Co-simulation. Springer, Heidelberg (2013). Scholar
  12. 12.
    Fröhlich, B., Larsen, P.G.: Combining VDM-SL specifications with C++ code. In: Gaudel, M.-C., Woodcock, J. (eds.) FME 1996. LNCS, vol. 1051, pp. 179–194. Springer, Heidelberg (1996). Scholar
  13. 13.
    Fuchs, N.E.: Specifications are (preferably) executable. Softw. Eng. J. 7, 323–334 (1992)CrossRefGoogle Scholar
  14. 14.
    Gamble, C., Payne, R., Fitzgerald, J., Soudjani, S., Foldager, F.F., Larsen, P.G.: Automated exploration of parameter spaces as a method for tuning a predictive digital twin (2018). Submitted for publicationGoogle Scholar
  15. 15.
    Gaudel, M.-C.: Testing can be formal, too. In: Mosses, P.D., Nielsen, M., Schwartzbach, M.I. (eds.) CAAP 1995. LNCS, vol. 915, pp. 82–96. Springer, Heidelberg (1995). Scholar
  16. 16.
    Gomes, C., Thule, C., Broman, D., Larsen, P.G., Vangheluwe, H.: Co-simulation: a survey. ACM Comput. Surv. 51(3), 49:1–49:33 (2018)CrossRefGoogle Scholar
  17. 17.
    Hallerstede, S., Zimmermann, Y.: Circuit design by refinement in EventB. In: FDL, pp. 624–637. ECSI (2004)Google Scholar
  18. 18.
    Hansen, D., Schneider, D., Leuschel, M.: Using B and ProB for data validation projects. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 167–182. Springer, Cham (2016). Scholar
  19. 19.
    Hasanagić, M., Fabbri, T., Larsen, P.G., Bandur, V., Tran-Jørgensen, P., Ouy, J.: Code generation for distributed embedded systems (2018). Submitted for publicationGoogle Scholar
  20. 20.
    Hayes, I., Jones, C.: Specifications are not (necessarily) executable. Softw. Eng. J., 330–338 (1989). Scholar
  21. 21.
    Hentenryck, P.V., Michel, L.: Constraint-Based Local Search. MIT Press, Cambridge (2005)zbMATHGoogle Scholar
  22. 22.
    Hinchey, M., Bowen, J.P., Olderog, E.R. (eds.): Provably Correct Systems. NASA Monographs in Systems and Software Engineering. Springer, Cham (2017). Scholar
  23. 23.
    Holt, J., Perry, S.: SysML for Systems Engineering. IET (2008)Google Scholar
  24. 24.
    IEEE: International Standard ISO/IEC/IEEE 15288:2015(E), Systems and software engineering — System life cycle processes. ISO/IEC and IEEE Computer Society (2015)Google Scholar
  25. 25.
    IEEE Standards Board: IEEE standard glossary of software engineering terminology–IEEE std 610.12-1990 (1990)Google Scholar
  26. 26.
    INCOSE: Systems Engineering Handbook. A Guide for System Life Cycle Processes and Activities, Version 4.0. Technical report INCOSE-TP-2003-002-04, International Council on Systems Engineering (INCOSE), January 2015Google Scholar
  27. 27.
    SAE International: SAE J1708 revised OCT93, serial data communication between microcomputer systems in heavy-duty vehicle applications.
  28. 28.
    Jackson, M.: Problem Frames: Analysing and Structuring Software Development Problems. Addison-Wesley, New York (2001)Google Scholar
  29. 29.
    Jacobson, I.: Ivar Jacobson on UML, MDA, and the future of methodologies. InnoQ (2006). InterviewGoogle Scholar
  30. 30.
    Jørgensen, P.W.V., Larsen, M., Couto, L.D.: A code generation platform for VDM. In: Battle, N., Fitzgerald, J. (eds.) Proceedings of the 12th Overture Workshop. School of Computing Science, Newcastle University, UK, Technical report CS-TR-1446, January 2015Google Scholar
  31. 31.
    Kowalski, R.: The relation between logic programming and logic specification. In: Hoare, C.A.R., Shepherdson, J. (eds.) Mathematical Logic and Programming Languages, pp. 11–24. Prentice-Hall, Upper Saddle River (1985)Google Scholar
  32. 32.
    Kramer, J.: Is abstraction the key to computing? Commun. ACM 50(4), 37–42 (2007)CrossRefGoogle Scholar
  33. 33.
    Larsen, P.G.: Evaluation of underdetermined explicit definitions. In: Naftalin, M., Denvir, T., Bertran, M. (eds.) FME 1994. LNCS, vol. 873, pp. 233–250. Springer, Heidelberg (1994). Scholar
  34. 34.
    Larsen, P.G.: Ten years of historical development: “Bootstrapping” VDMTools. J. Univers. Comput. Sci. 7(8), 692–709 (2001)zbMATHGoogle Scholar
  35. 35.
    Larsen, P.G., Battle, N., Ferreira, M., Fitzgerald, J., Lausdahl, K., Verhoef, M.: The overture initiative – integrating tools for VDM. SIGSOFT Softw. Eng. Notes 35(1), 1–6 (2010). Scholar
  36. 36.
    Larsen, P.G., Fitzgerald, J., Brookes, T.: Applying formal specification in industry. IEEE Softw. 13(3), 48–56 (1996)CrossRefGoogle Scholar
  37. 37.
    Larsen, P.G., Fitzgerald, J., Woodcock, J., Nilsson, R., Gamble, C., Foster, S.: Towards semantically integrated models and tools for cyber-physical systems design. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 171–186. Springer, Cham (2016). Scholar
  38. 38.
    Lecomte, T., Burdy, L., Leuschel, M.: Formally Checking Large Data Sets in the Railways. CoRR abs/1210.6815 (2012)Google Scholar
  39. 39.
    Nielsen, C.B., Larsen, P.G.: Extending VDM-RT to enable the formal modelling of system of systems. In: Proceedings of the 7th International Conference on System of System Engineering, IEEE SoSE 2012. IEEE, July 2012. IEEE Systems JournalGoogle Scholar
  40. 40.
    Nielsen, C.B., Lausdahl, K., Larsen, P.G.: Combining VDM with executable code. In: Derrick, J. (ed.) ABZ 2012. LNCS, vol. 7316, pp. 266–279. Springer, Heidelberg (2012). ISBN 978-3-642-30884-0CrossRefGoogle Scholar
  41. 41.
    Nilsson, R.S., Lausdahl, K.G., Macedo, H.D., Larsen, P.G.: Transforming an industrial case study from VDM++ to VDM-SL. In: The 16th Overture Workshop, Oxford, July 2018Google Scholar
  42. 42.
    NIST, Cyber Physical Systems Public Working Group: Framework for cyber-physical systems: Release 1.0. Technical report National Institute of Standardards and Technology, May 2016Google Scholar
  43. 43.
    Oxford English Dictionary Online. Oxford University Press (2010)Google Scholar
  44. 44.
    Kowalski, R.: The relation between logic programming and logic specification. In: Mathematical Logic and Programming Languages, pp. 11–27 (1985)Google Scholar
  45. 45.
    Royce, W.: Managing the development of large software systems. In: WESCON, August 1970. Reprinted in the Proceedings of the 9th International Conference on Software Engineering (ICSE), Washington D.C. IEEE Computer Society Press (1987)Google Scholar
  46. 46.
    Schneider, D., Leuschel, M., Witt, T.: Model-based problem solving for university timetable validation and improvement. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 487–495. Springer, Cham (2015). Scholar
  47. 47.
    Sedgewick, R., Wayne, K.: Algorithms, 4th edn. Addison-Wesley, Boston (2011)Google Scholar
  48. 48.
    Sommerville, J.: Software Engineering, 10th edn. Pearson, Boston (2016)zbMATHGoogle Scholar
  49. 49.
    Søndergaard, H., Sestoft, P.: Referential transparency, definiteness and unfoldability. Acta Inform. 27, 505–517 (1990)MathSciNetCrossRefGoogle Scholar
  50. 50.
    Turner, D.A.: Functional programming as executable specifications. In: Hoare, C.A.R., Shepherdson, J.C. (eds.) Mathematical Logic and Programming Languages, pp. 29–50. Prentice Hall, Upper Saddle River (1985)Google Scholar
  51. 51.
    Zimmermann, Y., Hallerstede, S., Cansell, D.: Formal modelling of electronic circuits using event-B, Case Study: SAE J1708 Serial Communication Link. In: Mermet, J. (ed.) UML-B - Specification for Proven Embedded Systems Design. Kluwer Academic Publishers, Boston (2004)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Stefan Hallerstede
    • 1
    Email author
  • Peter Gorm Larsen
    • 1
  • John Fitzgerald
    • 2
  1. 1.DIGIT, Department of EngineeringAarhus UniversityAarhusDenmark
  2. 2.School of ComputingNewcastle UniversityNewcastle upon TyneUK

Personalised recommendations