{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T23:27:52Z","timestamp":1743118072503,"version":"3.40.3"},"publisher-location":"Cham","reference-count":16,"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_10","type":"book-chapter","created":{"date-parts":[[2014,2,20]],"date-time":"2014-02-20T15:12:22Z","timestamp":1392909142000},"page":"135-153","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["An Approach to Declaring Data Types for Formal Specifications"],"prefix":"10.1007","author":[{"given":"Xi","family":"Wang","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":"1","key":"10_CR1","first-page":"1","volume":"35","author":"LP Gorm","year":"2010","unstructured":"Gorm, L.P., Nick, B., Miguel, F., John, F., Kenneth, L., Marcel, V.: The overture initiative integrating tools for vdm. SIGSOFT Softw. Eng. Notes 35(1), 1\u20136 (2010)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Chen, J., Durnota, B.: Type checking classes in object-z to promote quality of specifications (1994)","DOI":"10.1007\/978-0-387-34848-3_15"},{"issue":"9","key":"10_CR3","doi-asserted-by":"publisher","first-page":"753","DOI":"10.1093\/comjnl\/37.9.753","volume":"37","author":"S Vadera","year":"1994","unstructured":"Vadera, S., Meziane, F.: From English to formal specifications. Comput. J. 37(9), 753\u2013763 (1994)","journal-title":"Comput. J."},{"key":"10_CR4","series-title":"LNCS","first-page":"662","volume-title":"ICFEM 2010","author":"X Wang","year":"2010","unstructured":"Wang, X., Liu, S., Miao, H.: A pattern system to support refining informal ideas into formal expressions. In: Dong, J.S., Zhu, H. (eds.) ICFEM 2010. LNCS, vol. 6447, pp. 662\u2013677. Springer, Heidelberg (2010)"},{"key":"10_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07287-5","volume-title":"Formal Engineering for Industrial Software Development","author":"S Liu","year":"2004","unstructured":"Liu, S.: Formal Engineering for Industrial Software Development. Springer, Heidelberg (2004)"},{"issue":"1","key":"10_CR6","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/32.663996","volume":"24","author":"S Liu","year":"1998","unstructured":"Liu, S., Offutt, A., Ho-Stuart, C., Sun, Y., Ohba, M.: Sofl: a formal engineering methodology for industrial applications. IEEE Trans. Softw. Eng. 24(1), 24\u201345 (1998)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10_CR7","unstructured":"http:\/\/spivey.oriel.ox.ac.uk\/mike\/fuzz\/"},{"issue":"2","key":"10_CR8","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1145\/1361213.1361214","volume":"43","author":"F John","year":"2008","unstructured":"John, F., Gorm, L.P., Shin, S.: Vdmtools: advances in support for formal modeling in vdm. SIGPLAN Not. 43(2), 3\u201311 (2008)","journal-title":"SIGPLAN Not."},{"key":"10_CR9","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modelling in Event-B: System and Software Design","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R.: Modelling in Event-B: System and Software Design. Cambridge University Press, Cambridge (2010)"},{"key":"10_CR10","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"JR Abrial","year":"2010","unstructured":"Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T., Mehta, F., Voisin, L.: Rodin: an open toolset for modelling and reasoning in event-b. Int. J. Softw. Tools Technol. Transf. (STTT) 12, 447\u2013466 (2010). doi:10.1007\/s10009-010-0145-y. http:\/\/dx.doi.org\/10.1007\/s10009-010-0145-y (Online)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"10_CR11","series-title":"LNCS","first-page":"22","volume-title":"TPHOLs 2008","author":"S Owre","year":"2008","unstructured":"Owre, S., Shankar, N.: A brief overview of PVS. In: Ait Mohamed, O., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 22\u201327. Springer, Heidelberg (2008)"},{"issue":"9","key":"10_CR12","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1109\/32.713327","volume":"24","author":"J Rushby","year":"1998","unstructured":"Rushby, J., Owre, S., Shankar, N.: Subtypes for specifications: predicate subtyping in pvs. IEEE Trans. Softw. Eng. 24(9), 709\u2013720 (1998)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"10_CR13","unstructured":"Tan, X., Wang, Y., Ngolah, C.: A novel type checker for software system specifications in rtpa. In: Canadian Conference on Electrical and Computer Engineering, vol. 3, May 2004, pp. 1549\u20131552 (2004)"},{"key":"10_CR14","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/j.entcs.2007.08.027","volume":"195","author":"M Xavier","year":"2008","unstructured":"Xavier, M., Cavalcanti, A., Sampaio, A.: Type checking circus specifications. Electr. Notes Theor. Comput. Sci. 195, 75\u201393 (2008). http:\/\/dx.doi.org\/10.1016\/j.entcs.2007.08.027 (Online)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"1","key":"10_CR15","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/1125808.1125811","volume":"15","author":"C Snook","year":"2006","unstructured":"Snook, C., Butler, M.: Uml-b: Formal modeling and design aided by uml. ACM Trans. Softw. Eng. Methodol. 15(1), 92\u2013122 (2006). http:\/\/doi.acm.org\/10.1145\/1125808.1125811 (Online)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"10_CR16","series-title":"LNCS","first-page":"436","volume-title":"MODELS 2007","author":"K Anastasakis","year":"2007","unstructured":"Anastasakis, K., Bordbar, B., Georg, G., Ray, I.: UML2Alloy: a challenging model transformation. In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) MODELS 2007. LNCS, vol. 4735, pp. 436\u2013450. Springer, Heidelberg (2007)"}],"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_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,9]],"date-time":"2023-02-09T21:24:51Z","timestamp":1675977891000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-04915-1_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319049144","9783319049151"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-04915-1_10","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"}}]}}