{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,15]],"date-time":"2025-06-15T08:40:03Z","timestamp":1749976803448,"version":"3.41.0"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2017,2,11]],"date-time":"2017-02-11T00:00:00Z","timestamp":1486771200000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2018,4]]},"DOI":"10.1007\/s10009-017-0448-3","type":"journal-article","created":{"date-parts":[[2017,2,11]],"date-time":"2017-02-11T12:52:51Z","timestamp":1486817571000},"page":"211-235","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Automated translation of VDM to JML-annotated Java"],"prefix":"10.1007","volume":"20","author":[{"given":"Peter W. V.","family":"Tran-J\u00f8rgensen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter Gorm","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gary T.","family":"Leavens","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,2,11]]},"reference":[{"key":"448_CR1","volume-title":"Object-Oriented Software Construction","author":"B Meyer","year":"1988","unstructured":"Meyer, B.: Object-Oriented Software Construction. Prentice-Hall International, Upper Saddle River (1988)"},{"key":"448_CR2","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, D., Jones, C. (eds.): The Vienna Development Method: The Meta-Language. Lecture Notes in Computer Science, vol.\u00a061. Springer (1978)","DOI":"10.1007\/3-540-08766-4"},{"key":"448_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511626975","volume-title":"Modelling Systems\u2014Practical Tools and Techniques in Software Development","author":"J Fitzgerald","year":"2009","unstructured":"Fitzgerald, J., Larsen, P.G.: Modelling Systems\u2014Practical Tools and Techniques in Software Development, 2nd edn. Cambridge University Press, Cambridge (2009). doi: 10.1017\/CBO9780511626975","edition":"2"},{"key":"448_CR4","doi-asserted-by":"crossref","unstructured":"Fitzgerald, J.S., Larsen, P.G., Verhoef, M.: Vienna Development Method. Wiley Encyclopedia of Computer Science and Engineering. Wiley (2008)","DOI":"10.1002\/9780470050118.ecse447"},{"key":"448_CR5","unstructured":"Woodcock, J., Davies, J.: Using Z\u2014Specification, Refinement, and Proof. Prentice Hall International Series in Computer Science. Hertfordshire, UK (1996)"},{"key":"448_CR6","volume-title":"Software Development A Rigorous Approach","author":"CB Jones","year":"1980","unstructured":"Jones, C.B.: Software Development A Rigorous Approach. Prentice-Hall International, Englewood Cliffs (1980)"},{"issue":"1","key":"448_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/9758.10500","volume":"9","author":"JM Wing","year":"1987","unstructured":"Wing, J.M.: Writing Larch interface language specifications. ACM Trans. Program. Lang. Syst. 9(1), 1\u201324 (1987). doi: 10.1145\/9758.10500","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"448_CR8","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L Burdy","year":"2005","unstructured":"Burdy, L., Cheon, Y., Cok, D., Ernst, M.D., Kiniry, J.R., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transf. 7, 212\u2013232 (2005)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"1","key":"448_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1668862.1668864","volume":"35","author":"PG Larsen","year":"2010","unstructured":"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\u20136 (2010). doi: 10.1145\/1668862.1668864","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"448_CR10","unstructured":"The Overture tool website. http:\/\/overturetool.org\/ (2015)"},{"key":"448_CR11","unstructured":"J\u00f8rgensen, P.W.V., Couto, L.D., Larsen, M.: A code generation platform for VDM. In: Proceedings of the 12th Overture workshop (2014)"},{"key":"448_CR12","doi-asserted-by":"publisher","unstructured":"Cok, D.: OpenJML: JML for Java 7 by Extending OpenJDK. In: Bobaru, M., Havelund, K., Holzmann, G., Joshi, R. (eds.) NASA Formal Methods. Lecture Notes in Computer Science, vol. 6617, pp. 472\u2013479. Springer, Berlin. doi: 10.1007\/978-3-642-20398-5_35 (2011)","DOI":"10.1007\/978-3-642-20398-5_35"},{"key":"448_CR13","unstructured":"Larsen, P.G., Lausdahl, K., Battle, N., Fitzgerald, J., Wolff, S., Sahara, S., Verhoef, M., Tran-J\u00f8rgensen, P.W.V., Oda, T., Chisholm, P.: The VDM-10 Language Manual. Tech. Rep. TR-2010-06, The Overture Open Source Initiative (2010)"},{"key":"448_CR14","unstructured":"Andrews, D., Bruun, H., Damm, F., Dawes, J., Hansen, B., Larsen, P., Parkin, G., Plat, N., Totenel, H.: A Formal Definition of VDM-SL. Tech. Rep. 1998\/9, Leicester University (1998)"},{"key":"448_CR15","doi-asserted-by":"publisher","unstructured":"Lausdahl, K., Larsen, P.G., Battle, N.: A deterministic interpreter simulating a distributed real time system using VDM. In: Qin, S., Qiu, Z. (eds.) Proceedings of the 13th International Conference on Formal methods and Software Engineering. Lecture Notes in Computer Science, vol. 6991, pp. 179\u2013194. Springer, Berlin. doi: 10.1007\/978-3-642-24559-6_14 . ISBN 978-3-642-24558-9 (2011)","DOI":"10.1007\/978-3-642-24559-6_14"},{"key":"448_CR16","unstructured":"Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C., Cok, D., Kiniry, J.: JML Reference Manual, revision 2344 edn. (2013)"},{"issue":"3","key":"448_CR17","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/j.scico.2006.03.001","volume":"62","author":"P M\u00fcller","year":"2006","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Sci. Comput. Program. 62(3), 253\u2013286 (2006). doi: 10.1016\/j.scico.2006.03.001","journal-title":"Sci. Comput. Program."},{"key":"448_CR18","unstructured":"The Apache Maven Project website. https:\/\/maven.apache.org (2016)"},{"key":"448_CR19","unstructured":"The Overture tool Github repository. https:\/\/github.com\/overturetool\/overture (2016)"},{"key":"448_CR20","doi-asserted-by":"publisher","unstructured":"Yi, J., Robby, Deng, X., Roychoudhury, A.: Past expression: encapsulating pre-states at post-conditions by means of AOP. In: Proceedings of the 12th Annual International Conference on Aspect-oriented Software Development, AOSD \u201913, pp. 133\u2013144. ACM. doi: 10.1145\/2451436.2451453 (2013)","DOI":"10.1145\/2451436.2451453"},{"key":"448_CR21","doi-asserted-by":"crossref","unstructured":"McCarthy, J.: A Basis for a Mathematical Theory of Computation. In: Western Joint Computer Conference (1961)","DOI":"10.1145\/1460690.1460715"},{"key":"448_CR22","unstructured":"Tran-J\u00f8rgensen, P.W.V.: Automated translation of VDM-SL to JML-annotated Java. Department of Engineering, Aarhus University, Tech. rep. (2016)"},{"key":"448_CR23","doi-asserted-by":"publisher","unstructured":"Larsen, P.G., Lausdahl, K., Battle, N.: Combinatorial testing for VDM. In: Proceedings of the 2010 8th IEEE International Conference on Software Engineering and Formal Methods, SEFM \u201910, pp. 278\u2013285. IEEE Computer Society, Washington, DC, USA. doi: 10.1109\/SEFM.2010.32 . ISBN 978-0-7695-4153-2 (2010)","DOI":"10.1109\/SEFM.2010.32"},{"key":"448_CR24","unstructured":"Tran-J\u00f8rgensen, P.W.V., Larsen, P.G., Battle, N.: Using JML-based code generation to enhance test automation for VDM models. In: Proceedings of the 14th Overture Workshop (2016)"},{"key":"448_CR25","doi-asserted-by":"publisher","DOI":"10.1007\/b138800","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, New York (2005). doi: 10.1007\/b138800"},{"key":"448_CR26","unstructured":"Vilhena, C.: Connecting between VDM++ and JML. Master\u2019s thesis, Minho University with exchange to Engineering College of Aarhus (2008)"},{"key":"448_CR27","doi-asserted-by":"crossref","unstructured":"Jin, D., Yang, Z.: Strategies of modeling from VDM-SL to JML. In: International Conference on Advanced Language Processing and Web Information Technology, pp. 320\u2013323 (2008)","DOI":"10.1109\/ALPIT.2008.25"},{"key":"448_CR28","volume-title":"Unified Modeling Language Reference Manual","author":"J Rumbaugh","year":"2004","unstructured":"Rumbaugh, J., Jacobson, I., Booch, G.: Unified Modeling Language Reference Manual, 2nd edn. Pearson Higher Education, Boston (2004)","edition":"2"},{"key":"448_CR29","doi-asserted-by":"crossref","unstructured":"Zhou, J., Jin, D.: Research on modeling from VDM-SL to JML for systematic software development. Control and Decision Conference (CCDC). 2010 Chinese, pp. 2312\u20132317. IEEE, Xuzhou (2010)","DOI":"10.1109\/CCDC.2010.5498815"},{"issue":"8","key":"448_CR30","first-page":"692","volume":"7","author":"PG Larsen","year":"2001","unstructured":"Larsen, P.G.: Ten years of historical development: \u201cBootstrapping\u201d VDMTools. J. Univers. Comput. Sci. 7(8), 692\u2013709 (2001)","journal-title":"J. Univers. Comput. Sci."},{"key":"448_CR31","doi-asserted-by":"crossref","unstructured":"Rivera, V., Cata\u00f1o, N., Wahls, T., Rueda, C.: Code generation for event-B. Int. J. Softw. Tools Technol. Transf. 19:1\u201322 (2015)","DOI":"10.1007\/s10009-015-0381-2"},{"key":"448_CR32","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"key":"448_CR33","doi-asserted-by":"publisher","unstructured":"Lensink, L., Smetsers, S., van Eekelen, M.: Generating verifiable Java code from verified PVS specifications. In: Goodloe, A., Person, S. (eds.) NASA Formal Methods. Lecture Notes in Computer Science, vol. 7226, pp. 310\u2013325. Springer, Berlin. doi: 10.1007\/978-3-642-28891-3_30 (2012)","DOI":"10.1007\/978-3-642-28891-3_30"},{"key":"448_CR34","doi-asserted-by":"crossref","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) 11th International Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 607, pp. 748\u2013752. Springer, Saratoga (1992)","DOI":"10.1007\/3-540-55602-8_217"},{"key":"448_CR35","unstructured":"Filli\u00e2tre, J.C.: Why: a multi-language multi-prover verification tool. Research Report 1366, LRI, Universit\u00e9 Paris Sud. http:\/\/www.lri.fr\/~filliatr\/ftp\/publis\/why-tool.ps.gz (2003)"},{"key":"448_CR36","unstructured":"Hubbers, E., Oostdijk, M.: Generating JML specifications from UML state diagrams. In: Forum on Specification and Design Languages FDL\u201903, Frankfurt, Germany, pp 263\u2013273, September 23\u201326, 2003"},{"key":"448_CR37","volume-title":"Java Card Technology for Smart Cards","author":"Z Zhen","year":"2000","unstructured":"Zhen, Z.: Java Card Technology for Smart Cards. Prentice-Hall, Boston (2000)"},{"key":"448_CR38","doi-asserted-by":"crossref","unstructured":"Klebanov, A.: Automata-based programming technology extension for generation of JML annotated Java card code. In: Proceedings of the Spring\/Summer Young Researchers\u2019 Colloquium on Software Engineering, pp. 41\u201344 (2008)","DOI":"10.15514\/SYRCOSE-2008-2-8"},{"issue":"8","key":"448_CR39","doi-asserted-by":"crossref","first-page":"77","DOI":"10.5381\/jot.2005.4.8.a4","volume":"4","author":"DR Cok","year":"2005","unstructured":"Cok, D.R.: Reasoning with specifications containing method calls and model fields. J. Object Technol. 4(8), 77\u2013103 (2005)","journal-title":"J. Object Technol."}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-017-0448-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0448-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-017-0448-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,15]],"date-time":"2025-06-15T08:17:30Z","timestamp":1749975450000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-017-0448-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,2,11]]},"references-count":39,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2018,4]]}},"alternative-id":["448"],"URL":"https:\/\/doi.org\/10.1007\/s10009-017-0448-3","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2017,2,11]]}}}