{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T11:27:51Z","timestamp":1725794871940},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662436516"},{"type":"electronic","value":"9783662436523"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-43652-3_16","type":"book-chapter","created":{"date-parts":[[2014,5,29]],"date-time":"2014-05-29T02:22:12Z","timestamp":1401330132000},"page":"188-203","source":"Crossref","is-referenced-by-count":2,"title":["Modular Refinement for Submachines of ASMs"],"prefix":"10.1007","author":[{"given":"Gidon","family":"Ernst","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"J\u00f6rg","family":"Pf\u00e4hler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"Abrial, J.-R., Hallerstede, S.: Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B. Fundamenta Informaticae\u00a077 (2007)"},{"key":"16_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: The B\u00a0Book - Assigning Programs to Meanings. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511624162"},{"key":"16_CR3","doi-asserted-by":"crossref","unstructured":"Abrial, J.-R.: Modeling in Event-B. Cambridge University Press (2010)","DOI":"10.1017\/CBO9781139195881"},{"issue":"1-2","key":"16_CR4","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/s00165-003-0012-7","volume":"15","author":"E. B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E.: The ASM Refinement Method. Formal Aspects of Computing\u00a015(1-2), 237\u2013257 (2003)","journal-title":"Formal Aspects of Computing"},{"key":"16_CR5","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E., St\u00e4rk, R.F.: Abstract State Machines \u2014 A Method for High-Level System Design and Analysis. Springer (2003)","DOI":"10.1007\/978-3-642-18216-7"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-642-00255-7_2","volume-title":"Integrated Formal Methods","author":"M. Butler","year":"2009","unstructured":"Butler, M.: Decomposition Structures for Event-B. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol.\u00a05423, pp. 20\u201338. Springer, Heidelberg (2009)"},{"key":"16_CR7","doi-asserted-by":"crossref","unstructured":"de Roever, W., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge Tracts in Theoretical Computer Science, vol.\u00a047. Cambridge University Press (1998)","DOI":"10.1017\/CBO9780511663079"},{"key":"16_CR8","doi-asserted-by":"crossref","unstructured":"Derrick, J., Boiten, E.: Refinement in Z and in Object-Z: Foundations and Advanced Applications. FACIT, 2nd revised edn. Springer (2014)","DOI":"10.1007\/978-1-4471-5355-9"},{"key":"16_CR9","unstructured":"Ernst, G., Pf\u00e4hler, J., Schellhorn, G.: Web presentation of the Flash Filesystem (2014), \n                  \n                    https:\/\/swt.informatik.uni-augsburg.de\/swt\/projects\/flash.html"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Ernst, G., Schellhorn, G., Haneberg, D., Pf\u00e4hler, J., Reif, W.: A Formal Model of a Virtual Filesystem Switch. In: Proc. of Software and Systems Modeling (SSV), pp. 33\u201345 (2012)","DOI":"10.4204\/EPTCS.102.5"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-642-54108-7_13","volume-title":"Verified Software: Theories, Tools, Experiments","author":"G. Ernst","year":"2014","unstructured":"Ernst, G., Schellhorn, G., Haneberg, D., Pf\u00e4hler, J., Reif, W.: Verification of a Virtual Filesystem Switch. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol.\u00a08164, pp. 242\u2013261. Springer, Heidelberg (2014)"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-16442-1_14","volume-title":"ESOP 86","author":"J. He","year":"1986","unstructured":"He, J., Hoare, C.A.R., Sanders, J.W.: Data refinement refined. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol.\u00a0213, pp. 187\u2013196. Springer, Heidelberg (1986)"},{"key":"16_CR14","unstructured":"Hunter, A.: A brief introduction to the design of UBIFS (2008), \n                  \n                    http:\/\/www.linux-mtd.infradead.org\/doc\/ubifs_whitepaper.pdf"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Joshi, R., Holzmann, G.J.: A mini challenge: build a verifiable filesystem. Formal Aspects of Computing\u00a019(2) (June 2007)","DOI":"10.1007\/s00165-006-0022-3"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Moszkowski, B.: Executing Temporal Logic Programs. Cambr. Univ. Press (1986)","DOI":"10.1007\/3-540-15670-4_6"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/3-540-45022-X_19","volume-title":"Automata, Languages and Programming","author":"B.C. Moszkowski","year":"2000","unstructured":"Moszkowski, B.C.: An automata-theoretic completeness proof for Interval Temporal Logic. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol.\u00a01853, pp. 223\u2013234. Springer, Heidelberg (2000)"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-319-03077-7_15","volume-title":"Hardware and Software: Verification and Testing","author":"J. Pf\u00e4hler","year":"2013","unstructured":"Pf\u00e4hler, J., Ernst, G., Schellhorn, G., Haneberg, D., Reif, W.: Formal Specification of an Erase Block Management Layer for Flash Memory. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol.\u00a08244, pp. 214\u2013229. Springer, Heidelberg (2013)"},{"key":"16_CR19","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University (1981)"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Reeves, G., Neilson, T.: The Mars Rover Spirit FLASH anomaly. In: Aerospace Conference, pp. 4186\u20134199. IEEE Computer Society (2005)","DOI":"10.1109\/AERO.2005.1559723"},{"key":"16_CR21","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1007\/978-94-017-0435-9_1","volume-title":"Automated Deduction\u2014A Basis for Applications","author":"W. Reif","year":"1998","unstructured":"Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction\u2014A Basis for Applications, vol.\u00a0II, pp. 13\u201339. Kluwer, Dordrecht (1998)"},{"issue":"11","key":"16_CR22","first-page":"952","volume":"7","author":"G. Schellhorn","year":"2001","unstructured":"Schellhorn, G.: Verification of ASM Refinements Using Generalized Forward Simulation. Journal of Universal Computer Science (J.UCS)\u00a07(11), 952\u2013979 (2001), \n                  \n                    http:\/\/www.jucs.org","journal-title":"Journal of Universal Computer Science (J.UCS)"},{"issue":"2-3","key":"16_CR23","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1016\/j.tcs.2004.11.013","volume":"336","author":"G. Schellhorn","year":"2005","unstructured":"Schellhorn, G.: ASM Refinement and Generalizations of Forward Simulation in Data Refinement: A Comparison. Journal of Theoretical Computer Science\u00a0336(2-3), 403\u2013435 (2005)","journal-title":"Journal of Theoretical Computer Science"},{"key":"16_CR24","doi-asserted-by":"crossref","unstructured":"Schellhorn, G.: Completeness of Fair ASM Refinement. Science of Computer Programming, 76(9) (2009)","DOI":"10.1016\/j.scico.2009.10.004"},{"key":"16_CR25","series-title":"LNCS","first-page":"9","volume-title":"ABZ 2014","author":"G. Schellhorn","year":"2014","unstructured":"Schellhorn, G., Ernst, G., Pf\u00e4hler, J., Haneberg, D., Reif, W.: Development of a Verified Flash File System. In: Ait Ameur, Y., Schewe, K.-D. (eds.) ABZ 2014. LNCS, vol.\u00a08477, pp. 9\u201324. Springer, Heidelberg (2014)"},{"key":"16_CR26","unstructured":"Schellhorn, G., Tofan, B., Ernst, G., Pf\u00e4hler, J., Reif, W.: RGITL: A Temporal Logic Framework for Compositional Reasoning about Interleaved Programs. In: AMAI (2014), appeared online first, draft available at \n                  \n                    https:\/\/swt.informatik.uni-augsburg.de\/swt\/projects\/RGITL.html"},{"issue":"11","key":"16_CR27","first-page":"981","volume":"7","author":"R.F. St\u00e4rk","year":"2001","unstructured":"St\u00e4rk, R.F., Nanchen, S.: A Complete Logic for Abstract State Machines. Journal of Universal Computer Science (J.UCS)\u00a07(11), 981\u20131006 (2001)","journal-title":"Journal of Universal Computer Science (J.UCS)"},{"key":"16_CR28","unstructured":"The Open Group. The Open Group Base Specifications Issue 7, IEEE Std 1003.1, 2008 Edition (2008), \n                  \n                    http:\/\/www.unix.org\/version3\/online.html\n                  \n                  \n                 (login required)"},{"key":"16_CR29","unstructured":"Woodcock, J.C.P., Davies, J.: Using Z: Specification, Proof and Refinement. Prentice Hall International Series in Computer Science (1996)"}],"container-title":["Lecture Notes in Computer Science","Abstract State Machines, Alloy, B, TLA, VDM, and Z"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-43652-3_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T23:05:56Z","timestamp":1558911956000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-43652-3_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783662436516","9783662436523"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-43652-3_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}