{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T22:40:04Z","timestamp":1746139204037,"version":"3.40.4"},"publisher-location":"Cham","reference-count":12,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319049144"},{"type":"electronic","value":"9783319049151"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-04915-1_9","type":"book-chapter","created":{"date-parts":[[2014,2,20]],"date-time":"2014-02-20T15:12:22Z","timestamp":1392909142000},"page":"118-131","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["SOFL Specification Animation with Tool Support"],"prefix":"10.1007","author":[{"given":"Mo","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shaoying","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2014,2,21]]},"reference":[{"issue":"5","key":"9_CR1","doi-asserted-by":"publisher","first-page":"599","DOI":"10.1016\/S1389-1286(02)00354-7","volume":"40","author":"P Combes","year":"2002","unstructured":"Combes, P., Dubois, F., Renard, B.: An open animation tool: application to telecommunication systems. Int. J. Comput. Telecommun. Netw. 40(5), 599\u2013620 (2002)","journal-title":"Int. J. Comput. Telecommun. Netw."},{"key":"9_CR2","doi-asserted-by":"crossref","unstructured":"Waeselynck, H., Behnia, S.: B model animation for external verification. In: Proceedings of the Second IEEE International Conference on Formal Engineering Methods, pp. 36\u201345 (1998)","DOI":"10.1109\/ICFEM.1998.730568"},{"issue":"3","key":"9_CR3","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S0164-1212(97)10016-4","volume":"41","author":"I Morrey","year":"1998","unstructured":"Morrey, I., Siddiqi, J., Hibberd, R., Buckberry, G.: A toolset to support the construction and animation of formal specifications. J. Syst. Softw. 41(3), 147\u2013160 (1998)","journal-title":"J. Syst. Softw."},{"key":"9_CR4","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07287-5","volume-title":"Formal Engineering for Industrial Software Development Using the SOFL Method","author":"S Liu","year":"2004","unstructured":"Liu, S.: Formal Engineering for Industrial Software Development Using the SOFL Method. Springer, Heidelberg (2004). ISBN 3-540-20602-7"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"Liu, S., Nakajima, S.: A Decompositional approach to automatic test case generation based on formal specification. In: Fourth IEEE International Conference on Secure Software Integration and Reliability Improvement, pp. 147\u2013155 (2010)","DOI":"10.1109\/SSIRI.2010.11"},{"key":"9_CR6","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/APSEC.2012.115","volume-title":"In: Proceedings of the 19th Asia-Pacific Software Engineering Conference (APSEC 2012)","author":"M Li","year":"2012","unstructured":"Li, M., Liu, S.: Automated functional scenarios-based formal specification animation. In: Proceedings of the 19th Asia-Pacific Software Engineering Conference (APSEC 2012), pp. 107\u2013115. IEEE CS Press, Hong Kong (2012)"},{"key":"9_CR7","doi-asserted-by":"publisher","first-page":"1271","DOI":"10.1016\/j.jss.2006.12.540","volume":"80","author":"S Liu","year":"2007","unstructured":"Liu, S., Wang, H.: An automated approach to specification animation for validation. J. Syst. Softw. 80, 1271\u20131285 (2007)","journal-title":"J. Syst. Softw."},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"Li, M., Liu, S.: Automatically generating functional scenarios from SOFL CDFD for specification inspection. In: 10th IASTED International Conference on Software Engineering, Innsbruck, Austria, pp. 18\u201325 (2011)","DOI":"10.2316\/P.2011.720-057"},{"issue":"5","key":"9_CR9","doi-asserted-by":"publisher","first-page":"665","DOI":"10.1016\/S1389-1286(02)00356-0","volume":"40","author":"B Stepien","year":"2002","unstructured":"Stepien, B., Logrippo, L.: Graphic visualization and animation of LOTOS execution traces. Comput. Netw.: Int. J. Comput. Telecommun. Netw. 40(5), 665\u2013681 (2002)","journal-title":"Comput. Netw.: Int. J. Comput. Telecommun. Netw."},{"issue":"2","key":"9_CR10","first-page":"259","volume":"21","author":"S Liu","year":"2011","unstructured":"Liu, S., Chen, Y., Nagoya, F., McDermid, J.A.: Formal specification-based inspection for verification of programs. IEEE Trans. Softw. Eng. 21(2), 259\u2013288 (2011). IEEE Computer Society Digital Library, IEEE Computer Society","journal-title":"IEEE Trans. Softw. Eng."},{"key":"9_CR11","series-title":"LNCS","first-page":"136","volume-title":"ICFEM 2007","author":"S Liu","year":"2007","unstructured":"Liu, S.: Integrating specification-based review and testing for detecting errors in programs. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) ICFEM 2007. LNCS, vol. 4789, pp. 136\u2013150. Springer, Heidelberg (2007)"},{"key":"9_CR12","series-title":"LNCS","first-page":"192","volume-title":"ICFEM 2002","author":"T Miller","year":"2002","unstructured":"Miller, T., Strooper, P.: Model-based specification animation using testgraphs. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 192\u2013203. Springer, Heidelberg (2002)"}],"container-title":["Lecture Notes in Computer Science","Structured Object-Oriented Formal Language and Method"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-04915-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,1]],"date-time":"2025-05-01T22:07:26Z","timestamp":1746137246000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-04915-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319049144","9783319049151"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-04915-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]},"assertion":[{"value":"21 February 2014","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}