Abstract
In this paper we argue that there is a value in providing a unified view of modeling and programming. Models are meant to describe a system at a high level of abstraction for the purpose of human understanding and analysis. Programs, on the other hand, are meant for execution. However, programming languages are becoming increasingly higher-level, with convenient notation for concepts that in the past would only be reserved formal specification languages. This leads to the observation, that programming languages could be used for modeling, if only appropriate modifications were made to these languages. At the same time, model-based engineering formalisms such as UML and SysML are highly popular in engineering communities due to their graphical nature. However, these communities are, due to the complex nature of these formalisms, struggling to find grounds in textual formalisms with proper semantics. A unified view of modeling and programming may provide a common ground. The paper illustrates these points with selected examples comparing models and programs.
K. Havelund—The research performed by this author was carried out at Jet Propulsion Laboratory, California Institute of Technology, under a contract with the National Aeronautics and Space Administration.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
This characteristic of the difference is somewhat simplified since a VDM specification in fact also can denote more than one model.
- 2.
This is an example of a discussion about semantics that can throw a project meeting off its course.
- 3.
Note that the constraint can actually be avoided in Z by defining the type of
to be \(\mathbb {N}_1\), the natural numbers starting from 1.
to be References
Documents associated with Object Constraint Language (OCL), Version 2.4. http://www.omg.org/spec/OCL/2.4. Accessed 29 June 2016
EMF. http://www.eclipse.org/modeling/emf/. Accessed 6 July 2016
Mathematica. https://www.wolfram.com/mathematica. Accessed 29 June 2016
Modelica - A Unified Object-Oriented Language for Systems Modeling. Language Specification Version 3.3. https://www.modelica.org/documents/ModelicaSpec33.pdf. Accessed 29 June 2016
OCLInEcore. https://wiki.eclipse.org/OCL/OCLinEcore. Accessed 28 June 2016
OCLInEcore online tutorial. http://goo.gl/wR2HvP. Accessed 28 June 2016
OMG Systems Modeling Language (SysML). http://www.omgsysml.org. Accessed 12 July 2016
OMG Unified Modeling Language (UML). http://www.omg.org/spec/UML. Accessed: 12 July 2016
The Coq Theorem Prover. https://coq.inria.fr. Accessed: 12 July 2016
The Isabelle Theorem Prover. https://isabelle.in.tum.de. Accessed 12 July 2016
The PVS Theorem prover. http://pvs.csl.sri.com. Accessed 12 July 2016
Abrial, J.-R.: Modeling in Event-B. Cambridge University Press, New York (2010)
Bjørner, D., Jones, C.B.: The Vienna Development Method: The Meta-Language. Lecture Notes in Computer Science, vol. 61. Springer, Heidelberg (1978)
Bjørner, D., Jones, C.B.: Formal Specification and Software Development. Prentice Hall International, Upper Saddle River (1982). ISBN: 0-13-880733-7
Broy, M.: From chaos to undefinedness. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol. 4060, pp. 476–496. Springer, Heidelberg (2006). doi:10.1007/11780274_25
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Upper Saddle River (1976)
Elmqvist, H., Otter, M., Henriksson, D., Thiele, B., Mattsson, S.E.: Modelica for embedded systems. In: Proceedings of the 7th Modelica Conference, Como, Italy, pp. 354–363, September 2009
Fitzgerald, J., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M.: Validated Designs For Object-Oriented Systems. Springer, Santa Clara (2005)
Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J. (ed.) Mathematical Aspects of Computer Science, Proceedings of Symposium in Applied Mathematics, pp. 19–32. American Mathematical Society, Rhode Island (1967)
Forgy, C.: Rete: a fast algorithm for the many pattern/many object pattern match problem. Artif. Intell. 19, 17–37 (1982)
Futatsugi, K., Goguen, J.A., Jouannaud, J.-P., Meseguer, J.: Principles of OBJ2. In: POPL (1985)
George, C., Haff, P., Havelund, K., Haxthausen, A., Milne, R., Nielsen, C.B., Prehn, S., Wagner, K.R.: The RAISE Specification Language. The BCS Practitioner Series. Prentice-Hall, Hemel Hampstead (1992)
Havelund, K.: Closing the gap between specification and programming: VDM\(^{++}\) and Scala. In: Korovina, M., Voronkov, A. (eds.) HOWARD-60: Higher-Order Workshop on Automated Runtime Verification and Debugging, EasyChair Proceedings, vol. 1, Manchester, UK, December 2011
Havelund, K.: Rule-based runtime verification revisited. Softw. Tools Technol. Transf. (STTT) 17, 143–170 (2015)
Havelund, K., Joshi, R.: Experience with rule-based analysis of spacecraft logs. In: Artho, C., Ölveczky, P.C. (eds.) Formal Techniques for Safety-Critical Systems. Communications in Computer and Information Science, vol. 476. Springer, Switzerland (2015)
Havelund, K., Kumar, R., Delp, C., Clement, B., K: a wide spectrum language for modeling, programming and analysis. In: Proceedings of the 4th International Conference on Model-Driven Engineering and Software Development (MODELSWARD), Rome, Italy, pp. 111–122. Scitepress Digital Library, February 2016
Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. Int. J. Softw. Tools Technol. Transf. STTT 2(4), 366–381 (2000)
Havelund, K., Visser, W.: Program model checking as a new trend. STTT 4(1), 8–20 (2002)
Hoare, C.A.R.: An axiomatic basis of computer programming. Commun. ACM 12, 567–583 (1969)
Holzmann, G.J.: The Spin Model Checker - Primer and Reference Manual. Addison-Wesley, Boston (2004)
Jones, C.B.: Systematic Software Development using VDM. Prentice Hall, Englewood Cliffs (1990). ISBN: 0-13-880733-7
Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16, 872–923 (1994)
Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. STTT 1, 134–152 (1997)
McCarthy, J.: Recursive functions of symbolic expressions and their computation by machines, part I. Commun. ACM 3, 184–195 (1960)
McCarthy, J.: Towards a mathematical science of computation. In: Popplewell, C. (ed.) IFIP World Congress Proceedings, pp. 21–28 (1962)
Scott, D., Strachey, C.: Towards a mathematical semantics for computer languages. Comput. Automata Microwave Res. Inst. Symp. 21, 19–46 (1971)
Spivey, J.M.: The Z Notation - a Reference Manual. International Series in Computer Science, 2nd edn. Prentice Hall, Hemel Hempstead (1992)
The CIP Language Group. The Munich Project CIP Volume I: The Wide Spectrum Language CIP-L. LNCS, vol. 183. Springer (1985)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Broy, M., Havelund, K., Kumar, R. (2016). Towards a Unified View of Modeling and Programming. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications. ISoLA 2016. Lecture Notes in Computer Science(), vol 9953. Springer, Cham. https://doi.org/10.1007/978-3-319-47169-3_17
Download citation
DOI: https://doi.org/10.1007/978-3-319-47169-3_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-47168-6
Online ISBN: 978-3-319-47169-3
eBook Packages: Computer ScienceComputer Science (R0)