{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T19:43:24Z","timestamp":1743018204711,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319471686"},{"type":"electronic","value":"9783319471693"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-47169-3_17","type":"book-chapter","created":{"date-parts":[[2016,10,4]],"date-time":"2016-10-04T17:56:23Z","timestamp":1475603783000},"page":"238-257","source":"Crossref","is-referenced-by-count":14,"title":["Towards a Unified View of Modeling and Programming"],"prefix":"10.1007","author":[{"given":"Manfred","family":"Broy","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Klaus","family":"Havelund","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rahul","family":"Kumar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,10,5]]},"reference":[{"key":"17_CR1","unstructured":"Documents associated with Object Constraint Language (OCL), Version 2.4. http:\/\/www.omg.org\/spec\/OCL\/2.4 . Accessed 29 June 2016"},{"key":"17_CR2","unstructured":"EMF. http:\/\/www.eclipse.org\/modeling\/emf\/ . Accessed 6 July 2016"},{"key":"17_CR3","unstructured":"Mathematica. https:\/\/www.wolfram.com\/mathematica . Accessed 29 June 2016"},{"key":"17_CR4","unstructured":"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"},{"key":"17_CR5","unstructured":"OCLInEcore. https:\/\/wiki.eclipse.org\/OCL\/OCLinEcore . Accessed 28 June 2016"},{"key":"17_CR6","unstructured":"OCLInEcore online tutorial. http:\/\/goo.gl\/wR2HvP . Accessed 28 June 2016"},{"key":"17_CR7","unstructured":"OMG Systems Modeling Language (SysML). http:\/\/www.omgsysml.org . Accessed 12 July 2016"},{"key":"17_CR8","unstructured":"OMG Unified Modeling Language (UML). http:\/\/www.omg.org\/spec\/UML . Accessed: 12 July 2016"},{"key":"17_CR9","unstructured":"The Coq Theorem Prover. https:\/\/coq.inria.fr . Accessed: 12 July 2016"},{"key":"17_CR10","unstructured":"The Isabelle Theorem Prover. https:\/\/isabelle.in.tum.de . Accessed 12 July 2016"},{"key":"17_CR11","unstructured":"The PVS Theorem prover. http:\/\/pvs.csl.sri.com . Accessed 12 July 2016"},{"key":"17_CR12","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B","author":"J-R Abrial","year":"2010","unstructured":"Abrial, J.-R.: Modeling in Event-B. Cambridge University Press, New York (2010)"},{"key":"17_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-08766-4","volume-title":"The Vienna Development Method: The Meta-Language","author":"D Bj\u00f8rner","year":"1978","unstructured":"Bj\u00f8rner, D., Jones, C.B.: The Vienna Development Method: The Meta-Language. Lecture Notes in Computer Science, vol. 61. Springer, Heidelberg (1978)"},{"key":"17_CR14","volume-title":"Formal Specification and Software Development","author":"D Bj\u00f8rner","year":"1982","unstructured":"Bj\u00f8rner, D., Jones, C.B.: Formal Specification and Software Development. Prentice Hall International, Upper Saddle River (1982). ISBN: 0-13-880733-7"},{"key":"17_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/11780274_25","volume-title":"Algebra, Meaning, and Computation","author":"M Broy","year":"2006","unstructured":"Broy, M.: From chaos to undefinedness. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol. 4060, pp. 476\u2013496. Springer, Heidelberg (2006). doi: 10.1007\/11780274_25"},{"key":"17_CR16","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Upper Saddle River (1976)"},{"key":"17_CR17","doi-asserted-by":"crossref","unstructured":"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\u2013363, September 2009","DOI":"10.3384\/ecp09430096"},{"key":"17_CR18","volume-title":"Validated Designs For Object-Oriented Systems","author":"J Fitzgerald","year":"2005","unstructured":"Fitzgerald, J., Larsen, P.G., Mukherjee, P., Plat, N., Verhoef, M.: Validated Designs For Object-Oriented Systems. Springer, Santa Clara (2005)"},{"key":"17_CR19","doi-asserted-by":"crossref","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J. (ed.) Mathematical Aspects of Computer Science, Proceedings of Symposium in Applied Mathematics, pp. 19\u201332. American Mathematical Society, Rhode Island (1967)","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"17_CR20","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/0004-3702(82)90020-0","volume":"19","author":"C Forgy","year":"1982","unstructured":"Forgy, C.: Rete: a fast algorithm for the many pattern\/many object pattern match problem. Artif. Intell. 19, 17\u201337 (1982)","journal-title":"Artif. Intell."},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Futatsugi, K., Goguen, J.A., Jouannaud, J.-P., Meseguer, J.: Principles of OBJ2. In: POPL (1985)","DOI":"10.1145\/318593.318610"},{"key":"17_CR22","series-title":"The BCS Practitioner Series","volume-title":"The RAISE Specification Language","author":"C George","year":"1992","unstructured":"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)"},{"key":"17_CR23","unstructured":"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"},{"key":"17_CR24","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1007\/s10009-014-0309-2","volume":"17","author":"K Havelund","year":"2015","unstructured":"Havelund, K.: Rule-based runtime verification revisited. Softw. Tools Technol. Transf. (STTT) 17, 143\u2013170 (2015)","journal-title":"Softw. Tools Technol. Transf. (STTT)"},{"key":"17_CR25","series-title":"Communications in Computer and Information Science","volume-title":"Formal Techniques for Safety-Critical Systems","author":"K Havelund","year":"2015","unstructured":"Havelund, K., Joshi, R.: Experience with rule-based analysis of spacecraft logs. In: Artho, C., \u00d6lveczky, P.C. (eds.) Formal Techniques for Safety-Critical Systems. Communications in Computer and Information Science, vol. 476. Springer, Switzerland (2015)"},{"key":"17_CR26","doi-asserted-by":"crossref","unstructured":"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\u2013122. Scitepress Digital Library, February 2016","DOI":"10.5220\/0005741401110122"},{"issue":"4","key":"17_CR27","doi-asserted-by":"crossref","first-page":"366","DOI":"10.1007\/s100090050043","volume":"2","author":"K Havelund","year":"2000","unstructured":"Havelund, K., Pressburger, T.: Model checking Java programs using Java PathFinder. Int. J. Softw. Tools Technol. Transf. STTT 2(4), 366\u2013381 (2000)","journal-title":"Int. J. Softw. Tools Technol. Transf. STTT"},{"issue":"1","key":"17_CR28","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1007\/s10009-002-0080-7","volume":"4","author":"K Havelund","year":"2002","unstructured":"Havelund, K., Visser, W.: Program model checking as a new trend. STTT 4(1), 8\u201320 (2002)","journal-title":"STTT"},{"key":"17_CR29","doi-asserted-by":"crossref","first-page":"567","DOI":"10.1145\/363235.363255","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis of computer programming. Commun. ACM 12, 567\u2013583 (1969)","journal-title":"Commun. ACM"},{"key":"17_CR30","volume-title":"The Spin Model Checker - Primer and Reference Manual","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J.: The Spin Model Checker - Primer and Reference Manual. Addison-Wesley, Boston (2004)"},{"key":"17_CR31","volume-title":"Systematic Software Development using VDM","author":"CB Jones","year":"1990","unstructured":"Jones, C.B.: Systematic Software Development using VDM. Prentice Hall, Englewood Cliffs (1990). ISBN: 0-13-880733-7"},{"key":"17_CR32","doi-asserted-by":"crossref","first-page":"872","DOI":"10.1145\/177492.177726","volume":"16","author":"L Lamport","year":"1994","unstructured":"Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16, 872\u2013923 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR33","doi-asserted-by":"crossref","first-page":"134","DOI":"10.1007\/s100090050010","volume":"1","author":"KG Larsen","year":"1997","unstructured":"Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. STTT 1, 134\u2013152 (1997)","journal-title":"STTT"},{"key":"17_CR34","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1145\/367177.367199","volume":"3","author":"J McCarthy","year":"1960","unstructured":"McCarthy, J.: Recursive functions of symbolic expressions and their computation by machines, part I. Commun. ACM 3, 184\u2013195 (1960)","journal-title":"Commun. ACM"},{"key":"17_CR35","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: Popplewell, C. (ed.) IFIP World Congress Proceedings, pp. 21\u201328 (1962)"},{"key":"17_CR36","first-page":"19","volume":"21","author":"D Scott","year":"1971","unstructured":"Scott, D., Strachey, C.: Towards a mathematical semantics for computer languages. Comput. Automata Microwave Res. Inst. Symp. 21, 19\u201346 (1971)","journal-title":"Comput. Automata Microwave Res. Inst. Symp."},{"key":"17_CR37","series-title":"International Series in Computer Science","volume-title":"The Z Notation - a Reference Manual","author":"JM Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation - a Reference Manual. International Series in Computer Science, 2nd edn. Prentice Hall, Hemel Hempstead (1992)","edition":"2"},{"key":"17_CR38","unstructured":"The CIP Language Group. The Munich Project CIP Volume I: The Wide Spectrum Language CIP-L. LNCS, vol. 183. Springer (1985)"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-47169-3_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T20:21:56Z","timestamp":1498335716000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-47169-3_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319471686","9783319471693"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-47169-3_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}