Abstract
Today we see an increasing demand for flash memory because it has certain advantages like resistance against kinetic shock. However, reliable data storage also requires a specialized file system knowing and handling the limitations of flash memory. This paper develops a formal, abstract model for the UBIFS flash file system, which has recently been included in the Linux kernel. We develop formal specifications for the core components of the file system: the inode-based file store, the flash index, its cached copy in the RAM and the journal to save the differences. Based on these data structures we give an abstract specification of the interface operations of UBIFS and prove some of the most important properties using the interactive verification system KIV.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Balser, M., Bäumler, 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)
Bäumler, 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. 372 (2008)
Börger, E., Stärk, R.F.: Abstract State Machines—A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003)
Butterfield, A., Woodcock, J.: Formalising flash memory: First steps. In: Proc. of the 12th IEEE Int. Conf. on Engineering Complex Computer Systems (ICECCS), Washington DC, USA, pp. 251–260. IEEE Comp. Soc., Los Alamitos (2007)
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. 5256, pp. 25–44. Springer, Heidelberg (2008)
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. 5311, pp. 141–155. Springer, Heidelberg (2008)
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
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–162 (2008)
Gal, E., Toledo, S.: Algorithms and data structures for flash memory. ACM computing surveys, 138–163 (2005)
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. 5014, pp. 165–180. Springer, Heidelberg (2008)
Gurevich, Y.: Evolving algebras 1993: Lipari guide. In: Börger, E. (ed.) Specification and Validation Methods, pp. 9–36. Oxford Univ. Press, Oxford (1995)
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 20(1) (January 2008)
Hoare, C.A.R.: The verifying compiler: A grand challenge for computing research. J. ACM 50(1), 63–69 (2003)
Hunter, A.: A brief introduction to the design of UBIFS (2008), http://www.linux-mtd.infradead.org/doc/ubifs_whitepaper.pdf
The Open Group Base Specifications Issue 6, IEEE Std 1003.1, 2004 Edition (2004), http://www.unix.org/version3/online.html (login required)
Joshi, R., Holzmann, G.J.: A mini challenge: build a verifiable filesystem. Formal Aspects of Computing 19(2) (June 2007)
Kang, E., Jackson, D.: Formal modelling and analysis of a flash filesystem in Alloy. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 294–308. Springer, Heidelberg (2008)
Web presentation of the Flash File System Case Study in KIV (2009), http://www.informatik.uni-augsburg.de/swt/projects/flash.html
LXR - the Linux cross reference, http://lxr.linux.no/
Morgan, C., Sufrin, B.: Specification of the UNIX filing system. In: Specification case studies, pp. 91–140. Prentice Hall (UK) Ltd., Hertfordshire (1987)
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. 5520, pp. 195–251. Springer, Heidelberg (2009)
Reeves, G., Neilson, T.: The Mars Rover Spirit FLASH anomaly. In: Aerospace Conference, pp. 4186–4199. IEEE, Los Alamitos (2005)
Reif, W., Schellhorn, G., Stenzel, K., Balser, M.: Structured specifications and interactive proofs with KIV. In: Bibel, W., Schmitt, P. (eds.) Automated Deduction—A Basis for Applications, ch. 1, vol. II, pp. 13–39. Kluwer Academic Publishers, Dordrecht (1998)
Schellhorn, G., Banach, R.: A concept-driven construction of the mondex protocol using three refinements. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 39–41. Springer, Heidelberg (2008)
Schellhorn, G., Grandy, H., Haneberg, D., Moebius, N., Reif, W.: A Systematic Verification Approach for Mondex Electronic Purses using ASMs. In: Glässer, U., Abrial, J.-R. (eds.) Dagstuhl Seminar on Rigorous Methods for Software Construction and Analysis. LNCS, vol. 5115. Springer, Heidelberg (2008)
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 10(4), 339–367 (2002)
Spivey, J.M.: The Z Notation: A Reference Manual. Prentice Hall, Englewood Cliffs (1992)
STMicroelectronics. SPC56xB/C/D Automotive 32-bit Flash microcontrollers for car body applications (February 2009), http://www.st.com/stonline/products/promlit/a_automotive.htm
Woodhouse, D.: JFFS: The Journalling Flash File System (2001), http://sources.redhat.com/jffs2/jffs2.pdf
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Schierl, A., Schellhorn, G., Haneberg, D., Reif, W. (2009). Abstract Specification of the UBIFS File System for Flash Memory. In: Cavalcanti, A., Dams, D.R. (eds) FM 2009: Formal Methods. FM 2009. Lecture Notes in Computer Science, vol 5850. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-05089-3_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-05089-3_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-05088-6
Online ISBN: 978-3-642-05089-3
eBook Packages: Computer ScienceComputer Science (R0)