Abstract
We propose tackling a “mini challenge” problem: a nontrivial verification effort that can be completed in 2-3 years, and will help establish notational standards, common formats, and libraries of benchmarks that will be essential in order for the verification community to collaborate on meeting Hoare’s 15-year verification grand challenge. We believe that a suitable candidate for such a mini challenge is the development of a filesystem that is verifiably reliable and secure. The paper argues why we believe a filesystem is the right candidate for a mini challenge and describes a project in which we are building a small embedded filesystem for use with flash memory.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Hoare, T.: The Verifying Compiler: A Grand Challenge for Computing Research. Journal of the ACM 50(1), 63–69 (2003)
Workshop on the Verification Grand Challenge, SRI International, Menlo Park, CA (February 2005), http://www.csl.sri.com/users/shankar/VGC05
Pnueli, A.: Looking Ahead, Presentation at the Workshop on The Verification Grand Challenge, SRI International, Menlo Park, CA (February 2005), http://www.csl.sri.com/users/shankar/VGC05/pnueli.pdf
The Open Group, The POSIX 1003.1, 2003 Edition Specification, http://www.opengroup.org/certification/idx/posix.html
Morgan, C., Sufrin, B.: Specification of the UNIX Filing System. IEEE Transactions on Software Engineering SE-10(2), 128–142 (1984)
Bevier, W.R., Cohen, R., Turner, J.: A Specification for the Synergy File System, Technical Report 120, Computational Logic, Inc., (September 1995)
Yang, J., Twohey, P., Engler, D., Musuvathi, M.: Using Model Checking to Find Serious File System Errors. In: Proceedings of the Conference on Operating Systems Design and Implementation (OSDI), San Francisco, pp. 273–288 (December 2004)
Data I/O, A Collection of NAND Flash Application Notes, Whitepapers and Articles, http://www.data-io.com/NAND/NANDApplicationNotes.asp
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Joshi, R., Holzmann, G.J. (2008). A Mini Challenge: Build a Verifiable Filesystem. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_6
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_6
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)