{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T21:51:39Z","timestamp":1743112299533,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319295091"},{"type":"electronic","value":"9783319295107"}],"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-29510-7_14","type":"book-chapter","created":{"date-parts":[[2016,1,29]],"date-time":"2016-01-29T14:39:16Z","timestamp":1454078356000},"page":"241-256","source":"Crossref","is-referenced-by-count":1,"title":["Towards Verifying VDM Using SPIN"],"prefix":"10.1007","author":[{"given":"Hsin-Hung","family":"Lin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yoichi","family":"Omori","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shigeru","family":"Kusakabe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Keijiro","family":"Araki","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,1,30]]},"reference":[{"key":"14_CR1","unstructured":"VDMJ. http:\/\/sourceforge.net\/projects\/vdmj\/"},{"key":"14_CR2","unstructured":"Agerholm, S., Larsen, P.G.: Modeling and validating SAFER in VDM-SL. In: Proceedings of the Fourth NASA Langley Formal Methods Workshop, NASA Conference, Publication 3356 (1997)"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science","volume-title":"The Vienna Development Method: The Meta-Language","year":"1978","unstructured":"Bjorner, D., Jones, C.B. (eds.): The Vienna Development Method: The Meta-Language. LNCS, vol. 61. Springer, Heidelberg (1978)"},{"key":"14_CR4","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"14_CR5","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511626975","volume-title":"Modelling Systems: Practical Tools and Techniques in Software Development","author":"J Fitzgerald","year":"2009","unstructured":"Fitzgerald, J., Larsen, P.G.: Modelling Systems: Practical Tools and Techniques in Software Development, 2nd edn. Cambridge University Press, New York (2009)","edition":"2"},{"key":"14_CR6","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)"},{"issue":"2","key":"14_CR7","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/1361213.1361214","volume":"43","author":"J Fitzgerald","year":"2008","unstructured":"Fitzgerald, J., Larsen, P.G., Sahara, S.: VDMTools: advances in support for formal modeling in VDM. SIGPLAN Not. 43(2), 3\u201311 (2008)","journal-title":"SIGPLAN Not."},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/3-540-60973-3_87","volume-title":"FME 1996: Industrial Benefit and Advances in Formal Methods","author":"B Fr\u00f6hlich","year":"1996","unstructured":"Fr\u00f6hlich, B., Larsen, P.: Combining VDM-SL specifications with C++ code. In: Gaudel, M.C., Woodcock, J. (eds.) FME 1996. LNCS, vol. 1051, pp. 179\u2013194. Springer, Heidelberg (1996)"},{"key":"14_CR9","unstructured":"Holzmann, G.: SPIN Model Checker: The Primer and Reference Manual. Addison-Wesley Professional, Reading (2003)"},{"issue":"2","key":"14_CR10","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1145\/2560217.2560218","volume":"57","author":"GJ Holzmann","year":"2014","unstructured":"Holzmann, G.J.: Mars code. Commun. ACM 57(2), 64\u201373 (2014)","journal-title":"Commun. ACM"},{"issue":"6","key":"14_CR11","doi-asserted-by":"publisher","first-page":"845","DOI":"10.1109\/TSE.2010.110","volume":"37","author":"GJ Holzmann","year":"2011","unstructured":"Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification techniques. IEEE Trans. Softw. Eng. 37(6), 845\u2013857 (2011)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-540-24732-6_6","volume-title":"Model Checking Software","author":"GJ Holzmann","year":"2004","unstructured":"Holzmann, G.J., Joshi, R.: Model-driven software verification. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 76\u201391. Springer, Heidelberg (2004)"},{"key":"14_CR13","volume-title":"Systematic Software Development Using VDM","author":"CB Jones","year":"1990","unstructured":"Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. Prentice-Hall Inc, Upper Saddle River (1990)","edition":"2"},{"key":"14_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-540-68237-0_31","volume-title":"FM 2008: Formal Methods","author":"T Kurita","year":"2008","unstructured":"Kurita, T., Chiba, M., Nakatsugawa, Y.: Application of a formal specification language in the development of the \u201cMobile FeliCa\u201d IC chip firmware for embedding in mobile phone. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 425\u2013429. Springer, Heidelberg (2008)"},{"issue":"2\u20133","key":"14_CR15","first-page":"343","volume":"3","author":"T Kurita","year":"2009","unstructured":"Kurita, T., Nakatsugawa, Y.: The application of VDM to the industrial development of firmware for a smart card IC chip. Int. J. Softw. Inf. 3(2\u20133), 343\u2013355 (2009)","journal-title":"Int. J. Softw. Inf."},{"issue":"1","key":"14_CR16","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)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Larsen, P.G., Fitzgerald, J.: Recent industrial applications of VDM in Japan. In: Proceedings of the 2007th Internatioanal Conference on Formal Methods in Industry, FACS-FMI 2007, p. 8. British Computer Society, Swinton (2007)","DOI":"10.14236\/ewic\/FMI2007.8"},{"issue":"5\u20136","key":"14_CR18","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1016\/0920-5489(95)00026-Q","volume":"17","author":"PG Larsen","year":"1995","unstructured":"Larsen, P.G., Pawlowski, W.: The formal semantics of ISO VDM-SL. Comput. Stand. Interfaces 17(5\u20136), 585\u2013601 (1995)","journal-title":"Comput. Stand. Interfaces"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"604","DOI":"10.1007\/3-540-54834-3_36","volume-title":"Formal Software Development Methods","author":"P Larsen","year":"1991","unstructured":"Larsen, P., Lassen, P.: An executable subset of meta-IV with loose specification. In: Prehn, S., Toetenel, W. (eds.) VDM 1991. LNCS, vol. 551, pp. 604\u2013618. Springer, Berlin Heidelberg (1991)"},{"key":"14_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1007\/978-3-642-38613-8_4","volume-title":"Integrated Formal Methods","author":"K Lausdahl","year":"2013","unstructured":"Lausdahl, K.: Translating VDM to alloy. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 46\u201360. Springer, Heidelberg (2013)"},{"key":"14_CR21","unstructured":"Lausdahl, K., Ishikawa, H., Larsen, P.G.: Interpreting implicit VDM specifications using ProB. In: Battle, N., Fitzgerald, J. (eds.) Proceedings of the 12th Overture Workshop, Newcastle University, 21 June, 2014. School of Computing Science, Newcastle University, UK, Technical report CS-TR-1446, January 2015"},{"key":"14_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"855","DOI":"10.1007\/978-3-540-45236-2_46","volume-title":"Formal Methods","author":"M Leuschel","year":"2003","unstructured":"Leuschel, M., Butler, M.: ProB: a model checker for B. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 855\u2013874. Springer, Berlin Heidelberg (2003)"},{"key":"14_CR23","doi-asserted-by":"crossref","unstructured":"Nakatsugawa, Y., Kurita, T., Araki, K.: A framework for formal specification considering review and specification-based testing. In: TENCON 2010\u20132010 IEEE Region 10 Conference, pp. 2444\u20132448, November 2010","DOI":"10.1109\/TENCON.2010.5685922"},{"key":"14_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-642-30885-7_19","volume-title":"Abstract State Machines, Alloy, B, VDM, and Z","author":"K Lausdahl","year":"2012","unstructured":"Lausdahl, K., Larsen, P.G., Nielsen, C.B.: Combining VDM with executable code. In: Derrick, J., Fitzgerald, J., Gnesi, S., Khurshid, S., Leuschel, M., Reeves, S., Riccobene, E. (eds.) ABZ 2012. LNCS, vol. 7316, pp. 266\u2013279. Springer, Heidelberg (2012)"},{"key":"14_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-642-29822-6_24","volume-title":"Functional and Logic Programming","author":"M Triska","year":"2012","unstructured":"Triska, M.: The finite domain constraint solver of SWI-Prolog. In: Schrijvers, T., Thiemann, P. (eds.) FLOPS 2012. LNCS, vol. 7294, pp. 307\u2013316. Springer, Heidelberg (2012)"},{"key":"14_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/11813040_11","volume-title":"FM 2006: Formal Methods","author":"PG Larsen","year":"2006","unstructured":"Larsen, P.G., Hooman, J., Verhoef, M.: Modeling and Validating Distributed Embedded Real-Time Systems with VDM++. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 147\u2013162. Springer, Heidelberg (2006)"}],"container-title":["Communications in Computer and Information Science","Formal Techniques for Safety-Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29510-7_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,14]],"date-time":"2020-09-14T16:14:36Z","timestamp":1600100076000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29510-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319295091","9783319295107"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29510-7_14","relation":{},"ISSN":["1865-0929","1865-0937"],"issn-type":[{"type":"print","value":"1865-0929"},{"type":"electronic","value":"1865-0937"}],"subject":[],"published":{"date-parts":[[2016]]}}}