A mini challenge: build a verifiable filesystem
A mini challenge: build a verifiable filesystem
复制标题
一个小挑战：构建一个可验证的文件系统
DOI：
10.1007/s00165-006-0022-3
复制
发表时间：
2007
影响因子：
1
通讯作者：
G. Holzmann
中科院分区：
文献类型：
--
作者：
Rajeev Joshi;G. Holzmann
我们建议解决一个“迷你挑战”问题：一个可以在2 - 3年内完成的非平凡验证工作，并将有助于建立符号标准，常见格式和基准图书馆，这对于验证社区而言至关重要在满足Hoare的15年验证挑战赛时，我们认为这是一个小型挑战的候选人是一个可靠和安全的文件系统的开发。并描述了一个项目，在该项目中，我们正在构建一个用于闪存的小型嵌入式文件系统。
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.