{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,27]],"date-time":"2025-05-27T12:58:46Z","timestamp":1748350726402},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642050886"},{"type":"electronic","value":"9783642050893"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-05089-3_13","type":"book-chapter","created":{"date-parts":[[2009,11,3]],"date-time":"2009-11-03T22:31:40Z","timestamp":1257287500000},"page":"190-206","source":"Crossref","is-referenced-by-count":29,"title":["Abstract Specification of the UBIFS File System for Flash Memory"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Schierl","sequence":"first","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":"13_CR1","unstructured":"Balser, M., B\u00e4umler, S., Reif, W., Schellhorn, G.: Interactive verification of concurrent systems using symbolic execution. In: Proceedings of 7th International Workshop of Implementation of Logics, IWIL 2008 (2008)"},{"key":"13_CR2","unstructured":"B\u00e4umler, S., Nafz, F., Balser, M., Reif, W.: Compositional proofs with symbolic execution. In: Beckert, B., Klein, G. (eds.) Proceedings of the 5th International Verification Workshop. Ceur Workshop Proceedings, vol.\u00a0372 (2008)"},{"key":"13_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-18216-7","volume-title":"Abstract State Machines\u2014A Method for High-Level System Design and Analysis","author":"E. B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E., St\u00e4rk, R.F.: Abstract State Machines\u2014A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)"},{"key":"13_CR4","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1109\/ICECCS.2007.23","volume-title":"Proc.\u00a0of the 12th IEEE Int.\u00a0Conf.\u00a0on Engineering Complex Computer Systems (ICECCS)","author":"A. Butterfield","year":"2007","unstructured":"Butterfield, A., Woodcock, J.: Formalising flash memory: First steps. In: Proc.\u00a0of the 12th IEEE Int.\u00a0Conf.\u00a0on Engineering Complex Computer Systems (ICECCS), Washington DC, USA, pp. 251\u2013260. IEEE Comp.\u00a0Soc., Los Alamitos (2007)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-540-88194-0_5","volume-title":"Formal Methods and Software Engineering","author":"K. Damchoom","year":"2008","unstructured":"Damchoom, K., Butler, M., Abrial, J.-R.: Modelling and proof of a tree-structured file system in Event-B and Rodin. In: Liu, S., Maibaum, T., Araki, K. (eds.) ICFEM 2008. LNCS, vol.\u00a05256, pp. 25\u201344. Springer, Heidelberg (2008)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-88387-6_12","volume-title":"Automated Technology for Verification and Analysis","author":"A. Dunets","year":"2008","unstructured":"Dunets, A., Schellhorn, G., Reif, W.: Automating Algebraic Specifications of Non-freely Generated Data Types. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol.\u00a05311, pp. 141\u2013155. Springer, Heidelberg (2008)"},{"key":"13_CR7","unstructured":"Ferreira, M.A., Silva, S.S., Oliveira, J.N.: Verifying Intel flash file system core specification. In: Modelling and Analysis in VDM: Proceedings of the Fourth VDM\/Overture Workshop. School of Computing Science, Newcastle University (2008) Technical Report CS-TR-1099"},{"key":"13_CR8","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 Eng. of Complex Computer Systems, Washington, DC, USA, pp. 153\u2013162 (2008)","DOI":"10.1109\/ICECCS.2008.35"},{"key":"13_CR9","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":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/978-3-540-68237-0_13","volume-title":"FM 2008: Formal Methods","author":"H. Grandy","year":"2008","unstructured":"Grandy, H., Bischof, M., Schellhorn, G., Reif, W., Stenzel, K.: Verification of Mondex Electronic Purses with KIV: From a Security Protocol to Verified Code. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol.\u00a05014, pp. 165\u2013180. Springer, Heidelberg (2008)"},{"key":"13_CR11","first-page":"9","volume-title":"Specification and Validation Methods","author":"Y. Gurevich","year":"1995","unstructured":"Gurevich, Y.: Evolving algebras 1993: Lipari guide. In: B\u00f6rger, E. (ed.) Specification and Validation Methods, pp. 9\u201336. Oxford Univ. Press, Oxford (1995)"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Haneberg, D., Schellhorn, G., Grandy, H., Reif, W.: Verification of Mondex Electronic Purses with KIV: From Transactions to a Security Protocol. Formal Aspects of Computing\u00a020(1) (January 2008)","DOI":"10.1007\/s00165-007-0057-0"},{"issue":"1","key":"13_CR13","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. J. ACM\u00a050(1), 63\u201369 (2003)","journal-title":"J. ACM"},{"key":"13_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":"13_CR15","unstructured":"The Open Group Base Specifications Issue 6, IEEE Std 1003.1, 2004 Edition (2004), \n                    \n                      http:\/\/www.unix.org\/version3\/online.html\n                    \n                    \n                   (login required)"},{"key":"13_CR16","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":"13_CR17","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 modelling 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)"},{"key":"13_CR18","unstructured":"Web presentation of the Flash File System Case Study in KIV (2009), \n                    \n                      http:\/\/www.informatik.uni-augsburg.de\/swt\/projects\/flash.html"},{"key":"13_CR19","unstructured":"LXR - the Linux cross reference, \n                    \n                      http:\/\/lxr.linux.no\/"},{"key":"13_CR20","first-page":"91","volume-title":"Specification case studies","author":"C. Morgan","year":"1987","unstructured":"Morgan, C., Sufrin, B.: Specification of the UNIX filing system. In: Specification case studies, pp. 91\u2013140. Prentice Hall (UK) Ltd., Hertfordshire (1987)"},{"key":"13_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/978-3-642-03153-3_5","volume-title":"LerNet ALFA Summer School 2008","author":"J.N. Oliveira","year":"2009","unstructured":"Oliveira, J.N.: Extended Static Checking by Calculation Using the Pointfree Transform. In: Bove, A., et al. (eds.) LerNet ALFA Summer School 2008. LNCS, vol.\u00a05520, pp. 195\u2013251. Springer, Heidelberg (2009)"},{"key":"13_CR22","first-page":"4186","volume-title":"Aerospace Conference","author":"G. Reeves","year":"2005","unstructured":"Reeves, G., Neilson, T.: The Mars Rover Spirit FLASH anomaly. In: Aerospace Conference, pp. 4186\u20134199. IEEE, Los Alamitos (2005)"},{"key":"13_CR23","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1007\/978-94-017-0435-9_1","volume-title":"Automated Deduction\u2014A Basis for Applications, ch.\u00a01","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, ch.\u00a01, vol.\u00a0II, pp. 13\u201339. Kluwer Academic Publishers, Dordrecht (1998)"},{"key":"13_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"39","DOI":"10.1007\/978-3-540-87603-8_4","volume-title":"Abstract State Machines, B and Z","author":"G. Schellhorn","year":"2008","unstructured":"Schellhorn, G., Banach, R.: A concept-driven construction of the mondex protocol using three refinements. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol.\u00a05238, pp. 39\u201341. Springer, Heidelberg (2008)"},{"key":"13_CR25","series-title":"Lecture Notes in Computer Science","volume-title":"Dagstuhl Seminar on Rigorous Methods for Software Construction and Analysis","author":"G. Schellhorn","year":"2008","unstructured":"Schellhorn, G., Grandy, H., Haneberg, D., Moebius, N., Reif, W.: A Systematic Verification Approach for Mondex Electronic Purses using ASMs. In: Gl\u00e4sser, U., Abrial, J.-R. (eds.) Dagstuhl Seminar on Rigorous Methods for Software Construction and Analysis. LNCS, vol.\u00a05115. Springer, Heidelberg (2008)"},{"issue":"4","key":"13_CR26","doi-asserted-by":"crossref","first-page":"339","DOI":"10.3233\/JCS-2002-10403","volume":"10","author":"G. Schellhorn","year":"2002","unstructured":"Schellhorn, G., Reif, W., Schairer, A., Karger, P., Austel, V., Toll, D.: Verified Formal Security Models for Multiapplicative Smart Cards. Special issue of the Journal of Computer Security\u00a010(4), 339\u2013367 (2002)","journal-title":"Special issue of the Journal of Computer Security"},{"key":"13_CR27","volume-title":"The Z Notation: A Reference Manual","author":"J.M. Spivey","year":"1992","unstructured":"Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall, Englewood Cliffs (1992)"},{"key":"13_CR28","unstructured":"STMicroelectronics. SPC56xB\/C\/D Automotive 32-bit Flash microcontrollers for car body applications (February 2009), \n                    \n                      http:\/\/www.st.com\/stonline\/products\/promlit\/a_automotive.htm"},{"key":"13_CR29","unstructured":"Woodhouse, D.: JFFS: The Journalling Flash File System (2001), \n                    \n                      http:\/\/sources.redhat.com\/jffs2\/jffs2.pdf"}],"container-title":["Lecture Notes in Computer Science","FM 2009: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-05089-3_13.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T11:19:01Z","timestamp":1619781541000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-05089-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642050886","9783642050893"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-05089-3_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}