{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,8]],"date-time":"2024-09-08T00:00:59Z","timestamp":1725753659204},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319030760"},{"type":"electronic","value":"9783319030777"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-319-03077-7_15","type":"book-chapter","created":{"date-parts":[[2013,10,27]],"date-time":"2013-10-27T21:40:21Z","timestamp":1382910021000},"page":"214-229","source":"Crossref","is-referenced-by-count":9,"title":["Formal Specification of an Erase Block Management Layer for Flash Memory"],"prefix":"10.1007","author":[{"given":"J\u00f6rg","family":"Pf\u00e4hler","sequence":"first","affiliation":[]},{"given":"Gidon","family":"Ernst","sequence":"additional","affiliation":[]},{"given":"Gerhard","family":"Schellhorn","sequence":"additional","affiliation":[]},{"given":"Dominik","family":"Haneberg","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Reif","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"15_CR1","doi-asserted-by":"crossref","unstructured":"B\u00f6rger, E., St\u00e4rk, R.F.: Abstract State Machines\u2014A Method for High-Level System Design and Analysis. Springer (2003)","DOI":"10.1007\/978-3-642-18216-7"},{"key":"15_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-10452-7_6","volume-title":"Formal Methods: Foundations and Applications","author":"A. Butterfield","year":"2009","unstructured":"Butterfield, A., \u00d3 Cath\u00e1in, A.: Concurrent models of flash memory device behaviour. In: Oliveira, M.V.M., Woodcock, J. (eds.) SBMF 2009. LNCS, vol.\u00a05902, pp. 70\u201383. Springer, Heidelberg (2009)"},{"issue":"4","key":"15_CR3","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1016\/j.scico.2008.09.014","volume":"74","author":"A. Butterfield","year":"2009","unstructured":"Butterfield, A., Freitas, L., Woodcock, J.: Mechanising a formal model of flash memory. Sci. Comput. Program.\u00a074(4), 219\u2013237 (2009)","journal-title":"Sci. Comput. Program."},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"Butterfield, A., Woodcock, J.: Formalising flash memory: First steps. In: IEEE Int. Conf. on Engineering of Complex Computer Systems, pp. 251\u2013260 (2007)","DOI":"10.1109\/ICECCS.2007.23"},{"issue":"5-6","key":"15_CR5","doi-asserted-by":"publisher","first-page":"332","DOI":"10.1016\/j.sysarc.2009.03.005","volume":"55","author":"T.-S. Chung","year":"2009","unstructured":"Chung, T.-S., Park, D.-J., Park, S., Lee, D.-H., Lee, S.-W., Song, H.-J.: A survey of flash translation layer. J. Syst. Archit.\u00a055(5-6), 332\u2013343 (2009)","journal-title":"J. Syst. Archit."},{"key":"15_CR6","unstructured":"Intel Corp. Intel Flash File System Core Reference Guide, version 1. Technical report, Intel Corporation (2004)"},{"key":"15_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-642-10452-7_10","volume-title":"Formal Methods: Foundations and Applications","author":"K. Damchoom","year":"2009","unstructured":"Damchoom, K., Butler, M.: Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B. In: Oliveira, M.V.M., Woodcock, J. (eds.) SBMF 2009. LNCS, vol.\u00a05902, pp. 134\u2013152. Springer, Heidelberg (2009)"},{"key":"15_CR8","unstructured":"Samsung Electronics. Page program addressing for MLC NAND application note (2009), \n                    \n                      http:\/\/www.samsung.com"},{"key":"15_CR9","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":"15_CR10","unstructured":"Ernst, G., Schellhorn, G., Haneberg, D., Pf\u00e4hler, J., Reif, W.: Verification of a Virtual Filesystem Switch. In: Proc. of Verified Software, Theories Tools and Experiments (to appear, 2013)"},{"key":"15_CR11","unstructured":"Intel Corporation, et al.: Open NAND Flash Interface Specification (June 2013), \n                    \n                      http:\/\/www.onfi.org"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Freitas, L., Woodcock, J., Butterfield, A.: POSIX and the Verification Grand Challenge: A Roadmap. In: ICECCS 2008: Proc. of the 13th IEEE Int. Conf. on Engineering of Complex Computer Systems (2008)","DOI":"10.1109\/ICECCS.2008.35"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"Gal, E., Toledo, S.: Algorithms and Data Structures for flash memory. ACM Computing Surveys, 138\u2013163 (2005)","DOI":"10.1145\/1089733.1089735"},{"key":"15_CR14","unstructured":"Gleixner, T., Haverkamp, F., Bityutskiy, A.: UBI - Unsorted Block Images (2006), \n                    \n                      http:\/\/www.linux-mtd.infradead.org\/doc\/ubidesign\/ubidesign.pdf"},{"issue":"1","key":"15_CR15","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"C.A.R. Hoare","year":"2003","unstructured":"Hoare, C.A.R.: The verifying compiler: A grand challenge for computing research. Journal of the ACM\u00a050(1), 63\u201369 (2003)","journal-title":"Journal of the ACM"},{"key":"15_CR16","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":"15_CR17","unstructured":"INCITS. ATA\/ATAPI Command Set - 2 (ACS-2), Revision 2 (August 3, 2009)"},{"key":"15_CR18","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":"15_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"294","DOI":"10.1007\/978-3-540-87603-8_23","volume-title":"Abstract State Machines, B and Z","author":"E. Kang","year":"2008","unstructured":"Kang, E., Jackson, D.: Formal Modeling and Analysis of a Flash Filesystem in Alloy. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol.\u00a05238, pp. 294\u2013308. Springer, Heidelberg (2008)"},{"issue":"2-3","key":"15_CR20","first-page":"129","volume":"3","author":"E. Kang","year":"2009","unstructured":"Kang, E., Jackson, D.: Designing and analyzing a flash file system with alloy. Int. J. Software and Informatics\u00a03(2-3), 129\u2013148 (2009)","journal-title":"Int. J. Software and Informatics"},{"key":"15_CR21","unstructured":"Knight, F.: TRIM - DRAT\/RZAT clarifications for ATA8-ACS2, Revision 2 (February 23, 2010)"},{"key":"15_CR22","unstructured":"Memory Technology Device (MTD) and Unsorted Block Images (UBI) Subsystem of Linux, \n                    \n                      http:\/\/www.linux-mtd.infradead.org\/index.html"},{"key":"15_CR23","volume-title":"Programming in Scala: A Comprehensive Step-by-step Guide","author":"M. Odersky","year":"2008","unstructured":"Odersky, M., Spoon, L., Venners, B.: Programming in Scala: A Comprehensive Step-by-step Guide, 1st edn. Artima Incorporation, USA (2008)","edition":"1"},{"key":"15_CR24","unstructured":"Pf\u00e4hler, J., Ernst, G., Haneberg, D., Schellhorn, G., Reif, W.: KIV models and proofs of MTD, UBI and abstract UBI (2013), \n                    \n                      http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/flash.html"},{"key":"15_CR25","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":"15_CR26","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)"},{"key":"15_CR27","doi-asserted-by":"crossref","unstructured":"Schellhorn, G., Tofan, B., Ernst, G., Reif, W.: Interleaved programs and rely-guarantee reasoning with ITL. In: Proc. of TIME, pp. 99\u2013106. IEEE Computer Society (2011)","DOI":"10.1109\/TIME.2011.12"},{"key":"15_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-642-05089-3_13","volume-title":"FM 2009: Formal Methods","author":"A. Schierl","year":"2009","unstructured":"Schierl, A., Schellhorn, G., Haneberg, D., Reif, W.: Abstract Specification of the UBIFS File System for Flash Memory. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.\u00a05850, pp. 190\u2013206. Springer, Heidelberg (2009)"},{"key":"15_CR29","unstructured":"The Open Group. The Open Group Base Specifications Issue 7, IEEE Std 1003.1, 2008 edn. (2008), \n                    \n                      http:\/\/www.unix.org\/version3\/online.html\n                    \n                    \n                   (login required)"},{"key":"15_CR30","unstructured":"UBI - Out-of-Band Data Area, \n                    \n                      http:\/\/www.linux-mtd.infradead.org\/faq\/ubi.html"},{"key":"15_CR31","unstructured":"UBIFS - Unstable Bits Issue, \n                    \n                      http:\/\/www.linux-mtd.infradead.org\/doc\/ubifs.html"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-03077-7_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,23]],"date-time":"2019-05-23T19:53:51Z","timestamp":1558641231000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-03077-7_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783319030760","9783319030777"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-03077-7_15","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}