References

  1. K. Arkoudas, K. Zee, V. Kuncak & M. C. Rinard (2004): On Verifying a File System Implementation. In: ICFEM, pp. 373–390, doi:10.1007/978-3-540-30482-1_32.
  2. E. Börger & R. F. Stärk (2003): Abstract State Machines—A Method for High-Level System Design and Analysis. Springer-Verlag, doi:10.1007/3-540-36498-6.
  3. A. Butterfield & J. Woodcock (2007): Formalising Flash Memory: First Steps. In: Proc. of the 12th IEEE Int. Conf. on Engineering Complex Computer Systems (ICECCS). IEEE Comp. Soc., Washington DC, USA, pp. 251–260, doi:10.1109/ICECCS.2007.23.
  4. K. Damchoom & M. Butler (2009): Applying Event and Machine Decomposition to a Flash-Based Filestore in Event-B. In: Marcel Vinícius Oliveira & Jim Woodcock: Formal Methods: Foundations and Applications. Springer, Berlin, Heidelberg, pp. 134–152, doi:10.1007/978-3-642-10452-7_10.
  5. K. Damchoom, M. Butler & J.-R. Abrial (2008): Modelling and Proof of a Tree-Structured File System in Event-B and Rodin. In: Proc. of the 10th Int. Conf. on Formal Methods and Sw. Eng. (ICFEM). Springer LNCS 5256, pp. 25–44, doi:10.1007/978-3-540-88194-0_5.
  6. G. Ernst, G. Schellhorn, D. Haneberg, J. Pfähler & W. Reif (2012): KIV models and proofs of VFS and AFS. Available at http://www.informatik.uni-augsburg.de/swt/projects/flash.html.
  7. M.A. Ferreira, S.S. Silva & J.N. Oliveira (2008): 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, pp. 54–71. Available at http://twiki.di.uminho.pt/twiki/pub/Research/VFS/WebHome/overture08sl.pdf. Technical Report CS-TR-1099.
  8. A. Galloway, G. Lüttgen, J.T. Mühlberg & R.I. Siminiceanu (2009): Model-Checking the Linux Virtual File System. In: Proc. VMCAI'09. Springer, pp. 74–88, doi:10.1007/978-3-540-93900-9_10.
  9. W.H. Hesselink & M.I. Lali (2012): Formalizing a hierarchical file system. Form. Asp. Comput. 24(1), pp. 27–44, doi:10.1007/s00165-010-0171-2.
  10. C. A. R. Hoare (2003): The verifying compiler: A grand challenge for computing research.. J. ACM 50(1), pp. 63–69, doi:10.1007/3-540-36579-6_19.
  11. A. Hunter (2008): A Brief Introduction to the Design of UBIFS. Available at http://www.linux-mtd.infradead.org/doc/ubifs_whitepaper.pdf.
  12. R. Joshi & G.J. Holzmann (2007): A mini challenge: build a verifiable filesystem. Formal Aspects of Computing 19(2), doi:10.1007/s00165-006-0022-3.
  13. E. Kang & D. Jackson (2008): Formal Modelling and Analysis of a Flash Filesystem in Alloy. In: Proceedings of ABZ 2008. Springer LNCS 5238, pp. 294 – 308, doi:10.1007/978-3-540-87603-8_23.
  14. C. Morgan & B. Sufrin (1987): Specification of the UNIX filing system. In: Specification case studies. Prentice Hall (UK) Ltd., Hertfordshire, UK, pp. 91–140, doi:10.1109/TSE.1984.5010215.
  15. G. Reeves & T. Neilson (2005): The Mars Rover Spirit FLASH anomaly. In: Aerospace Conference, 2005 IEEE, pp. 4186–4199, doi:10.1109/AERO.2005.1559723.
  16. W. Reif, G. Schellhorn, K. Stenzel & M. Balser (1998): Structured Specifications and Interactive Proofs with KIV. In: W. Bibel & P. Schmitt: Automated Deduction—A Basis for Applications, chapter 1 II. Kluwer, Dordrecht, pp. 13 – 39. Available at http://www.informatik.uni-augsburg.de/de/lehrstuehle/swt/se/publications/1998-struc_spec_proofs_kiv/. ISBN: 978-0-7923-5132-0.
  17. G. Schellhorn, B. Tofan, G. Ernst & W. Reif (2011): Interleaved Programs and Rely-Guarantee Reasoning with ITL. In: Proc. of Temporal Representation and Reasoning (TIME), IEEE, CPS, pp. 99–106, doi:10.1109/TIME.2011.12.
  18. A. Schierl, G. Schellhorn, D. Haneberg & W. Reif (2009): Abstract Specification of the UBIFS File System for Flash Memory. In: Proceedings of FM 2009: Formal Methods. Springer LNCS 5850, pp. 190–206, doi:10.1007/978-3-642-05089-3_13.
  19. M. Szeredi: File system in user space. Available at http://fuse.sourceforge.net.
  20. The Open Group (2008): The Open Group Base Specifications Issue 7, IEEE Std 1003.1, 2008 Edition. Available at http://www.unix.org/version3/online.html. (login required).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org